x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
November 2021
status : proved with no lemmas
aK1.pf
status : proved with lemmas lemmas : 4 single-a goals posted AIM lemmas cb100 lemmas
30instances.goals
30instances.pf_1 (large file)
Eliminating the cb100 lemmas,
status : proved with lemmas lemmas : 4 single-a goals posted AIM lemmas
30instances.pf_2 (large file)
status : 120/240 proved with lemmas (60/120 permutations of each) lemmas : 4 single-a goals nil3 clauses instances of the aa goals by renaming a single variable posted AIM lemmas cb100 lemmas
120aaeq.goals
120aaeq.pf (large file)Note that the aa1_eq_aa2 case is implied.
status : proved 180 with lemmas (60/120 permutations of each) lemmas : permutations of aa1_eq_aa3 and aa2_eq_aa3
120aaeq.sos
180aaperms.goals
180aaperms.pf
The current status is that there is a high-level mathematical argument that AIM loops are nilpotent of class 3, but we do not yet have a Prover9 proof. An intermediate goal is to prove it assuming middle Bol as an extra assumption.
We know from posted lemmas that middle Bol => the 23/32 nil3 clauses having at least one occurrence of K. It remains to prove the 9/32 having 0 occurrences of K.
Here is a proof that it suffices to prove just one of the 9, for example,
a(a(a(x,y,z),u,w),v5,v6) = 1 # label("nil3 24, aa1-Nl").Proof: (in, out, pf, xml)
Here, for example, are the 60/120 missing permutations of aa1_eq_aa3.
Note that assuming, for example, the single clause
a(a(x,y,z),u,w) = a(x,y,a(z,w,u)) # label("aa1_eq_aa3 (12354)").suffices to prove the remaining 59/60. It also suffices to prove all 360 aa permutations.