********** AIM Axioms ********** % loop axioms 1 * x = x. x * 1 = x. x \ (x * y) = y. x * (x \ y) = y. (x * y) / y = x. (x / y) * y = x. % associator (x * (y * z)) \ ((x * y) * z) = a(x,y,z). % commutator (x * y) \ (y * x) = K(y,x). % inner mappings % L_(x,y) = L_x * L_y * (L_(y*x))^(-1) L(u,x,y) = (y * x) \ (y * (x * u)). % R_(x,y) = R_x * R_y * (R_(x*y))^(-1) R(u,x,y) = ((u * x) * y) / (x * y). % T_x = R_x * (L_x)^(-1) T(u,x) = x \ (u * x). % abelian inner mapping group T(T(u,x),y) = T(T(u,y),x). T(L(u,x,y),z) = L(T(u,z),x,y). T(R(u,x,y),z) = R(T(u,z),x,y). L(R(u,x,y),z,w) = R(L(u,z,w),x,y). L(L(u,x,y),z,w) = L(L(u,z,w),x,y). R(R(u,x,y),z,w) = R(R(u,z,w),x,y). ********* AIM Goals ********* % Q/N(Q) is commutative a(K(x,y),z,u) = 1 # label("aK1"). a(x,K(y,z),u) = 1 # label("aK2"). a(x,y,K(z,u)) = 1 # label("aK3"). % Q/C(Q) is a group K(a(x,y,z),u) = 1 # label("Ka"). % Q/N(Q) is a group a(a(x,y,z),u,w) = 1 # label("aa1"). a(x,a(y,z,u),w) = 1 # label("aa2"). a(x,y,a(z,u,w)) = 1 # label("aa3"). sometimes: % Q/C(Q) is commutative K(K(x,y),z) = 1 # label("KK"). *************************************************************** Some cases where the result was already known (as of ADAM 2009) *************************************************************** % Moufang (these are equivalent identities) ((x * y) * x) * z = x * (y * (x * z)). ((x * y) * z) * y = x * (y * (z * y)). (x * y) * (z * x) = x * ((y * z) * x). % A-loop (better results hold in this case) L(x,y,z) * L(u,y,z) = L(x * u,y,z). R(x,y,z) * R(u,y,z) = R(x * u,y,z). T(x,y) * T(z,y) = T(x * z,y). % Left conjugacy closed (better results hold in this case) ((x * y) / x) * (x * z) = x * (y * z). % Right conjugacy closed (better results hold in this case) (x * y) * (y \ (z * y)) = (x * z) * y. ************************** Some Varieties of Interest ************************** We have Prover9 proofs for several of these. % Moufang (equivalent in all loops) ((x * y) * x) * z = x * (y * (x * z)) # label("left Moufang"). ((x * y) * z) * y = x * (y * (z * y)) # label("right Moufang"). (x * y) * (z * x) = x * ((y * z) * x) # label("middle Moufang"). % A-loop (left and right are dependent on the other two in all loops) L(x,y,z) * L(u,y,z) = L(x * u,y,z) # label("left A-loop"). R(x,y,z) * R(u,y,z) = R(x * u,y,z) # label("right A-loop"). T(x,y) * T(z,y) = T(x * z,y) # label("middle A-loop"). % Conjugacy Closed ((x * y) / x) * (x * z) = x * (y * z) # label("LCC"). (x * y) * (y \ (z * y)) = (x * z) * y # label("RCC"). % LC ((x * x) * y) * z = x * (x * (y * z)) # label("LC"). % Bol (left + right => Moufang) (x * (y * x)) * z = x * (y * (x * z)) # label("left Bol"). ((x * y) * z) * y = x * ((y * z) * y) # label("right Bol"). % Bruck (left/right AIP equivalent in all loops, Bol + AIP => Bruck) (x * y) \ 1 = (x \ 1) * (y \ 1) # label("left AIP"). 1 / (x * y) = (1 / x) * (1 / y) # label("right AIP"). % Steiner x * y = y * x # label("commutativity"). (1 / x) * (x * y) = y # label("LIP"). x * x = 1 # label("exponent 2"). % Buchsteiner x \ ((x * y) * z) = (y * (z * x)) / x # label("Buchsteiner"). % RIF (equivalent in all loops) (x * y) * (z * (x * y)) = ((x * (y * z)) * x) * y # label("RIF1"). ((y * x) * z) * (y * x) = y * (x * ((z * y) * x)) # label("RIF2").