Comments about the main index page (AIM_REDONE)
-----------------------------------------------

Disclaimer

   The index page is a working document for ourselves (mostly to store results
   in one place so we don't lose track of them).  It was never intended to be
   a presentation of the material for others. Some consequences ...

       The results are not in chronological order.

       Some later results subsume several earlier results, but the earlier
       results remain posted.

       Naming conventions are ad hoc and probably inconsistent.  For example,
       aK1 sometimes refers to the goal clause

          a(K(x,y),z,u) = 1     # label("aK1").

       and sometimes just to the left side term

          a(K(x,y),z,u).

       We sometimes refer to the aKi/aai goals, sometimes to the
       single-a/double-a goals and sometimes to the a/aa goals.

Rough map of the page

   Recognizing rather late in the project that some people might look at
   the page besides us, we added some introductory/overview material at
   the beginning.

   The next sections include several properties (all assuming AIM) of
   the 7 primary goals (goals of the main conjecture), the operators
   {a,K,T,L,R} and the 32 nilpotency class 3 goals.  

   Section "The Conjecture" includes proofs of primary goal aK1 or both
   primary goals aK1 and aa1 for various special cases.  Some of these 
   special case are of interest to the mathematicians; some are just 
   syntactic constructs that might be useful lemmas.  It is important to
   note that posted results show that proving both goals aK1 and aa1
   suffices to prove all 7 goals of the main conjecture. 

   Section "Miscellanious Results" includes several properties of 
   interest and several that give alternative sufficient conditions for
   proving results of interest.  For one example, a single permutation
   of primary goal aa1,

      a(a(x,y,z),u,w) = a(a(x,y,z),w,u) # label("aa1_45"). 

   suffices to prove all 32 of the nilpotency class 3 conditions, and
   therefore suffices to prove nilpotency class 3.  Another significant
   result with aa1_45 is 

      aa1_45 + aK1 => aa1

   and therefore gives another sufficient condition for proving the strong
   conjecture.

Finally, note that there are two associated pages of interest.

   AIM_REDONE/AKEQ includes several results relating the aKi goals.

   AIM_REDONE/MBOL includes several results dependent on middle Bol

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

   which is a property of special interest.