In[]:=
TokenEventSubstitutionGraph[{x_∘y_<->(y_∘x_)∘y_},2,AspectRatio->.6,"TokenLabeling"->False,GraphLayout->"LayeredDigraphEmbedding"]
In[]:=
AccumulativeTokenEventGraph[AxiomaticTheoryTWP[aa∘a],2,"PatternTest"->(Length@Level[#,{-1}]<5&),"TokenLabeling"->False,GraphLayout->"SpringElectricalEmbedding"]
Out[]=
In[]:=
AccumulativeTokenEventGraph[AxiomaticTheoryTWP[aa∘a],2,"PatternTest"->(Length@Level[#,{-1}]<4&),"TokenLabeling"->False,GraphLayout->"SpringElectricalEmbedding"]
Out[]=
In[]:=
AccumulativeTokenEventGraph[AxiomaticTheoryTWP[aa∘a],2,"PatternTest"->(Length@Level[#,{-1}]<4&),"TokenLabeling"->True,GraphLayout->"SpringElectricalEmbedding"]
Out[]=
TokenEventSubstitutionGraph[{x_∘y_<->(y_∘x_)∘y_},2,AspectRatio->.6,"TokenLabeling"->False,GraphLayout->"LayeredDigraphEmbedding"]
In[]:=
With[{bteg=branchialGraph[removeEvents[TokenEventSubstitutionGraph[{x_∘y_<->y_},2,"PatternTest"->(LeafCount[#]<Infinity&),AspectRatio->.8,"TokenLabeling"->False,GraphLayout->"LayeredDigraphEmbedding"]]]},Show[Graph[bteg,EdgeStyle->Opacity[.15,ResourceFunction["WolframPhysicsProjectStyleData"]["BranchialGraph"]["EdgeStyle"]],VertexSize->.05],Graphics[Inset[ExpressionGraph[#,EdgeStyle->Black,ImageSize->{30,30}]&/@Last[#],First[#],Center,{Automatic,.2}]&/@Transpose[{GraphEmbedding[bteg],VertexList[bteg]}]]]]
Out[]=
In[]:=
With[{bteg=branchialGraph[removeEvents[TokenEventSubstitutionGraph[{x_∘y_<->y_},2,"PatternTest"->(LeafCount[#]<20&),AspectRatio->.8,"TokenLabeling"->False,GraphLayout->"LayeredDigraphEmbedding"]]]},Show[Graph[bteg,EdgeStyle->Opacity[.15,ResourceFunction["WolframPhysicsProjectStyleData"]["BranchialGraph"]["EdgeStyle"]],VertexSize->.05],Graphics[Inset[ExpressionGraph[#,EdgeStyle->Black,ImageSize->{30,30}]&/@Last[#],First[#],Center,{Automatic,.2}]&/@Transpose[{GraphEmbedding[bteg],VertexList[bteg]}]]]]
Out[]=
In[]:=
With[{bteg=branchialGraph[removeEvents[TokenEventSubstitutionGraph[{x_∘y_<->y_},2,"PatternTest"->(Length@Level[#,{-1}]<4&),AspectRatio->.8,"TokenLabeling"->False,GraphLayout->"LayeredDigraphEmbedding"]]]},Show[Graph[bteg,EdgeStyle->Opacity[.15,ResourceFunction["WolframPhysicsProjectStyleData"]["BranchialGraph"]["EdgeStyle"]],VertexSize->.05],Graphics[Inset[ExpressionGraph[#,EdgeStyle->Black,ImageSize->{30,30}]&/@Last[#],First[#],Center,{Automatic,.2}]&/@Transpose[{GraphEmbedding[bteg],VertexList[bteg]}]]]]
Out[]=
In[]:=
With[{bteg=branchialGraph[removeEvents[TokenEventSubstitutionGraph[{x_∘y_<->y_},3,"PatternTest"->(Length@Level[#,{-1}]<4&),AspectRatio->.8,"TokenLabeling"->False,GraphLayout->"LayeredDigraphEmbedding"]]]},Show[Graph[bteg,EdgeStyle->Opacity[.15,ResourceFunction["WolframPhysicsProjectStyleData"]["BranchialGraph"]["EdgeStyle"]],VertexSize->.05],Graphics[Inset[ExpressionGraph[#,EdgeStyle->Black,ImageSize->{30,30}]&/@Last[#],First[#],Center,{Automatic,.2}]&/@Transpose[{GraphEmbedding[bteg],VertexList[bteg]}]]]]
Out[]=

Does this prove the same theorem as another axiom system?