x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").

Last updated: October 23, 2023

Results posted after March 01, 2023

• middle Bol => nilpotency class 3

  From previous results, it suffices to show

     a(x,y,a(z,u,a(w,v5,v6))) = 1   # label("nil3 32, aa3-Nr").
  

  Proof: (in, out, pf, xml)

  Here is the original proof.

• We've known about most of the following 12 lemmas for a while, but they are collected here for convenience.

     a(x \ 1,y,z \ 1) = a(x,y,z)  # label("mbol lem01").
     a(x \ 1,y,z) = a(x,y,z \ 1)  # label("mbol lem02").
     a(x,y \ 1,z) = a(x,y,z) \ 1  # label("mbol lem03").
     a(x,y \ 1,z) = a(z,y,x)      # label("mbol lem04").
     a(x,y,z \ 1) = a(z,y,x)      # label("mbol lem05").
   
     a(x,y,z) * a(z,y,x) = 1      # label("mbol lem06").
     a(x,y,z * x) = a(x,y,z)      # label("mbol lem07").
     a(x * y,z,x) = a(y,z,x)      # label("mbol lem08").
     a(x,y,a(z,u * u,w)) = a(x,y,a(z,w,u))                # label("mbol lem09").
     a(x,y,a(z,u,w * w)) = a(x,y,a(z,w,u))                # label("mbol lem10").
     a(x,y,a(z,u,w * (w * (w * w)))) = a(x,y,a(z,u,w))    # label("mbol lem11").
     a(x,y,a(z,u * (u * (u * u)),w)) = a(x,y,a(z,u,w))    # label("mbol lem12").
  

  Proof: (in, out, pf, xml)

• middle Bol + Commutativity => nilpotency class 3

  Proof: (in, out, pf, xml)

• middle Bol => a squared 1 and 3

     a(x,y,z) * a(x,y,z) = a(x * x,y,z) # label("a squared 1").
     a(x,y,z) * a(x,y,z) = a(x,y,z * z) # label("a squared 3").
  

  Proof: (in, out, pf, xml)

• This is not a new result. It (or things that trivially imply it) appear as intermediate steps in other posted proofs. I'm not sure if we have already posted a variation as a standalone result.

     L(x,y,z) = x * a(x,y,z) # label("mbol_L2a").
     R(x,y,z) = x * a(x,y,z) # label("mbol_R2a").
  

  Proof: (in, out, pf, xml)

• A stronger version of the result for R ...

     a(a(x,y,z),x,w) = 1 # label("aa1{x1/x4}").
  

  suffices to prove

     R(x,y,z) = x * a(x,y,z) # label("Rxa").
  

  That is, without assuming middle Bol or aK1.

  Proof: (in, out, pf, xml)

Results posted after November 01, 2022

I am working on bringing this section up to date ...

• Here are two lemmas that Michael suggests might be helpful.

     ((x / (u \ y)) \ (x / y)) * ((x / (v \ y)) \ (x / y)) = (x / ((v * u) \ y)) \ (x / y) # label("mbol_lem1").
  
     ((x \ y) / ((x / v) \ y)) * ((x \ y) / ((x / u) \ y)) = (x \ y) / ((x / (u * v)) \ y) # label("mbol_lem2").
  

  Proof of mbol_lem1: (in, out, pf, xml)

  Proof of mbol_lem2: (in, out, pf, xml)

• aa1_sq4 => nilpotency class 3

     a(a(x,y,z),u * u,w) = 1 # label("aa1_sq4").
  

  From previous results, it suffices to prove nil3 24.

  aa1sq4_to_nil3.out

  aa1sq4_to_nil3.pf

• Any one of nil3 24-32 => nilpotency class 3.

  We already have that nil3 24 suffices (in, out, pf, xml), so to confirm the others, it suffices to prove nil3 24. The following proofs include the 4 aK (single a) goals as assumptions, which are lemmas when middle Bol is assumed.

  Proof of nil3 25: (in, out, pf, xml)

  Proof of nil3 26: (in, out, pf, xml)

  Proof of nil3 27: (in, out, pf, xml)

  Proof of nil3 28: (in, out, pf, xml)

  Proof of nil3 29: (in, out, pf, xml)

  Proof of nil3 30: (in, out, pf, xml)

  Proof of nil3 31: (in, out, pf, xml)

  Proof of nil3 32: (in, out, pf, xml)

• 180 even permutations of aai_eq_aaj (i < j)

  Below we show the result (for the 120 even permutations of aa1_eq_aa3 and aa2_eq_aa3, which suffices) when assuming the 32 nil3 clauses. Michael has the result without the nil3 assumptions.

Results posted after July 23, 2022

In the followng, "rsv-instances" refers to instances formed by renaming a single variable.

• Middle Bol => all 10 rsv-instances of aa1

  Proof: (in, out, pf, xml)

  This is a single proof of the conjunction of the 10 goals.

• Middle Bol + 10 rsv-instances of aa1 => all 10 rsv-instances of aa2

  Proof: (in, out, pf, xml)

  This is a single proof of the conjunction of the 10 goals.

• Middle Bol + 10 rsv-instances of aa1 => all 10 rsv-instances of aa3

  Proof: (in, out, pf, xml)

  This is a single proof of the conjunction of the 10 goals.

• Middle Bol => all 30 rsv-instances of the aa goals

  Proof: (in, out, pf, xml)

  This is a single proof of the conjunction of the 30 goals.

Results posted through July 23, 2022

• aK1

        status : proved with no lemmas
        

  aK1.pf

• all 30 instances of the 3 aa goals by renaming a single variable

        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)

  Sfdf derivations from axioms of some of the 30 instances:

  aa1{x1/x2}: (in, out, pf, xml)

  aa1{x1/x4}: (in, out, pf, xml)

  aa1{x1/x5}: (in, out, pf, xml)

  aa2{x1/x2}: (in, out, pf, xml)

  aa3{x1/x2}: (in, out, pf, xml)

  aa3{x1/x5}: (in, out, pf, xml)

  aa3{x4/x5}: (in, out, pf, xml)

• permutations of aa3 in aa1_eq_aa3 and aa2_eq_aa3

        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.

• permutations of the aa goals

        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

  Note that 120aaeq.sos depends on both middle Bol and nil3.

• nilpotency class 3

  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)

Some remaining challenges

• Prove any of 120/240 missing permutations of aa1_eq_aa3 and aa2_eq_aa3

• Prove any of 180/360 missing permutations of the 3 aa goals.

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)").