February 2022

formulas(assumptions). % 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 (right associated * a = left associated) (x * (y * z)) \ ((x * y) * z) = a(x,y,z) # label("associator"). % commutator ( (x * y) * K(y,x) = y * x ) (x * y) \ (y * x) = K(y,x) # label("commutator"). % inner mappings (y * x) \ (y * (x * u)) = L(u,x,y). ((u * x) * y) / (x * y) = R(u,x,y). x \ (u * x) = T(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). end_of_list.

AIM loops are nilpotent of class 3.

Status:

- Proved with a high-level mathematical argument.
- Challenge: Prove with Prover9.
- Status of 32 goals sufficient to prove
that AIM loops are nilpotent of class 3.
- the 8 having > 1 occurrence of K are lemmas
(in, out, pf, xml)

- nil3 15 => the remaining 14 of 15 having exactly 1 occurrence of K
(in, out, pf, xml)

- aK1 + nil3 24 => the remaining 8/32 nil3 clauses having 0 occurrences of K.
(in, out, pf, xml)

- Since aK1 trivially => nil3 15, it follows that aK1 + nil3 24 => nilpotency class 3.

formulas(goals). % aK (or "single-a") goals K(a(x,y,z),u) = 1 # label("Ka"). 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"). % aa (or "double-a") goals 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"). end_of_list.

- The 4 goals are equivalent.
- Proved for several special cases.
- Equality relationships between the single-a goal terms

- The 3 goals are equivalent.
- Proved for several special cases.
- Example next step challenge: middle Bol + KK => aa1.
x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol"). K(K(x,y),z) = 1 # label("KK").

- Another example challenge: AIM => any aai_eq_aaj.
- Results assuming middle Bol as an extra assumption