Relationship to FindEquationalProof

In[]:=
NestGraph[Flatten[{Values[coSubstitutionLemmas[#,x_⊕y_y_⊕x_,"Canonicalize"->True]]}]&,a_⊕b_b_⊕a_,4,GraphLayout->"SpringElectricalEmbedding",VertexLabels->Placed["Name",Tooltip]]
Out[]=
In[]:=
RandomChoiceVertexList

Out[]=
a_⊕((b_⊕c_)⊕(d_⊕(e_⊕f_)))(((f_⊕e_)⊕d_)⊕(c_⊕b_))⊕a_
In[]:=
FindEquationalProof[ForAll[{a,b,c},(a⊕b)⊕c==c⊕(a⊕b)],ForAll[{x,y},x⊕y==y⊕x]]
Out[]=
ProofObject
Logic: EquationalLogic
Steps: 3
Theorem:
∀
{a,b,c}
(a⊕b)⊕cc⊕(a⊕b)

In[]:=
%["ProofGraph"]
Out[]=
In[]:=
a_⊕((b_⊕c_)⊕(d_⊕(e_⊕f_)))(((f_⊕e_)⊕d_)⊕(c_⊕b_))⊕a_/.p_Pattern:>First[p]
Out[]=
a⊕((b⊕c)⊕(d⊕(e⊕f)))(((f⊕e)⊕d)⊕(c⊕b))⊕a
In[]:=
FindEquationalProof[ForAll[{a,b,c,d,e,f},a⊕((b⊕c)⊕(d⊕(e⊕f)))==(((f⊕e)⊕d)⊕(c⊕b))⊕a],ForAll[{x,y},x⊕y==y⊕x]]
Out[]=
ProofObject
Logic: EquationalLogic
Steps: 7
Theorem:
∀
{a,b,c,d,e,f}
a⊕((b⊕c)⊕(d⊕(e⊕f)))(((f⊕e)⊕d)⊕(c⊕b))⊕a

In[]:=
%["ProofGraph"]
Out[]=
In[]:=
%41["ProofDataset"]
Out[]=
›
› Proof
Input
{SubstitutionLemma,1}
Position
{1,1,2}
Construct
{Axiom,1}
Orientation
{-1,1}
Rule
x_⊕y_y⊕x
OutputExpression
(((f⊕e)⊕d)⊕(b⊕c))⊕aa⊕((b⊕c)⊕(d⊕(f⊕e)))
In[]:=
Variables[(a⊕b)⊕c==c⊕(b⊕a)]
Out[]=
{}
In[]:=
(ForAll@@{Union[Level[#,{-1}]],#/.TwoWayRule->Equal})&/@VertexList
/.p_Pattern:>First[p]
Out[]=
In[]:=
FindEquationalProof[#,ForAll[{x,y},x⊕y==y⊕x],"ProofGraph"]&/@Take[%,10]
FindEquationalProof
:Invalid specification of propositions True and axioms
∀
{x,y}
x⊕yy⊕x.
Out[]=

,
,
,FindEquationalProofTrue,
∀
{x,y}
x⊕yy⊕x[ProofGraph],
,
,
,
,
,
