In[]:=
vvvv=VertexList[TokenEventBisubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory["GroupAxioms"]]/.{CircleTimes->SmallCircle,OverTilde[1]->1},1,GraphLayout->"SpringElectricalEmbedding"],_TwoWayRule];
In[]:=
vvvv
Out[]=
a_∘(b_∘c_)(a_∘b_)∘c_,a_∘1a_,a_∘1,11,a_a_,1∘1a_∘,1∘1,1∘(a_∘b_)((c_∘)∘a_)∘b_,a_∘1a_∘1,a_∘1(a_∘b_)∘,a_∘1∘1,a_∘b_∘,a_∘1,a_∘b_(a_∘b_)∘1,a_∘(1∘1)a_,a_∘(1∘b_)a_∘b_,a_∘(1∘b_)(a_∘(c_∘))∘b_,a_∘(∘1)1,a_∘(∘b_)1∘b_,a_∘(b_∘1)a_∘b_,a_∘(b_∘1)(a_∘b_)∘(c_∘),a_∘(b_∘)a_,a_∘(b_∘)1,a_∘(b_∘c_)a_∘(b_∘c_),a_∘(b_∘c_)(a_∘b_)∘(c_∘1),a_∘(b_∘c_)(a_∘(b_∘1))∘c_,a_∘(b_∘c_)((a_∘1)∘b_)∘c_,a_∘(b_∘c_)((a_∘b_)∘1)∘c_,a_∘(b_∘c_)((a_∘b_)∘c_)∘1,a_∘(b_∘(c_∘1))(a_∘b_)∘c_,a_∘(b_∘(c_∘))(a_∘b_)∘1,a_∘(b_∘(c_∘d_))(a_∘(b_∘c_))∘d_,a_∘(b_∘(c_∘d_))((a_∘b_)∘c_)∘d_,a_∘(b_∘(c_∘(d_∘e_)))(a_∘b_)∘((c_∘d_)∘e_),a_∘(b_∘((c_∘d_)∘e_))(a_∘b_)∘(c_∘(d_∘e_)),a_∘((b_∘1)∘c_)(a_∘b_)∘c_,a_∘((b_∘)∘c_)(a_∘1)∘c_,a_∘((b_∘c_)∘1)(a_∘b_)∘c_,a_∘((b_∘c_)∘d_)(a_∘b_)∘(c_∘d_),a_∘((b_∘c_)∘d_)((a_∘b_)∘c_)∘d_,a_∘((b_∘(c_∘d_))∘e_)(a_∘((b_∘c_)∘d_))∘e_,a_∘(((b_∘c_)∘d_)∘e_)(a_∘(b_∘(c_∘d_)))∘e_,(a_∘1)∘1a_,(a_∘1)∘1,(a_∘1)∘(b_∘c_)(a_∘b_)∘c_,(a_∘)∘11,(a_∘)∘1,(a_∘)∘(b_∘c_)(1∘b_)∘c_,(a_∘b_)∘c_(a_∘b_)∘c_,(a_∘b_)∘(c_∘d_)(a_∘(b_∘c_))∘d_,(a_∘(b_∘c_))∘1(a_∘b_)∘c_,(a_∘(b_∘c_))∘1,(a_∘(b_∘c_))∘(d_∘e_)(((a_∘b_)∘c_)∘d_)∘e_,((a_∘b_)∘c_)∘1a_∘(b_∘c_),((a_∘b_)∘c_)∘1,((a_∘b_)∘c_)∘(d_∘e_)((a_∘(b_∘c_))∘d_)∘e_
a_
a_
a_∘
a_
c_
b_
a_
a_
b_
a_∘1
c_
a_
a_
c_
b_
a_∘b_
c_
b_
a_
a_
a_
1
a_
(a_∘b_)∘c_
a_∘(b_∘c_)
Function[nott,nott->Position[MatchQ[First[nott]/.Equal->TwoWayRule,#]&/@vvvv,True]]/@notablethms
In[]:=
Rest[AxiomaticTheory["GroupAxioms","NotableTheorems"]]
Out[]=
InverseOfComposite⊗,InverseOfInversea.,LeftIdentity⊗a.a.,LeftInverse⊗a.
∀
{a.,b.}
a.⊗b.
b.
a.
∀
a.
a.
∀
a.
1
∀
a.
a.
1
In[]:=
{,#}&/@ResourceFunction["UnformalizeSymbols"][Last/@Flatten[Values[Rest[AxiomaticTheory["GroupAxioms","NotableTheorems"]]]]]/.{CircleTimes->SmallCircle,OverTilde[1]->1}
In[]:=
gnot="inverse of composite",∘,"inverse of inverse",a,{"left identity",1∘aa},{"left inverse",∘a1}
a∘b
b
a
a
a
Out[]=
inverse of composite,∘,inverse of inverse,a,{left identity,1∘aa},{left inverse,∘a1}
a∘b
b
a
a
a
In[]:=
Function[nott,nott->Position[MatchQ[First[nott]/.Equal->TwoWayRule,#]&/@vvvv,True]]/@gnot
Out[]=
inverse of composite,∘{},inverse of inverse,a{},{left identity,1∘aa}{},{left inverse,∘a1}{}
a∘b
b
a
a
a
In[]:=
vvvv=VertexList[TokenEventSubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory["GroupAxioms"]]/.{CircleTimes->SmallCircle,OverTilde[1]->1},1,GraphLayout->"SpringElectricalEmbedding"],_TwoWayRule];
In[]:=
vvvv
Out[]=
a_∘(b_∘c_)(a_∘b_)∘c_,a_∘1a_,a_∘1,11,a_a_,a_∘1a_∘1,a_∘1∘1,a_∘b_∘,a_∘1,a_∘(1∘1)a_,a_∘(∘1)1,a_∘(b_∘)a_,a_∘(b_∘c_)a_∘(b_∘c_),a_∘(b_∘c_)(a_∘b_)∘(c_∘1),a_∘(b_∘c_)(a_∘(b_∘1))∘c_,a_∘(b_∘c_)((a_∘1)∘b_)∘c_,a_∘(b_∘c_)((a_∘b_)∘1)∘c_,a_∘(b_∘c_)((a_∘b_)∘c_)∘1,a_∘(b_∘(c_∘1))(a_∘b_)∘c_,a_∘((b_∘1)∘c_)(a_∘b_)∘c_,a_∘((b_∘c_)∘1)(a_∘b_)∘c_,(a_∘1)∘1a_,(a_∘1)∘1,(a_∘1)∘(b_∘c_)(a_∘b_)∘c_,(a_∘)∘11,(a_∘b_)∘c_(a_∘b_)∘c_,(a_∘(b_∘c_))∘1(a_∘b_)∘c_
a_
a_
a_
b_
a_∘1
a_
b_
a_
a_
In[]:=
Function[nott,nott->Position[MatchQ[First[nott]/.Equal->TwoWayRule,#]&/@vvvv,True]]/@gnot
Out[]=
inverse of composite,∘{},inverse of inverse,a{},{left identity,1∘aa}{},{left inverse,∘a1}{}
a∘b
b
a
a
a
In[]:=
VertexCount[TokenEventBisubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory["GroupAxioms"]]/.{CircleTimes->SmallCircle,OverTilde[1]->1},1,GraphLayout->"SpringElectricalEmbedding"],_TwoWayRule]
Out[]=
56
In[]:=
VertexCount[TokenEventSubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory["GroupAxioms"]]/.{CircleTimes->SmallCircle,OverTilde[1]->1},1,GraphLayout->"SpringElectricalEmbedding"],_TwoWayRule]
Out[]=
27
In[]:=
vvvg2=VertexList[TokenEventBisubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory["GroupAxioms"]]/.{CircleTimes->SmallCircle,OverTilde[1]->1},2,"PatternTest"->(LeafCount[symbolifyPatterns[#]]<9&),GraphLayout->"SpringElectricalEmbedding"],_TwoWayRule];
In[]:=
Length[vvvg2]
Out[]=
466
In[]:=
Function[nott,nott->Position[MatchQ[First[nott]/.Equal->TwoWayRule,#]&/@vvvg2,True]]/@gnot
Out[]=
inverse of composite,∘{},inverse of inverse,a{},{left identity,1∘aa}{},{left inverse,∘a1}{}
a∘b
b
a
a
a
In[]:=
vvvg2=VertexList[TokenEventBisubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory["GroupAxioms"]]/.{CircleTimes->SmallCircle,OverTilde[1]->1},2,"PatternTest"->(LeafCount[symbolifyPatterns[#]]<10&),GraphLayout->"SpringElectricalEmbedding"],_TwoWayRule];
In[]:=
Length[vvvg2]
Out[]=
714
In[]:=
Function[nott,nott->Position[MatchQ[First[nott]/.Equal->TwoWayRule,#]&/@vvvg2,True]]/@gnot
Out[]=
inverse of composite,∘{},inverse of inverse,a{},{left identity,1∘aa}{},{left inverse,∘a1}{}
a∘b
b
a
a
a
In[]:=
FindEquationalProof[#,"GroupAxioms","ProofGraph"]&/@AxiomaticTheory["GroupAxioms","NotableTheorems"]
Out[]=
ImpliesMcCuneAxioms
,InverseOfComposite
,InverseOfInverse
,LeftIdentity
,LeftInverse
In[]:=
vvvg2=VertexList[TokenEventBisubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory["GroupAxioms"]]/.{CircleTimes->SmallCircle,OverTilde[1]->1},2,"PatternTest"->(LeafCount[symbolifyPatterns[#]]<11&),GraphLayout->"SpringElectricalEmbedding"],_TwoWayRule];
Out[]=
$Aborted
In[]:=
Length[vvvg2]
Out[]=
714
In[]:=
Function[nott,nott->Position[MatchQ[First[nott]/.Equal->TwoWayRule,#]&/@vvvg2,True]]/@gnot
Out[]=
inverse of composite,∘{},inverse of inverse,a{},{left identity,1∘aa}{},{left inverse,∘a1}{}
a∘b
b
a
a
a
In[]:=
Magnify[VertexReplace[TokenEventSubstitutionGraph[AxiomaticTheoryTWP[AxiomaticTheory["AbelianGroupAxioms"]]/.{CircleTimes->SmallCircle,OverTilde[1]->1},1,"EventDeduplication"->True,"TokenLabeling"->True,GraphLayout->"SpringElectricalEmbedding"],v:Except[_List]:>(Row[{#1," = ",#2}]&@@symbolifyPatterns[v])],.8]
Out[]=
