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_∘1a_,a_∘
a_
1,11,a_a_,1∘1a_∘
a_
,1∘
a_∘
a_
1,1∘(a_∘b_)((c_∘
c_
)∘a_)∘b_,a_∘1a_∘1,a_∘1(a_∘b_)∘
b_
,a_∘
a_
1∘1,a_∘
a_
b_∘
b_
,a_∘
a_∘1
1,a_∘b_(a_∘b_)∘1,a_∘(1∘1)a_,a_∘(1∘b_)a_∘b_,a_∘(1∘b_)(a_∘(c_∘
c_
))∘b_,a_∘(
a_
∘1)1,a_∘(
a_
∘b_)1∘b_,a_∘(b_∘1)a_∘b_,a_∘(b_∘1)(a_∘b_)∘(c_∘
c_
),a_∘(b_∘
b_
)a_,a_∘(b_∘
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_∘
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_∘
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)∘1a_,(a_∘1)∘
a_
1,(a_∘1)∘(b_∘c_)(a_∘b_)∘c_,(a_∘
a_
)∘11,(a_∘
a_
)∘
1
1,(a_∘
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_))∘
(a_∘b_)∘c_
1,(a_∘(b_∘c_))∘(d_∘e_)(((a_∘b_)∘c_)∘d_)∘e_,((a_∘b_)∘c_)∘1a_∘(b_∘c_),((a_∘b_)∘c_)∘
a_∘(b_∘c_)
1,((a_∘b_)∘c_)∘(d_∘e_)((a_∘(b_∘c_))∘d_)∘e_
Function[nott,nott->Position[MatchQ[First[nott]/.Equal->TwoWayRule,#]&/@vvvv,True]]/@notablethms
In[]:=
Rest[AxiomaticTheory["GroupAxioms","NotableTheorems"]]
Out[]=
InverseOfComposite
∀
{a.,b.}
a.⊗b.

b.
⊗
a.
,InverseOfInverse
∀
a.
a.
a.,LeftIdentity
∀
a.

1
⊗a.a.,LeftInverse
∀
a.
a.
⊗a.

1

In[]:=
{,#}&/@ResourceFunction["UnformalizeSymbols"][Last/@Flatten[Values[Rest[AxiomaticTheory["GroupAxioms","NotableTheorems"]]]]]/.{CircleTimes->SmallCircle,OverTilde[1]->1}
In[]:=
gnot="inverse of composite",
a∘b

b
∘
a
,"inverse of inverse",
a
a,{"left identity",1∘aa},{"left inverse",
a
∘a1}
Out[]=
inverse of composite,
a∘b

b
∘
a
,inverse of inverse,
a
a,{left identity,1∘aa},{left inverse,
a
∘a1}
In[]:=
Function[nott,nott->Position[MatchQ[First[nott]/.Equal->TwoWayRule,#]&/@vvvv,True]]/@gnot
Out[]=
inverse of composite,
a∘b

b
∘
a
{},inverse of inverse,
a
a{},{left identity,1∘aa}{},{left inverse,
a
∘a1}{}
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_∘1a_,a_∘
a_
1,11,a_a_,a_∘1a_∘1,a_∘
a_
1∘1,a_∘
a_
b_∘
b_
,a_∘
a_∘1
1,a_∘(1∘1)a_,a_∘(
a_
∘1)1,a_∘(b_∘
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)∘1a_,(a_∘1)∘
a_
1,(a_∘1)∘(b_∘c_)(a_∘b_)∘c_,(a_∘
a_
)∘11,(a_∘b_)∘c_(a_∘b_)∘c_,(a_∘(b_∘c_))∘1(a_∘b_)∘c_
In[]:=
Function[nott,nott->Position[MatchQ[First[nott]/.Equal->TwoWayRule,#]&/@vvvv,True]]/@gnot
Out[]=
inverse of composite,
a∘b

b
∘
a
{},inverse of inverse,
a
a{},{left identity,1∘aa}{},{left inverse,
a
∘a1}{}
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,
a∘b

b
∘
a
{},inverse of inverse,
a
a{},{left identity,1∘aa}{},{left inverse,
a
∘a1}{}
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,
a∘b

b
∘
a
{},inverse of inverse,
a
a{},{left identity,1∘aa}{},{left inverse,
a
∘a1}{}
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,
a∘b

b
∘
a
{},inverse of inverse,
a
a{},{left identity,1∘aa}{},{left inverse,
a
∘a1}{}
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[]=