In[]:=
ggg=%229;
In[]:=
Select[VertexList[ggg],VertexInDegree[ggg,#]==0&]
Out[]=
{a.a.,a.((b.·c.)·a.)·(b.·((b.·a.)·b.)),a.·a.a.·a.,(c.·(c.·c.))·(a.·(c.·b.))(c.·(c.·c.))·(a.·(c.·b.))}
In[]:=
VertexOutComponentGraph[ggg,a.((b.·c.)·a.)·(b.·((b.·a.)·b.)),6,AspectRatio->12,VertexLabels->{x_HoldForm:>FormatLemma[x]/;LeafCount[x]<20}]
Out[]=
In[]:=
VertexOutComponentGraph[ggg,a.((b.·c.)·a.)·(b.·((b.·a.)·b.)),2,AspectRatio->12,VertexLabels->{x_HoldForm:>FormatLemma[x]/;LeafCount[x]<20}]
Out[]=
In[]:=
TakeLargestBy[VertexList[ggg,_HoldForm],VertexInDegree[ggg,#]&,10]//Column
Out[]=
(a.·a.)·(a.·a.)a.
a.·(b.·(b.·b.))a.·a.
a.·a.a.·((a.·a.)·a.)
a.·b.a.·((a.·b.)·a.)
a.(a.·a.)·(a.·b.)
a.(a.·a.)·(b.·(b.·(a.·c.)))
a.(a.·a.)·(b.·(b.·(c.·a.)))
a.(a.·a.)·(b.·(b.·(c.·(c.·(a.·c.)))))
a.(a.·a.)·(b.·((a.·c.)·b.))
a.(a.·a.)·(b.·((b.·a.)·b.))
In[]:=
TakeLargestBy[VertexList[ggg,_HoldForm],VertexOutDegree[ggg,#]&,10]//Column
Out[]=
a.·b.b.·a.
a.((b.·c.)·a.)·(b.·((b.·a.)·b.))
a.·(b.·(c.·α.))((α.·c.)·b.)·a.
a.·b.a.·((a.·b.)·a.)
(a.·b.)·c.c.·(b.·a.)
(a.·(b.·c.))·α.α.·((c.·b.)·a.)
a.·(b.·c.)a.·(c.·(a.·(a.·b.)))
a.(b.·a.)·((c.·b.)·(((c.·b.)·a.)·(c.·b.)))
a.·(b.·a.)a.·(b.·b.)
a.·(b.·a.)(b.·b.)·a.
​
What are traditional mathematical names for these theorems of equational logic?
a.·b.b.·a.
a.((b.·c.)·a.)·(b.·((b.·a.)·b.))
a.·(b.·(c.·α.))((α.·c.)·b.)·a.
a.·b.a.·((a.·b.)·a.)
(a.·b.)·c.c.·(b.·a.)
(a.·(b.·c.))·α.α.·((c.·b.)·a.)
a.·(b.·c.)a.·(c.·(a.·(a.·b.)))
a.(b.·a.)·((c.·b.)·(((c.·b.)·a.)·(c.·b.)))
a.·(b.·a.)a.·(b.·b.)
a.·(b.·a.)(b.·b.)·a.
The equations you provided appear to represent identities or theorems in algebraic structures, such as semigroups or monoids. Here are some traditional interpretations:​1. Commutativity: ​
•
a·bb·a
​​
• This is the commutative property, where the order of multiplication does not change the result.
​2. Associativity: ​
•
(a·b)·ca·(b·c)
​​
• This is the associative property, where the grouping of operations does not affect the result.
​3. Identity Element: ​
•
a·1a
​​
• This represents the identity element in a monoid, where multiplying by the identity leaves the element unchanged.
​4. Distributivity: ​
• If applicable in context, the distributive property could be inferred if there were expressions involving addition and multiplication.
​5. Idempotence: ​
•
a·aa
​​
• This property indicates that applying the operation to an element multiple times does not change the result beyond the first application.
​6. Inverse Element: ​
•
a·
-1
a
1
​​
• This involves the inverse element, where multiplication with its inverse yields the identity.
​These interpretations depend on the context and the algebraic structure being modeled. If these are part of a specific algebraic system, such as a ring or group, the meanings might vary accordingly.
In[]:=
TextMulticolumnTraditionalForm/@DeleteCasesCasesValuesNormalProofObject
Logic: EquationalLogic
Steps: 508
Theorems:
∀
a.
(a.·a.)·(a.·a.)a.…
["ProofDataset"][All,"Statement"],HoldForm[_==_],HoldForm[x_==x_],4
Out[]=
a.((b.·c.)·a.)·(b.·((b.·a.)·b.))
a.·b.b.·((a.·b.)·((a.·b.)·a.))
a.·a.a.·((a.·(b.·(b.·c.)))·c.)
a.·((a.·(b.·b.))·c.)a.·((((α.·(α.·α.))·b.)·(b.·b.))·c.)
((b.·b.)·a.)·((c.·c.)·a.)(a.·(b.·c.))·(a.·(b.·c.))
a.·b.b.·((a.·b.)·(a.·(a.·b.)))
a.·a.a.·(b.·(a.·(c.·(c.·b.))))
a.·((a.·(b.·b.))·c.)a.·(b.·c.)
(a.·a.)·(a.·a.)a.
a.·b.b.·a.
a.·a.a.·(b.·(b.·(c.·(a.·c.))))
a.·(b.·c.)a.·(c.·(a.·(b.·b.)))
a.·(b.·(b.·b.))a.·a.
(a.·b.)·((c.·a.)·b.)((c.·a.)·b.)·((α.·(a.·b.))·b.)
a.·(b.·(c.·(c.·a.)))a.·(b.·b.)
a.·((b.·(c.·(a.·c.)))·α.)a.·(α.·(a.·(a.·(a.·b.))))
a.·((a.·b.)·a.)b.·((a.·c.)·(((a.·c.)·(a.·((a.·b.)·a.)))·(a.·c.)))
a.((b.·c.)·a.)·((α.·(c.·a.))·a.)
a.·a.a.·((b.·((b.·a.)·c.))·b.)
a.·((b.·(c.·(a.·c.)))·α.)a.·((a.·b.)·α.)
a.(b.·a.)·(((c.·α.)·b.)·((((c.·α.)·b.)·a.)·((c.·α.)·b.)))
(a.·b.)·(b.·(c.·(a.·b.)))(b.·(c.·(a.·b.)))·(b.·(c.·(a.·b.)))
a.·a.a.·((b.·((a.·b.)·c.))·b.)
a.·((b.·((a.·b.)·c.))·α.)a.·(α.·(a.·(a.·(b.·b.))))
a.(((b.·((b.·a.)·b.))·c.)·a.)·((b.·((b.·a.)·b.))·a.)
a.·b.b.·((c.·a.)·(b.·a.))
a.·a.a.·((b.·(c.·(a.·b.)))·b.)
a.·((b.·((a.·b.)·c.))·α.)a.·((b.·b.)·α.)
a.((b.·((b.·c.)·b.))·a.)·(c.·(((((b.·α.)·c.)·(b.·((b.·c.)·b.)))·a.)·(((b.·α.)·c.)·(b.·((b.·c.)·b.)))))
a.(a.·b.)·((b.·c.)·a.)
(a.·a.)·(a.·a.)(a.·a.)·(b.·(b.·(c.·a.)))
a.·((b.·(a.·(b.·c.)))·α.)a.·(α.·(a.·(a.·(b.·c.))))
a.((b.·((b.·c.)·b.))·a.)·(c.·((c.·a.)·(((b.·α.)·c.)·(b.·((b.·c.)·b.)))))
a.(b.·a.)·(a.·(b.·c.))
a.(a.·a.)·(b.·(b.·(c.·a.)))
a.·((b.·(a.·(b.·c.)))·α.)a.·((b.·c.)·α.)
a.((b.·((b.·c.)·b.))·a.)·(c.·((c.·a.)·c.))
a.(a.·b.)·((c.·b.)·a.)
(a.·a.)·(a.·a.)(a.·a.)·(b.·(b.·(c.·(c.·(a.·c.)))))
a.·(((b.·c.)·(a.·b.))·α.)a.·(α.·(a.·(a.·b.)))
a.(b.·a.)·((c.·b.)·((((((α.·β.)·c.)·(α.·((α.·c.)·α.)))·b.)·a.)·((((α.·β.)·c.)·(α.·((α.·c.)·α.)))·b.)))
a.(b.·a.)·(a.·(c.·b.))
a.(a.·a.)·(b.·(b.·(c.·(c.·(a.·c.)))))
a.·(((b.·c.)·(a.·b.))·α.)a.·(b.·α.)
a.(b.·a.)·((c.·b.)·(((c.·b.)·a.)·((((α.·β.)·c.)·(α.·((α.·c.)·α.)))·b.)))
a.(a.·b.)·(a.·(b.·c.))
a.(a.·a.)·(b.·(b.·(a.·c.)))
a.·(b.·(b.·c.))a.·(b.·(c.·a.))
a.(b.·a.)·((c.·b.)·(((c.·b.)·a.)·(c.·b.)))
a.·b.b.·((a.·b.)·((b.·b.)·c.))
a.(a.·a.)·(b.·((c.·a.)·b.))
a.·((((b.·b.)·a.)·c.)·α.)a.·(α.·(a.·(a.·(b.·c.))))
a.(((b.·((b.·c.)·b.))·c.)·a.)·(c.·((c.·a.)·c.))
a.·b.((b.·c.)·(a.·b.))·a.
a.·(a.·(b.·c.))((a.·(a.·(b.·c.)))·c.)·c.
a.·((((b.·b.)·a.)·c.)·α.)a.·((b.·c.)·α.)
a.·((a.·b.)·a.)b.·((c.·((c.·a.)·c.))·(((c.·((c.·a.)·c.))·(a.·((a.·b.)·a.)))·(c.·((c.·a.)·c.))))
a.·(b.·c.)((a.·(b.·c.))·b.)·a.
a.(a.·a.)·(b.·((a.·c.)·b.))
a.·(((b.·c.)·(b.·a.))·α.)a.·((a.·(b.·a.))·α.)
a.·((a.·b.)·a.)(b.·(a.·((a.·b.)·a.)))·(((a.·c.)·b.)·(b.·((a.·c.)·b.)))
(a.·b.)·(b.·(a.·c.))(b.·(a.·c.))·((α.·(a.·b.))·b.)
a.·((b.·c.)·a.)((a.·((b.·c.)·a.))·c.)·c.
a.·(((b.·c.)·(b.·a.))·α.)a.·(b.·α.)
a.·((a.·b.)·a.)(b.·(a.·((a.·b.)·a.)))·(((c.·((c.·a.)·c.))·b.)·(b.·((c.·((c.·a.)·c.))·b.)))
a.(a.·(b.·c.))·((α.·(b.·a.))·a.)
a.((b.·((c.·α.)·b.))·a.)·(c.·a.)
(a.·(a.·b.))·c.c.·(a.·(b.·c.))
(a.·b.)·(((a.·b.)·c.)·(a.·b.))c.·(b.·((b.·((a.·b.)·(((a.·b.)·c.)·(a.·b.))))·b.))
a.(a.·b.)·(a.·(c.·b.))
a.·a.a.·(b.·(b.·((b.·a.)·c.)))
a.·(((a.·(b.·b.))·c.)·α.)a.·((a.·(a.·(b.·c.)))·α.)
(a.·b.)·(((a.·b.)·c.)·(a.·b.))(((b.·c.)·α.)·((a.·b.)·(((a.·b.)·c.)·(a.·b.))))·((b.·c.)·(c.·(b.·c.)))
a.·b.b.·((a.·b.)·(c.·(b.·b.)))
a.·a.a.·(b.·(b.·((a.·b.)·c.)))
a.·(((a.·(b.·b.))·c.)·α.)a.·((b.·c.)·α.)
(a.·b.)·(((a.·b.)·((b.·c.)·b.))·(a.·b.))((b.·c.)·b.)·(c.·((c.·((a.·b.)·(((a.·b.)·((b.·c.)·b.))·(a.·b.))))·c.))
a.·b.a.·((a.·b.)·(c.·(a.·a.)))
a.·a.a.·(b.·(b.·(c.·(a.·b.))))
a.·(b.·(a.·(c.·c.)))a.·(c.·((b.·α.)·(a.·b.)))
(a.·b.)·(((a.·b.)·c.)·(a.·b.))(c.·((a.·b.)·(((a.·b.)·c.)·(a.·b.))))·((b.·c.)·(c.·(b.·c.)))
a.·(b.·c.)((a.·(b.·c.))·c.)·a.
((a.·b.)·(a.·b.))·((b.·b.)·c.)(α.·(α.·α.))·((a.·b.)·(a.·b.))
a.·(b.·c.)a.·(b.·((c.·α.)·(a.·c.)))
a.·((a.·b.)·a.)b.·(b.·((b.·(a.·((a.·b.)·a.)))·b.))
(a.·b.)·(b.·(c.·a.))(b.·(c.·a.))·((α.·(a.·b.))·b.)
((a.·b.)·(a.·b.))·((b.·b.)·c.)a.·b.
a.·(b.·((c.·c.)·a.))(((b.·α.)·(a.·b.))·c.)·a.
(a.·((a.·b.)·a.))·b.b.·(b.·((b.·((a.·((a.·b.)·a.))·b.))·b.))
a.(a.·(b.·c.))·((α.·(c.·a.))·a.)
((a.·b.)·(a.·b.))·(c.·(a.·a.))(α.·(α.·α.))·((a.·b.)·(a.·b.))
(a.·b.)·c.(((a.·α.)·(c.·a.))·b.)·c.
(a.·b.)·(((a.·b.)·c.)·(a.·b.))(((α.·((α.·(b.·c.))·α.))·(b.·c.))·((a.·b.)·(((a.·b.)·c.)·(a.·b.))))·((b.·c.)·(c.·(b.·c.)))
a.·(b.·c.)a.·(((c.·a.)·α.)·(a.·(b.·c.)))
((a.·b.)·(a.·b.))·(c.·(a.·a.))a.·b.
a.·(b.·c.)a.·(c.·((a.·b.)·c.))
a.·((a.·b.)·a.)b.·(((c.·((c.·a.)·c.))·a.)·((((c.·((c.·a.)·c.))·a.)·(a.·((a.·b.)·a.)))·((c.·((c.·a.)·c.))·a.)))
a.·b.((a.·b.)·(b.·c.))·a.
a.(a.·(b.·(c.·α.)))·((α.·c.)·a.)
a.·(b.·c.)a.·(c.·(c.·(a.·b.)))
(a.·b.)·(((a.·b.)·(a.·((a.·((a.·b.)·c.))·a.)))·(a.·b.))(a.·((a.·((a.·b.)·c.))·a.))·(((a.·b.)·c.)·((a.·((a.·((a.·b.)·c.))·a.))·((a.·b.)·c.)))
a.·b.((a.·b.)·(c.·b.))·a.
(a.·(b.·c.))·((α.·(b.·b.))·a.)((α.·(b.·b.))·a.)·((b.·c.)·a.)
a.·(b.·((a.·c.)·b.))a.·(((a.·c.)·b.)·b.)
a.·((a.·a.)·a.)(a.·(a.·((a.·a.)·a.)))·a.
(a.·b.)·(a.·(b.·c.))(a.·(b.·c.))·((α.·(a.·b.))·a.)
a.((b.·(c.·c.))·a.)·((c.·α.)·a.)
a.·(b.·c.)a.·(((a.·b.)·c.)·c.)
((a.·b.)·c.)·(c.·((a.·b.)·c.))(a.·((a.·c.)·a.))·(c.·((c.·(((a.·b.)·c.)·(c.·((a.·b.)·c.))))·c.))
a.(a.·(b.·c.))·((α.·(a.·b.))·a.)
a.(b.·a.)·((c.·((b.·α.)·c.))·a.)
(a.·a.)·(b.·((a.·c.)·b.))(b.·((a.·c.)·b.))·(a.·(c.·b.))
a.(a.·((a.·a.)·a.))·(a.·((a.·a.)·a.))
(a.·b.)·(b.·((a.·b.)·c.))(b.·((a.·b.)·c.))·(b.·((a.·b.)·c.))
a.((b.·c.)·a.)·(a.·(α.·(c.·b.)))
a.(b.·((a.·c.)·b.))·(a.·(c.·b.))
a.((b.·(b.·((b.·b.)·b.)))·a.)·((b.·((b.·b.)·b.))·(((b.·((b.·b.)·b.))·a.)·(b.·((b.·b.)·b.))))
(a.·b.)·((b.·c.)·a.)((b.·c.)·a.)·(((a.·b.)·α.)·a.)
a.·(a.·((b.·c.)·(c.·b.)))(c.·b.)·a.
a.·(a.·(b.·c.))c.·((b.·a.)·c.)
a.·((a.·a.)·a.)(a.·(a.·((a.·a.)·a.)))·((a.·((a.·a.)·a.))·(a.·((a.·(a.·((a.·a.)·a.)))·a.)))
a.((b.·c.)·a.)·(((a.·b.)·α.)·a.)
(a.·b.)·c.c.·(((b.·a.)·(a.·b.))·c.)
a.·(b.·c.)a.·(c.·(c.·(b.·a.)))
a.·((a.·a.)·a.)(a.·(a.·((a.·a.)·a.)))·((a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.))))
(a.·b.)·(b.·(a.·c.))(b.·(a.·c.))·(((a.·b.)·α.)·b.)
(a.·b.)·c.c.·(((b.·a.)·(b.·a.))·c.)
a.·(b.·c.)a.·(c.·((α.·(α.·α.))·(b.·a.)))
a.·((a.·a.)·a.)(((a.·((a.·a.)·a.))·b.)·(a.·((a.·a.)·a.)))·((a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.))))
a.(a.·(b.·c.))·(((b.·a.)·α.)·a.)
(a.·b.)·c.c.·(b.·a.)
a.·(b.·(c.·α.))a.·(b.·(c.·(a.·(c.·α.))))
a.·((a.·a.)·a.)(((a.·a.)·a.)·(a.·((a.·a.)·a.)))·((a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.))))
(a.·b.)·(a.·(b.·c.))(a.·(b.·c.))·(((a.·b.)·α.)·a.)
a.·((b.·(b.·b.))·c.)(c.·c.)·a.
(a.·b.)·c.c.·(b.·((c.·a.)·(a.·α.)))
a.·((a.·a.)·a.)a.·((a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.))))
a.(a.·(b.·c.))·(((a.·b.)·α.)·a.)
a.·((b.·c.)·c.)((b.·b.)·c.)·a.
(a.·a.)·(b.·b.)(b.·b.)·(a.·(b.·(a.·c.)))
(a.·b.)·(((a.·b.)·(a.·((a.·b.)·a.)))·(a.·b.))(a.·((a.·b.)·a.))·(b.·((a.·((a.·b.)·a.))·b.))
(a.·b.)·(a.·(c.·b.))(a.·(c.·b.))·(((a.·b.)·α.)·a.)
a.·((b.·c.)·c.)(c.·(b.·b.))·a.
a.(a.·(b.·c.))·((c.·(a.·b.))·c.)
(a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.)))(a.·((a.·a.)·a.))·(a.·((a.·((a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.)))))·a.))
a.(a.·(b.·c.))·(((a.·c.)·α.)·a.)
a.·(b.·(c.·c.))(b.·(c.·b.))·a.
a.(a.·(b.·c.))·(c.·((b.·a.)·c.))
(a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.)))(a.·((a.·a.)·a.))·(a.·((a.·((a.·a.)·a.))·a.))
a.·b.a.·((b.·c.)·(a.·b.))
(a.·b.)·c.(a.·b.)·((c.·(b.·a.))·(c.·α.))
a.·((b.·c.)·a.)((b.·a.)·(a.·((b.·c.)·a.)))·c.
(a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.)))(a.·a.)·(((a.·a.)·(a.·((a.·a.)·a.)))·(a.·a.))
a.·b.a.·((a.·b.)·(b.·c.))
(a.·(b.·c.))·α.α.·(a.·(c.·b.))
a.·((b.·c.)·a.)((b.·a.)·(b.·a.))·c.
a.·((a.·a.)·a.)((a.·(a.·((a.·a.)·a.)))·(a.·((a.·a.)·a.)))·((a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.))))
a.·b.a.·((a.·b.)·(c.·b.))
(a.·b.)·(c.·α.)(b.·a.)·(α.·c.)
a.·((b.·c.)·a.)c.·((b.·a.)·(a.·b.))
a.·((a.·a.)·a.)a.·(((b.·((b.·a.)·b.))·a.)·(a.·((b.·((b.·a.)·b.))·a.)))
(a.·(b.·a.))·b.b.·b.
((a.·b.)·c.)·α.α.·((b.·a.)·c.)
a.·((b.·c.)·a.)c.·((b.·a.)·(b.·a.))
((a.·((a.·b.)·a.))·b.)·(b.·((a.·((a.·b.)·a.))·b.))(a.·((a.·b.)·a.))·(b.·((b.·((b.·b.)·b.))·b.))
a.·(b.·(a.·b.))a.·a.
a.·b.((b.·a.)·c.)·((a.·b.)·(α.·c.))
a.·((b.·c.)·a.)((b.·a.)·(a.·b.))·c.
a.·((a.·b.)·a.)(b.·(a.·((a.·b.)·a.)))·((a.·((a.·b.)·a.))·(b.·((b.·((b.·b.)·b.))·b.)))
(a.·b.)·(a.·b.)(a.·b.)·((b.·(c.·a.))·b.)
a.·(b.·(c.·(c.·a.)))a.·(a.·b.)
(((a.·b.)·(b.·a.))·c.)·α.α.·(a.·((b.·c.)·a.))
a.·((a.·a.)·a.)a.·((b.·((b.·a.)·b.))·(a.·((a.·((a.·a.)·a.))·a.)))
(a.·b.)·(a.·b.)(a.·b.)·((a.·(b.·c.))·a.)
(a.·a.)·((a.·a.)·((b.·a.)·c.))(a.·a.)·c.
a.·(b.·(a.·c.))a.·((c.·c.)·b.)
a.·((a.·a.)·a.)(a.·(a.·((a.·a.)·a.)))·((b.·((b.·a.)·b.))·(a.·((a.·((a.·a.)·a.))·a.)))
(a.·b.)·(a.·b.)(a.·b.)·((a.·(c.·b.))·a.)
(a.·a.)·((a.·a.)·((a.·b.)·c.))(a.·a.)·c.
a.·(b.·(a.·c.))a.·(b.·(c.·b.))
(a.·((a.·b.)·a.))·(b.·((b.·((b.·b.)·b.))·b.))(b.·((b.·b.)·b.))·(b.·((b.·((a.·((a.·b.)·a.))·(b.·((b.·((b.·b.)·b.))·b.))))·b.))
a.(a.·(b.·(c.·b.)))·((c.·c.)·a.)
a.·(a.·b.)a.·((c.·(c.·a.))·b.)
a.·(b.·(c.·a.))a.·((c.·c.)·b.)
(a.·((a.·b.)·a.))·(b.·((b.·((b.·b.)·b.))·b.))(b.·((b.·b.)·b.))·(b.·((b.·((b.·b.)·b.))·b.))
(a.·b.)·c.c.·(a.·((a.·b.)·c.))
a.·(a.·b.)a.·(b.·((a.·a.)·c.))
(a.·b.)·(c.·(c.·b.))(a.·b.)·(c.·((c.·a.)·b.))
(a.·((a.·b.)·a.))·(b.·((b.·((b.·b.)·b.))·b.))(b.·b.)·(((b.·b.)·(b.·((b.·b.)·b.)))·(b.·b.))
a.·(b.·c.)a.·((a.·(b.·c.))·b.)
a.·(a.·b.)a.·(b.·(c.·(a.·c.)))
(a.·b.)·((c.·c.)·b.)(a.·b.)·(b.·(c.·(c.·a.)))
(a.·((a.·b.)·a.))·(b.·((b.·((b.·b.)·b.))·b.))(b.·((b.·b.)·b.))·(b.·(b.·((b.·b.)·b.)))
a.·(b.·c.)a.·(b.·(a.·(b.·c.)))
a.·(b.·(b.·c.))((c.·c.)·b.)·a.
a.·((a.·b.)·c.)a.·(c.·(b.·((a.·α.)·α.)))
a.·((a.·b.)·a.)(b.·(a.·((a.·b.)·a.)))·((b.·((b.·b.)·b.))·(b.·(b.·((b.·b.)·b.))))
a.·(b.·a.)a.·(b.·b.)
a.·(b.·(b.·c.))(b.·(c.·c.))·a.
a.·((b.·b.)·((c.·c.)·a.))((b.·((a.·b.)·α.))·c.)·a.
(a.·b.)·(((a.·b.)·(b.·((b.·b.)·b.)))·(a.·b.))(((b.·(b.·((b.·b.)·b.)))·c.)·((a.·b.)·(((a.·b.)·(b.·((b.·b.)·b.)))·(a.·b.))))·(b.·((b.·b.)·b.))
a.·(b.·b.)a.·(a.·b.)
a.·(b.·(c.·α.))((α.·c.)·b.)·a.
((a.·a.)·b.)·c.((a.·((c.·a.)·α.))·b.)·c.
(a.·b.)·(((a.·b.)·(b.·((b.·b.)·b.)))·(a.·b.))((b.·((b.·b.)·b.))·((a.·b.)·(((a.·b.)·(b.·((b.·b.)·b.)))·(a.·b.))))·(b.·((b.·b.)·b.))
a.·b.b.·(b.·(a.·a.))
(a.·(b.·c.))·α.α.·((c.·b.)·a.)
(a.·b.)·((a.·c.)·((b.·α.)·a.))(a.·b.)·a.
a.·((a.·a.)·a.)((b.·a.)·(((b.·a.)·(a.·((a.·a.)·a.)))·(b.·a.)))·((a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.))))
a.(a.·(b.·c.))·(a.·(c.·(b.·b.)))
(a.·b.)·(c.·α.)(α.·c.)·(b.·a.)
a.·((b.·c.)·α.)a.·(α.·(c.·(a.·(b.·b.))))
a.·((a.·a.)·a.)((a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.))))·((a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.))))
a.·(b.·a.)(b.·b.)·a.
(a.·b.)·(a.·b.)(a.·b.)·(b.·((a.·c.)·b.))
a.·((b.·c.)·α.)a.·(α.·((a.·(b.·b.))·c.))
(a.·b.)·(((a.·b.)·(a.·((a.·((a.·b.)·c.))·a.)))·(a.·b.))(a.·((a.·b.)·c.))·(((a.·((a.·b.)·c.))·(a.·((a.·((a.·b.)·c.))·a.)))·(a.·((a.·b.)·c.)))
a.·((b.·b.)·a.)a.·b.
(a.·b.)·(a.·b.)(a.·b.)·(a.·((c.·b.)·a.))
((a.·b.)·(a.·b.))·(c.·c.)(c.·c.)·((a.·b.)·(c.·b.))
(a.·a.)·(((a.·a.)·(a.·((a.·a.)·a.)))·(a.·a.))(((a.·(a.·((a.·a.)·a.)))·b.)·((a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.)))))·(a.·((a.·a.)·a.))
(a.·a.)·b.b.·(b.·a.)
(a.·b.)·(a.·b.)(a.·b.)·(a.·((b.·c.)·a.))
a.·((b.·(c.·c.))·a.)(c.·c.)·((b.·a.)·(c.·a.))
(a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.)))(((a.·(a.·((a.·a.)·a.)))·b.)·((a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.)))))·(a.·((a.·a.)·a.))
a.(a.·(b.·c.))·(a.·((b.·b.)·c.))
a.·(a.·(b.·c.))c.·(c.·((a.·(b.·c.))·a.))
a.·((a.·b.)·c.)a.·(c.·(b.·(α.·(α.·a.))))
(a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.)))(a.·((a.·a.)·a.))·(a.·((a.·a.)·a.))
a.((b.·c.)·a.)·(a.·((b.·b.)·c.))
a.·(a.·(b.·c.))c.·(c.·(a.·((c.·b.)·a.)))
((a.·a.)·b.)·c.c.·(b.·(((c.·a.)·α.)·a.))
(a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.)))a.
a.(a.·(b.·c.))·(((b.·b.)·c.)·a.)
a.·(a.·b.)a.·(b.·(c.·(c.·(α.·(a.·a.)))))
((a.·a.)·b.)·c.c.·(b.·(a.·(α.·(a.·c.))))
a.·((a.·((a.·a.)·a.))·(a.·(a.·((a.·a.)·a.))))a.·((a.·a.)·a.)
a.·(b.·c.)a.·((a.·(b.·c.))·c.)
a.·((b.·c.)·a.)c.·(c.·(((b.·c.)·a.)·a.))
(a.·(a.·b.))·(c.·a.)(a.·(b.·(c.·a.)))·(a.·(b.·(c.·a.)))
a.·a.a.·((a.·a.)·a.)
a.·(b.·c.)a.·(c.·(a.·(b.·c.)))
a.·((b.·c.)·a.)c.·(c.·(a.·(a.·(c.·b.))))
(a.·(a.·b.))·(c.·a.)(c.·(c.·c.))·((b.·(c.·a.))·a.)
(a.·(b.·((b.·a.)·b.)))·a.b.·((b.·a.)·b.)
a.·b.b.·((c.·(c.·b.))·(a.·b.))
a.·b.((a.·b.)·c.)·((α.·c.)·(b.·a.))
(a.·(a.·b.))·(c.·a.)(c.·(c.·c.))·(a.·((a.·c.)·b.))
a.·a.a.·((a.·a.)·a.)
a.·b.b.·((c.·(b.·c.))·(a.·b.))
(a.·a.)·b.(a.·a.)·((b.·b.)·(c.·a.))
(a.·(a.·b.))·(c.·a.)(c.·a.)·((α.·(α.·α.))·((c.·(c.·c.))·(a.·((a.·c.)·b.))))
(a.·((a.·a.)·a.))·a.a.·(a.·((a.·((a.·a.)·a.))·a.))
a.·b.a.·((c.·(a.·c.))·(a.·b.))
(a.·a.)·b.(a.·a.)·((c.·a.)·((c.·a.)·b.))
(a.·(a.·b.))·(c.·a.)(c.·a.)·(a.·((a.·c.)·b.))
(a.·a.)·a.a.·(a.·((a.·((a.·a.)·a.))·a.))
a.((b.·c.)·a.)·(a.·(α.·(c.·a.)))
a.·(b.·b.)((a.·(b.·b.))·(b.·c.))·(b.·c.)
(a.·a.)·((b.·b.)·c.)(c.·((b.·a.)·b.))·(a.·a.)
(a.·a.)·a.a.·(a.·((a.·a.)·a.))
a.(a.·(b.·(c.·a.)))·((α.·c.)·a.)
((a.·b.)·(b.·(a.·b.)))·(((c.·a.)·(((c.·a.)·b.)·(c.·a.)))·((a.·b.)·(α.·((α.·(a.·b.))·α.))))(c.·a.)·(((c.·a.)·b.)·(c.·a.))
(a.·((b.·c.)·a.))·α.α.·(b.·((a.·c.)·b.))
(a.·a.)·a.a.·(a.·a.)
a.(a.·(b.·c.))·(a.·(α.·(b.·a.)))
(((a.·b.)·(((a.·b.)·c.)·(a.·b.)))·((b.·c.)·(α.·((α.·(b.·c.))·α.))))·((b.·c.)·(c.·c.))(a.·b.)·(((a.·b.)·c.)·(a.·b.))
(a.·(a.·(b.·(c.·(c.·a.)))))·(b.·a.)(c.·(c.·c.))·(a.·((a.·b.)·((c.·c.)·b.)))
(a.·a.)·(a.·((a.·a.)·a.))a.
a.(a.·(b.·(c.·a.)))·(a.·(c.·α.))
((a.·b.)·(b.·b.))·(((a.·b.)·(c.·((c.·(a.·b.))·c.)))·((((α.·a.)·b.)·(α.·a.))·(α.·a.)))(α.·a.)·(((α.·a.)·b.)·(α.·a.))
(a.·((a.·b.)·a.))·(b.·a.)(c.·(c.·c.))·(a.·((a.·b.)·((c.·c.)·b.)))
(a.·a.)·(a.·a.)a.
a.(a.·(b.·c.))·(a.·(α.·(c.·a.)))
a.·(((b.·a.)·(c.·((c.·(b.·a.))·c.)))·((((α.·b.)·a.)·(α.·b.))·(α.·b.)))(α.·b.)·(((α.·b.)·a.)·(α.·b.))
(a.·((a.·b.)·a.))·(b.·a.)(c.·(c.·c.))·(a.·b.)
a.((a.·b.)·a.)·(a.·(a.·(a.·a.)))
a.·b.((a.·b.)·(c.·α.))·((a.·b.)·α.)
a.·(((b.·a.)·(c.·c.))·((((α.·b.)·a.)·(α.·b.))·(α.·b.)))(α.·b.)·(((α.·b.)·a.)·(α.·b.))
(a.·(a.·b.))·(c.·a.)(a.·c.)·(((a.·c.)·b.)·a.)
a.·a.a.·(a.·(a.·a.))
a.(a.·(b.·c.))·(a.·(α.·(a.·b.)))
a.·(((b.·a.)·(c.·c.))·((α.·b.)·((α.·b.)·(a.·(α.·b.)))))(α.·b.)·(((α.·b.)·a.)·(α.·b.))
(a.·(a.·(a.·b.)))·(b.·a.)(a.·((a.·b.)·a.))·(b.·a.)
a.((a.·b.)·a.)·(a.·a.)
a.((b.·c.)·a.)·(a.·((a.·b.)·α.))
a.·(((b.·a.)·(c.·c.))·(a.·(α.·b.)))(α.·b.)·(((α.·b.)·a.)·(α.·b.))
(a.·b.)·(b.·a.)(a.·((a.·b.)·a.))·(b.·a.)
a.·a.(((a.·a.)·b.)·(a.·a.))·a.
a.(a.·((a.·b.)·c.))·((b.·α.)·a.)
a.·(b.·c.)(b.·c.)·(((b.·c.)·a.)·(b.·c.))
(a.·b.)·(b.·a.)(b.·a.)·(a.·((a.·b.)·a.))
a.(b.·((b.·a.)·b.))·(a.·a.)
a.(a.·(b.·c.))·(a.·((b.·a.)·α.))
a.·(b.·c.)(b.·c.)·((b.·c.)·(a.·(c.·b.)))
(a.·b.)·(b.·a.)(b.·a.)·(a.·(a.·a.))
a.·a.(b.·((b.·(a.·a.))·b.))·a.
a.(a.·((b.·a.)·c.))·(a.·(b.·α.))
(a.·a.)·((b.·(a.·c.))·(b.·α.))(a.·a.)·((a.·a.)·((c.·a.)·b.))
a.·((b.·c.)·(c.·(a.·(b.·b.))))a.·(((a.·(b.·b.))·c.)·(c.·(c.·c.)))
a.·(a.·(b.·((b.·a.)·b.)))b.·((b.·a.)·b.)
a.(a.·(b.·c.))·(a.·((a.·b.)·α.))
(a.·a.)·((b.·(a.·c.))·(b.·α.))(a.·a.)·b.
a.·((b.·c.)·(b.·c.))a.·(((a.·(b.·b.))·c.)·(c.·(c.·c.)))
a.·a.a.·(b.·((b.·(a.·a.))·b.))
a.(a.·((a.·b.)·c.))·(a.·(b.·α.))
(a.·a.)·(((b.·a.)·c.)·(α.·c.))(a.·a.)·((a.·a.)·((b.·a.)·c.))
a.·((b.·c.)·a.)c.·(((c.·(b.·b.))·a.)·(a.·(a.·a.)))
a.(a.·a.)·(b.·((b.·a.)·b.))
a.(a.·(b.·c.))·(a.·((a.·c.)·α.))
(a.·a.)·(((b.·a.)·c.)·(α.·c.))(a.·a.)·c.
a.·((b.·c.)·a.)c.·((b.·a.)·(a.·(a.·a.)))
a.·((a.·((a.·b.)·(a.·b.)))·a.)((a.·b.)·(a.·b.))·((a.·b.)·(((a.·b.)·(a.·b.))·(a.·b.)))
a.(a.·((a.·b.)·c.))·(a.·(α.·b.))
(a.·a.)·(((a.·b.)·c.)·(α.·c.))(a.·a.)·((a.·a.)·((a.·b.)·c.))
a.·((b.·c.)·a.)c.·(((a.·a.)·a.)·(a.·b.))
a.·((a.·((a.·b.)·(a.·b.)))·a.)a.·b.
a.·(b.·(b.·b.))((a.·(b.·(b.·b.)))·((b.·b.)·a.))·a.
(a.·a.)·(((a.·b.)·c.)·(α.·c.))(a.·a.)·c.
a.·((b.·c.)·a.)c.·((a.·(a.·a.))·(b.·a.))
((a.·b.)·a.)·(a.·a.)((a.·b.)·a.)·((((a.·b.)·a.)·(a.·(((a.·b.)·a.)·(a.·a.))))·((a.·b.)·a.))
a.·(b.·(b.·b.))a.·a.
a.·(a.·b.)a.·(b.·((c.·((c.·a.)·α.))·c.))
(a.·a.)·((b.·b.)·c.)(c.·(b.·(a.·b.)))·(a.·a.)
a.((a.·b.)·a.)·((((a.·b.)·a.)·(a.·(((a.·b.)·a.)·(a.·a.))))·((a.·b.)·a.))
a.·a.(b.·(b.·b.))·a.
(a.·((a.·b.)·c.))·((c.·(c.·c.))·((a.·((a.·b.)·c.))·(a.·((a.·((a.·b.)·c.))·a.))))(a.·b.)·(((a.·b.)·(a.·((a.·((a.·b.)·c.))·a.)))·(a.·b.))
(a.·a.)·(((b.·c.)·(b.·c.))·(a.·(b.·c.)))(c.·(c.·(b.·(a.·(b.·c.)))))·(a.·a.)
a.((a.·b.)·a.)·((((a.·b.)·a.)·(a.·a.))·((a.·b.)·a.))
(a.·(b.·(a.·b.)))·(c.·(c.·c.))a.
(a.·((a.·b.)·c.))·(a.·((a.·((a.·b.)·c.))·a.))(a.·b.)·(((a.·b.)·(a.·((a.·((a.·b.)·c.))·a.)))·(a.·b.))
(a.·b.)·(((a.·b.)·(c.·c.))·(a.·b.))(b.·(b.·(a.·(c.·(a.·b.)))))·(c.·c.)
a.((a.·b.)·a.)·(a.·((a.·b.)·a.))
(a.·a.)·(b.·(b.·b.))a.
(a.·((a.·b.)·c.))·(a.·((a.·b.)·c.))(a.·b.)·(((a.·b.)·(a.·((a.·((a.·b.)·c.))·a.)))·(a.·b.))
(a.·b.)·(c.·(a.·b.))(b.·(b.·(a.·(c.·(a.·b.)))))·(c.·c.)
(a.·b.)·a.(a.·((a.·b.)·a.))·(((a.·b.)·a.)·((((a.·b.)·a.)·(a.·a.))·((a.·b.)·a.)))
a.·(a.·b.)(b.·(c.·(c.·c.)))·a.
(c.·(c.·c.))·(a.·((a.·b.)·c.))(a.·b.)·(((a.·b.)·(a.·((a.·((a.·b.)·c.))·a.)))·(a.·b.))
(a.·b.)·(c.·(a.·b.))(((a.·a.)·b.)·b.)·(c.·c.)
(a.·b.)·a.(a.·((a.·b.)·a.))·(((a.·b.)·a.)·(a.·((a.·b.)·a.)))
a.(b.·(b.·b.))·(a.·a.)
(c.·(c.·c.))·(a.·((a.·b.)·c.))(a.·b.)·((a.·b.)·((a.·((a.·((a.·b.)·c.))·a.))·(b.·a.)))
(a.·b.)·(b.·((b.·a.)·b.))(c.·(c.·c.))·(b.·a.)
(a.·b.)·a.(a.·((a.·b.)·a.))·a.
a.((b.·(b.·b.))·a.)·(c.·a.)
(c.·(c.·c.))·(a.·((a.·b.)·c.))(a.·((a.·((a.·b.)·c.))·a.))·(a.·b.)
(a.·b.)·(b.·(b.·b.))(c.·(c.·c.))·(b.·a.)
a.·((a.·((a.·b.)·a.))·a.)((a.·b.)·a.)·(((a.·b.)·a.)·(a.·((a.·b.)·a.)))
((a.·a.)·(b.·(b.·b.)))·c.c.·((b.·(b.·b.))·(a.·c.))
(c.·(c.·c.))·(a.·((a.·b.)·c.))(a.·b.)·((a.·(a.·((a.·b.)·c.)))·a.)
(c.·(c.·c.))·(a.·b.)((a.·a.)·a.)·(a.·b.)
a.·((a.·b.)·a.)((a.·b.)·a.)·(((a.·b.)·a.)·(a.·((a.·b.)·a.)))
a.·b.b.·((c.·(c.·c.))·(a.·b.))
(c.·(c.·c.))·(a.·((a.·b.)·c.))(a.·b.)·(a.·((((a.·b.)·c.)·a.)·a.))
(c.·(c.·c.))·(a.·b.)(a.·(a.·a.))·(b.·a.)
a.·((a.·b.)·a.)((a.·b.)·a.)·a.
a.·((b.·b.)·(c.·(c.·c.)))a.·((c.·(c.·c.))·(a.·b.))
(c.·(c.·c.))·(a.·((a.·b.)·c.))(a.·b.)·(a.·(a.·(a.·(c.·(a.·b.)))))
(a.·(a.·b.))·(c.·a.)(a.·c.)·(a.·(b.·a.))
a.·((a.·((a.·((a.·b.)·(a.·b.)))·a.))·a.)((a.·b.)·a.)·a.
a.·b.a.·((c.·(c.·c.))·(a.·b.))
(c.·(c.·c.))·(a.·((a.·b.)·c.))(a.·b.)·(a.·(c.·(a.·b.)))
(((a.·b.)·c.)·α.)·(((a.·b.)·c.)·((b.·a.)·((a.·b.)·c.)))(a.·b.)·(α.·((a.·b.)·c.))
a.·((a.·((a.·b.)·(a.·b.)))·a.)((a.·b.)·a.)·a.
a.(b.·(b.·b.))·((c.·(c.·c.))·a.)
(a.·b.)·(a.·((a.·((b.·c.)·a.))·(a.·b.)))(c.·(c.·c.))·(a.·((a.·b.)·(a.·b.)))
(((a.·b.)·c.)·α.)·(b.·a.)(a.·b.)·(α.·((a.·b.)·c.))
a.·b.((a.·b.)·a.)·a.
a.·a.a.·(((b.·(b.·b.))·a.)·c.)
(a.·((b.·c.)·a.))·(a.·b.)(c.·(c.·c.))·(a.·((a.·b.)·(a.·b.)))
(a.·b.)·(c.·(a.·b.))(b.·((a.·a.)·b.))·(c.·c.)
a.·b.a.·((a.·b.)·a.)
a.·(a.·b.)((c.·(c.·c.))·b.)·a.
(a.·((b.·c.)·a.))·(a.·b.)(c.·(c.·c.))·(b.·a.)
(a.·b.)·(c.·(a.·b.))(b.·a.)·(c.·c.)
((a.·b.)·c.)·(a.·c.)c.
a.·(b.·a.)((c.·(c.·c.))·b.)·a.
(a.·b.)·((a.·(b.·c.))·a.)(c.·(c.·c.))·(b.·a.)
(a.·b.)·((a.·c.)·((b.·α.)·a.))a.·(b.·a.)
((a.·b.)·a.)·(a.·b.)a.
a.·(a.·b.)a.·((c.·(c.·c.))·b.)
(a.·b.)·(a.·((c.·b.)·a.))(c.·(c.·c.))·(b.·a.)
(a.·b.)·(c.·(a.·b.))((a.·b.)·c.)·(((a.·b.)·c.)·((a.·(a.·a.))·(b.·a.)))
(a.·a.)·(b.·a.)a.
a.·(b.·a.)a.·((c.·(c.·c.))·b.)
(a.·b.)·(a.·b.)(c.·(c.·c.))·(b.·a.)
(a.·b.)·(c.·(a.·b.))((a.·b.)·c.)·(a.·((b.·((a.·b.)·c.))·a.))
(a.·b.)·(b.·b.)b.
((a.·(a.·a.))·b.)·c.c.·(b.·b.)
a.·(b.·b.)(b.·c.)·((b.·c.)·((b.·b.)·a.))
(a.·b.)·(c.·(a.·b.))((a.·b.)·c.)·(a.·((b.·b.)·a.))
a.·(a.·(b.·a.))b.·((b.·a.)·b.)
a.(a.·(b.·((c.·((b.·b.)·c.))·(α.·(b.·b.)))))·(a.·(α.·(b.·b.)))
a.·(a.·b.)a.·(b.·(c.·((α.·(c.·a.))·c.)))
(a.·b.)·(c.·(a.·b.))((a.·b.)·c.)·(a.·b.)
a.·(a.·(b.·a.))b.·a.
a.(a.·(b.·((c.·b.)·(α.·(b.·b.)))))·(a.·(α.·(b.·b.)))
a.·(a.·b.)a.·(b.·(c.·(c.·((a.·c.)·α.))))
(a.·b.)·(c.·c.)((b.·a.)·c.)·(b.·a.)
a.·(b.·(a.·a.))a.·a.
a.(a.·(b.·c.))·(a.·(α.·(c.·c.)))
a.·(a.·(b.·b.))a.·((b.·b.)·((a.·(c.·b.))·α.))
(a.·b.)·(c.·c.)(b.·a.)·(c.·(a.·b.))
(a.·b.)·((c.·a.)·b.)b.
a.((b.·((c.·((b.·b.)·c.))·(α.·(b.·b.))))·a.)·(a.·(α.·(b.·b.)))
a.·b.b.·((a.·a.)·((b.·(c.·a.))·α.))
(a.·b.)·(c.·(c.·(b.·a.)))(a.·b.)·(c.·(c.·((b.·a.)·(c.·c.))))
a.·((b.·((b.·c.)·b.))·(c.·((c.·a.)·c.)))c.·((c.·a.)·c.)
a.((b.·((c.·b.)·(α.·(b.·b.))))·a.)·(a.·(α.·(b.·b.)))
a.·b.b.·((c.·(b.·(α.·a.)))·(a.·a.))
(a.·b.)·(c.·(c.·(b.·a.)))(a.·b.)·(c.·(c.·c.))
a.·((b.·c.)·(c.·((c.·a.)·c.)))c.·((c.·a.)·c.)
a.((b.·c.)·a.)·(a.·(α.·(c.·c.)))
(a.·(a.·b.))·(((c.·a.)·((a.·b.)·a.))·b.)(c.·a.)·((a.·b.)·a.)
(c.·(a.·b.))·(b.·b.)(b.·a.)·((b.·a.)·((b.·b.)·(c.·c.)))
a.·((b.·c.)·(c.·a.))c.·((c.·a.)·c.)
a.((b.·((c.·((b.·b.)·c.))·((b.·b.)·α.)))·a.)·(a.·((b.·b.)·α.))
(a.·(a.·b.))·(b.·(((a.·b.)·a.)·(a.·c.)))(c.·a.)·((a.·b.)·a.)
(c.·(a.·b.))·(b.·b.)(c.·c.)·(b.·b.)
a.·((b.·c.)·(c.·a.))c.·a.
a.((b.·((c.·b.)·((b.·b.)·α.)))·a.)·(a.·((b.·b.)·α.))
(a.·(a.·b.))·(b.·((a.·(a.·b.))·(c.·a.)))(c.·a.)·((a.·b.)·a.)
(a.·a.)·((c.·(b.·a.))·c.)(a.·a.)·(c.·((α.·(α.·α.))·((c.·c.)·(a.·a.))))
a.·((b.·c.)·(b.·((b.·a.)·b.)))b.·((b.·a.)·b.)
a.((b.·c.)·a.)·(a.·((c.·c.)·α.))
(a.·(a.·b.))·(b.·(b.·(c.·a.)))(c.·a.)·((a.·b.)·a.)
(a.·a.)·((c.·(b.·a.))·c.)(a.·a.)·((c.·c.)·c.)
a.·((b.·c.)·(b.·a.))b.·((b.·a.)·b.)
a.((b.·((c.·(c.·(b.·b.)))·(α.·(b.·b.))))·a.)·(a.·(α.·(b.·b.)))
(a.·(a.·b.))·(b.·(b.·(c.·a.)))(c.·a.)·(a.·(b.·a.))
((c.·(a.·b.))·c.)·(c.·((b.·b.)·c.))(c.·(c.·(b.·b.)))·((b.·b.)·((b.·b.)·((c.·c.)·c.)))
a.·((b.·c.)·(b.·a.))b.·a.
a.((b.·((b.·c.)·(α.·(b.·b.))))·a.)·(a.·(α.·(b.·b.)))
(a.·(b.·c.))·c.c.·((b.·b.)·((a.·(b.·c.))·(a.·(b.·c.))))
((c.·(a.·b.))·c.)·(c.·b.)(c.·(c.·(b.·b.)))·((b.·b.)·((b.·b.)·((c.·c.)·c.)))
a.·(b.·((c.·b.)·(((c.·b.)·a.)·(c.·b.))))(c.·b.)·(((c.·b.)·a.)·(c.·b.))
a.((b.·c.)·a.)·(a.·(α.·(b.·b.)))
(a.·(b.·c.))·c.c.·((b.·b.)·a.)
((c.·(a.·b.))·c.)·(c.·b.)((c.·c.)·c.)·(c.·((b.·b.)·c.))
a.·(b.·((c.·b.)·a.))(c.·b.)·(((c.·b.)·a.)·(c.·b.))
a.(a.·(b.·((c.·((b.·b.)·c.))·(α.·(b.·b.)))))·((α.·(b.·b.))·a.)
((a.·b.)·c.)·b.b.·((a.·a.)·(((a.·b.)·c.)·((a.·b.)·c.)))
((c.·(a.·b.))·c.)·(c.·b.)((c.·c.)·c.)·(c.·b.)
a.·(b.·((c.·b.)·a.))(c.·b.)·a.
a.(a.·(b.·((c.·b.)·(α.·(b.·b.)))))·((α.·(b.·b.))·a.)
((a.·b.)·c.)·b.b.·((a.·a.)·c.)
(a.·b.)·(b.·(c.·b.))(b.·((a.·b.)·c.))·(b.·((a.·b.)·c.))
((a.·b.)·a.)·(b.·((c.·a.)·(((c.·a.)·((a.·b.)·a.))·(c.·a.))))(c.·a.)·(((c.·a.)·((a.·b.)·a.))·(c.·a.))
a.(a.·(b.·c.))·((α.·(c.·c.))·a.)
((a.·b.)·c.)·a.a.·((b.·b.)·(((a.·b.)·c.)·((a.·b.)·c.)))
(a.·b.)·(b.·(c.·b.))(c.·(c.·c.))·(((a.·b.)·c.)·b.)
((a.·b.)·a.)·(b.·((c.·a.)·((a.·b.)·a.)))(c.·a.)·(((c.·a.)·((a.·b.)·a.))·(c.·a.))
a.(a.·(b.·((c.·(c.·(b.·b.)))·(α.·(b.·b.)))))·((α.·(b.·b.))·a.)
((a.·b.)·c.)·a.a.·((b.·b.)·c.)
(a.·b.)·(b.·(c.·b.))(c.·(c.·c.))·(b.·(c.·(b.·a.)))
((a.·b.)·a.)·(b.·((c.·a.)·((a.·b.)·a.)))(c.·a.)·((a.·b.)·a.)
a.(a.·(b.·((b.·c.)·(α.·(b.·b.)))))·((α.·(b.·b.))·a.)
a.·((a.·b.)·c.)a.·((b.·b.)·c.)
((a.·a.)·b.)·(b.·(c.·b.))(c.·(c.·c.))·(b.·(a.·c.))
a.(a.·a.)·(a.·b.)
a.(a.·(b.·c.))·((α.·(b.·b.))·a.)
a.·(((b.·b.)·(b.·b.))·c.)a.·(c.·(a.·(a.·b.)))
(a.·b.)·(a.·((c.·b.)·c.))((c.·c.)·a.)·(a.·b.)
a.(a.·b.)·(a.·a.)
((a.·(b.·(c.·a.)))·c.)·a.a.·a.
a.·(b.·c.)a.·(c.·(a.·(a.·b.)))
(a.·b.)·(a.·(c.·(b.·c.)))((c.·c.)·a.)·(a.·b.)
a.·a.a.·((a.·a.)·b.)
a.·((a.·(b.·(c.·a.)))·c.)a.·a.
(a.·a.)·((b.·b.)·c.)(a.·a.)·(c.·(b.·(b.·a.)))
(a.·b.)·(c.·(α.·(b.·a.)))(b.·a.)·(c.·((b.·a.)·α.))
(a.·b.)·a.a.·(a.·b.)
a.·(b.·(a.·(c.·(b.·a.))))a.·a.
a.·((((b.·(b.·b.))·c.)·((b.·(b.·b.))·c.))·α.)a.·(((c.·c.)·a.)·α.)
(a.·b.)·(b.·((a.·b.)·c.))((c.·c.)·b.)·(b.·a.)
a.·(a.·(a.·b.))a.·b.
a.·(b.·(c.·(a.·b.)))a.·(b.·b.)
a.·(b.·c.)a.·(((b.·b.)·a.)·c.)
(a.·b.)·(b.·(c.·b.))((c.·c.)·b.)·(b.·a.)
a.(b.·a.)·((b.·c.)·a.)
a.·(b.·b.)a.·(b.·((a.·b.)·c.))
a.·((((b.·(b.·b.))·c.)·((b.·(b.·b.))·c.))·α.)a.·((a.·(c.·a.))·α.)
(c.·(c.·c.))·(a.·(b.·c.))((c.·c.)·a.)·(a.·(b.·b.))
(a.·b.)·((a.·b.)·a.)a.
a.·((b.·b.)·(b.·b.))a.·((b.·b.)·(c.·(a.·(b.·a.))))
a.·(b.·c.)a.·((a.·(b.·a.))·c.)
((b.·b.)·a.)·((c.·c.)·a.)(a.·(b.·c.))·(c.·(c.·c.))
(a.·b.)·(a.·(a.·b.))a.
a.·b.a.·((b.·b.)·(c.·(a.·(b.·a.))))
a.·((((b.·(b.·b.))·c.)·((b.·(b.·b.))·c.))·α.)a.·((a.·(a.·c.))·α.)
((b.·b.)·a.)·((c.·c.)·a.)(a.·(c.·b.))·(c.·(c.·c.))
a.·b.b.·((c.·(b.·b.))·(a.·b.))
a.·(b.·b.)a.·(b.·((b.·a.)·c.))
a.·(b.·c.)a.·((a.·(a.·b.))·c.)
((b.·b.)·a.)·((c.·c.)·a.)(c.·(c.·c.))·(a.·(c.·b.))
a.·b.a.·((c.·(a.·a.))·(a.·b.))
a.·((a.·(b.·c.))·(c.·c.))a.·a.
(a.·b.)·c.c.·(a.·((b.·b.)·c.))
((c.·c.)·a.)·(a.·(b.·b.))(c.·(c.·c.))·(a.·(c.·b.))
(a.·b.)·c.(a.·((a.·b.)·c.))·c.
a.·a.a.·((a.·(b.·(b.·c.)))·((c.·c.)·(c.·c.)))
a.·((a.·b.)·c.)a.·(c.·(b.·c.))
(c.·(c.·c.))·(a.·(b.·c.))(c.·(c.·c.))·(a.·(c.·b.))
Full expression not available
(
original memory size:
344.1 kB)

Models

Every lemma must be consistent with all models of Boolean algebra.....
This implies there is a model of the axiom for which the proposition is not true...

Lemma List

Are there repeated trees?

There are none that are common but big .... or rare and small
So introducing new operators doesn’t seem promising.....
How much redundancy is there in the lemmas ?
Is there a dictionary encoding that shortens this?

Can We Linearize the Proof?

Can we visualize this ?
Length of lemmas vs linearized position

Just applying axioms to get from one side of a lemma to the other

[[[ It has to step up or down, because it’s just applying the axiom at each step ]]]
[[[[[[[ Show position of axiom application :: ]]]]]]]]
[[ Use CountDependencies ?? ]] [[[ path length perhaps ~200 M ]]]
[[[ represent expressions in terms of depth ... cf. https://writings.stephenwolfram.com/2020/12/combinators-a-centennial-view/#visualizing-combinators ]]]

What are the laws of inference of LEAN ?

You can add LoIs ... just like you add axioms ....
​[ How do you know e.g. that you can copy a variable? ]
Reverse math: what LoI do you have to have to make the proof obvious? In general, could need new LoIs to make more proofs simple.
What observer would fish this proof out of the ruliad? Not a human........
Do the parameters of Waldmeister define different reference frames?

Can we find “nearby paths” ...

E.g. do substitutions at slightly different places? [and which direction of the rule?]