Length of proof is 47. Level of proof is 18. ---------------- PROOF ---------------- 2 [] x*1=1 # label("M3"). 3 [] 1*x=x # label("M4"). 4 [] x*y!=1|y*x!=1|x=y # label("M7"). 5 [] (x*y)* ((z*x)* (z*y))=1 # label("M5"). 6 [] x*x=1 # label("M8"). 7 [] x* (y*z)=y* (x*z) # label("M9"). 8 [] (x*y)* (x*z)= (y*x)* (y*z) # label("H"). 9 [] (((x*y)*y)*x)*x=g(x,y) # label("Definition"). 10 [] g(b,a)!=g(a,b). 74 [para_from,5.1.2,3.1.1.1] ((x*y)* ((z*x)* (z*y)))*u=u. 84 [para_from,6.1.2,2.1.1.2] x* (y*y)=1. 97 [para_into,7.1.1,84.1.1,flip.1] x* (y*x)=1. 98 [para_into,7.1.1,6.1.1,flip.1] x* ((x*y)*y)=1. 103 [para_from,7.1.1,5.1.1.2] (x*y)* (z* ((z*x)*y))=1. 114 [para_from,97.1.2,3.1.1.1] (x* (y*x))*z=z. 130 [para_from,98.1.1,5.1.1.2.1] (((x*y)*y)*z)* (1* (x*z))=1. 156 [para_from,9.1.1,98.1.1.2] ((x*y)*y)*g(x,y)=1. 177 [para_into,8.1.1.1,156.1.1,flip.1] (g(x,y)* ((x*y)*y))* (g(x,y)*z)=1* (((x*y)*y)*z). 186 [para_into,8.1.1,7.1.2,flip.1] (x*y)* (x*z)=y* ((y*x)*z). 206 [para_into,103.1.1,7.1.2] x* ((y*z)* ((x*y)*z))=1. 222 [para_into,206.1.1.2.2,114.1.1] x* (((y*x)*z)*z)=1. 229 [para_into,206.1.1.2,7.1.2] x* ((x*y)* ((y*z)*z))=1. 298 [para_into,130.1.1.2,3.1.1] (((x*y)*y)*z)* (x*z)=1. 302 [hyper,298,4,98,flip.1] ((x*y)*y)*y=x*y. 332 [para_into,302.1.1.1,9.1.1,flip.1] ((x*y)*y)*x=g(x,y)*x. 357 [para_from,332.1.1,9.1.1.1] (g(x,y)*x)*x=g(x,y). 369 [para_into,186.1.1.2,357.1.1] ((g(x,y)*x)*z)*g(x,y)=z* ((z* (g(x,y)*x))*x). 375 [para_into,186.1.1,7.1.2] x* ((x*y)*z)=y* ((y*x)*z). 385 [para_from,186.1.1,222.1.1.2.1.1] (x*y)* (((z* ((z*x)*y))*u)*u)=1. 394 [para_from,375.1.1,229.1.1.2.1] x* ((y* ((y*x)*z))* ((((x*y)*z)*u)*u))=1. 400 [para_into,385.1.1.2.1.1.2.1,98.1.1] (((x*y)*y)*z)* (((x* (1*z))*u)*u)=1. 401 [para_into,385.1.1.2.1.1.2,114.1.1] ((x*y)*z)* (((y*z)*u)*u)=1. 432 [para_into,401.1.1,7.1.2] ((x*y)*z)* (((u*x)*y)*z)=1. 454 [para_into,432.1.1.2,9.1.1] ((x*y)*y)*g(y,x)=1. 478 [para_from,454.1.1,375.1.1.2.1,flip.1] g(x,y)* ((g(x,y)* ((y*x)*x))*z)= ((y*x)*x)* (1*z). 516 [para_into,400.1.1.2.1.1.2,3.1.1] (((x*y)*y)*z)* (((x*z)*u)*u)=1. 523 [para_into,516.1.1.2,9.1.1] ((((x*y)*z)*z)*y)*g(x,y)=1. 541 [para_into,394.1.1.2.2.1,523.1.1] ((x*y)*z)* ((z* ((z* ((x*y)*z))*y))* (1*g(x,y)))=1. 548 [para_into,177.1.1.1,7.1.2] ((x*y)* (g(x,y)*y))* (g(x,y)*z)=1* (((x*y)*y)*z). 549 [para_into,478.1.1.2.1,7.1.2] g(x,y)* (((y*x)* (g(x,y)*x))*z)= ((y*x)*x)* (1*z). 551 [para_into,541.1.1.2.1.2,114.1.1] ((x*y)*z)* ((z*y)* (1*g(x,y)))=1. 587 [para_into,551.1.1.2.2,3.1.1] ((x*y)*z)* ((z*y)*g(x,y))=1. 608 [para_into,587.1.1,7.1.2] (x*y)* (((z*y)*x)*g(z,y))=1. 624 [para_from,608.1.1,401.1.1.2.1] ((x*y)*z)* (1* (((u*z)*y)*g(u,z)))=1. 627 [para_into,624.1.1.2,3.1.1] ((x*y)*z)* (((u*z)*y)*g(u,z))=1. 640 [para_into,548.1.2,3.1.1] ((x*y)* (g(x,y)*y))* (g(x,y)*z)= ((x*y)*y)*z. 641 [para_from,640.1.1,369.1.2.2.1] ((g(x,y)*x)* ((x*y)* (g(x,y)*y)))*g(x,y)= ((x*y)* (g(x,y)*y))* ((((x*y)*y)*x)*x). 642 [para_into,549.1.1,7.1.2] ((x*y)* (g(y,x)*y))* (g(y,x)*z)= ((x*y)*y)* (1*z). 670 [para_into,642.1.2.2,3.1.1] ((x*y)* (g(y,x)*y))* (g(y,x)*z)= ((x*y)*y)*z. 672 [para_into,641.1.1.1,7.1.2,flip.1] ((x*y)* (g(x,y)*y))* ((((x*y)*y)*x)*x)= ((x*y)* ((g(x,y)*x)* (g(x,y)*y)))*g(x,y). 673 [para_into,672.1.2,74.1.1] ((x*y)* (g(x,y)*y))* ((((x*y)*y)*x)*x)=g(x,y). 674 [para_into,673.1.1.2,9.1.1] ((x*y)* (g(x,y)*y))*g(x,y)=g(x,y). 678 [para_from,674.1.1,627.1.1.2] ((x* (g(y,z)*z))*z)*g(y,z)=1. 682 [para_into,678.1.1.1.1,670.1.1] ((((x*y)*y)*x)*x)*g(y,x)=1. 689 [para_into,682.1.1.1,9.1.1] g(x,y)*g(y,x)=1. 719 [hyper,689,4,689] g(x,y)=g(y,x). 720 [binary,719.1,10.1] $F. ------------ end of proof / derivation -------------