Proof in predicate calculus 2

[solakis]

Let:

1) P be one place operation

2) H be two place operation

3) G be two place predicate

4) k, m be two constants


Let :

The following assumptions :

1) $\forall x [\neg G(x,k)\Longrightarrow G[H(P(x),x),m]]$



2)$\forall x\forall y\forall z[G(x,y)\Longrightarrow G[H(z,x),H(z,y)]]$

3)$\forall x\forall y\forall z [G(x,y)\wedge G(y,z)\Longrightarrow G(x,z)]$

4)$\forall x\forall y [G(x,y)\Longrightarrow G(y,x)]$

5)$\forall x\forall y [G[H(x,y),H(y,x)]]$

6)$\forall x[ G[H(x,m),m]]$

Then formally prove that:

Then formally prove : $\forall x\forall y\forall z[\neg G(x,k)\Longrightarrow(G[H(x,y),H(x,z)]\Longrightarrow G(y,z))]$

 

[CompuChip]

That's the same one as here, luckily you've formatted it a bit better this time (Y).

Any progress on the answer?

 

[solakis]

That's the same one as here, luckily you've formatted it a bit better this time (Y).

Any progress on the answer?

That is a completely different problem.

No, no any answer yet.