(x @ y) @ z = u @ (v @ w) (A) "associativity" of commutator (x @ y) * z = z * (x @ y) (N) nilpotency of class 2 (x * y) @ z = (x @ z) * (y @ z) (D) distributivity of commutator x*y*z*y*x = y*x*z*x*y (E) CS essence of (N)In cancellative semigroups, we cannot define the commutator operation, because we don't necessarily have in inverse operation.
Consider, however, the following property of the commutator operation.
y * x * (x @ y) = x * y. % CS admits commutatorThen the four properties hold for cancellative semigroups.
Here are 24 proofs. We prove all pairwise implications between the four properties for both group theory and cancellative semigroups. (Of course we only need 8 of these proofs.)
The file AD-gt.out means (A) -> (D) for group theory.
prover9 -f gt.in AD.in > AD-gt.out ; ### ( AD-gt.out.xml )
prover9 -f cs.in AD.in > AD-cs.out ; ### ( AD-cs.out.xml )
prover9 -f gt.in AE.in > AE-gt.out ; ### ( AE-gt.out.xml )
prover9 -f cs.in AE.in > AE-cs.out ; ### ( AE-cs.out.xml )
prover9 -f gt.in AN.in > AN-gt.out ; ### ( AN-gt.out.xml )
prover9 -f cs.in AN.in > AN-cs.out ; ### ( AN-cs.out.xml )
prover9 -f gt.in DA.in > DA-gt.out ; ### ( DA-gt.out.xml )
prover9 -f cs.in DA.in > DA-cs.out ; ### ( DA-cs.out.xml )
prover9 -f gt.in DE.in > DE-gt.out ; ### ( DE-gt.out.xml )
prover9 -f cs.in DE.in > DE-cs.out ; ### ( DE-cs.out.xml )
prover9 -f gt.in DN.in > DN-gt.out ; ### ( DN-gt.out.xml )
prover9 -f cs.in DN.in > DN-cs.out ; ### ( DN-cs.out.xml )
prover9 -f gt.in EA.in > EA-gt.out ; ### ( EA-gt.out.xml )
prover9 -f cs.in EA.in > EA-cs.out ; ### ( EA-cs.out.xml )
prover9 -f gt.in ED.in > ED-gt.out ; ### ( ED-gt.out.xml )
prover9 -f cs.in ED.in > ED-cs.out ; ### ( ED-cs.out.xml )
prover9 -f gt.in EN.in > EN-gt.out ; ### ( EN-gt.out.xml )
prover9 -f cs.in EN.in > EN-cs.out ; ### ( EN-cs.out.xml )
prover9 -f gt.in NA.in > NA-gt.out ; ### ( NA-gt.out.xml )
prover9 -f cs.in NA.in > NA-cs.out ; ### ( NA-cs.out.xml )
prover9 -f gt.in ND.in > ND-gt.out ; ### ( ND-gt.out.xml )
prover9 -f cs.in ND.in > ND-cs.out ; ### ( ND-cs.out.xml )
prover9 -f gt.in NE.in > NE-gt.out ; ### ( NE-gt.out.xml )
prover9 -f cs.in NE.in > NE-cs.out ; ### ( NE-cs.out.xml )