In[]:=
ProofObjectToTokenEventGraph@FindEquationalProof[1(a⊗1)⊗,AxiomaticTheory["GroupAxioms"]/.OverTilde->Identity]
a
Out[]=
In[]:=
teg=AccumulativeTokenEventGraph[{a_⊗(b_⊗c_)(a_⊗b_)⊗c_,a_⊗1a_,a_⊗1},2,"SC","EventDeduplication"->False,"TokenLabeling"->True,AspectRatio->1/3];
a_
In[]:=
proofs=findProof[teg,{a_⊗(b_⊗c_)(a_⊗b_)⊗c_,a_⊗1a_,a_⊗1,1<->(a_⊗1)⊗},a_<->a_,1];
a_
a_
Out[]=
$Aborted
In[]:=
proofs=findProof[teg,{a_⊗(b_⊗c_)(a_⊗b_)⊗c_,a_⊗1a_,a_⊗1},1<->(a_⊗1)⊗,2];
a_
a_
In[]:=
Graph/@proofs
Out[]=
,
In[]:=
EdgeSubgraph[extendGraph[teg,#],#]&/@proofs
Out[]=
,
In[]:=
Graph[teg,VertexShapeFunction_->Automatic]
Out[]=
In[]:=
VertexInComponent[teg,{"Event",1,2},{1}]
Out[]=
{a_⊗1a_}
In[]:=
SortBy[Last]@VertexInComponent[teg,a_<->a_,{1}]
Out[]=
{{Event,1,1},{Event,1,2},{Event,1,3},{Event,1,7},{Event,1,8},{Event,1,9},{Event,1,10},{Event,1,11},{Event,1,12},{Event,1,13},{Event,1,14},{Event,1,15},{Event,1,16},{Event,1,17},{Event,1,18},{Event,1,19},{Event,1,20},{Event,1,21},{Event,1,22},{Event,1,23},{Event,1,24},{Event,1,25},{Event,1,26},{Event,1,27},{Event,1,28},{Event,1,29},{Event,1,30},{Event,1,31},{Event,1,33},{Event,1,34},{Event,1,35},{Event,1,36},{Event,1,37},{Event,1,38},{Event,1,39},{Event,1,40},{Event,1,41},{Event,1,42},{Event,1,43},{Event,1,44},{Event,1,45},{Event,1,46},{Event,1,47},{Event,1,48},{Event,1,49},{Event,1,50},{Event,1,51},{Event,1,52},{Event,1,53},{Event,1,54},{Event,1,55},{Event,1,56},{Event,1,57},{Event,1,58},{Event,1,59},{Event,1,73},{Event,1,78},{Event,1,82},{Event,1,84},{Event,1,97},{Event,1,102},{Event,1,106},{Event,1,108},{Event,1,120},{Event,1,125},{Event,1,129},{Event,1,131},{Event,1,142},{Event,1,147},{Event,1,151},{Event,1,153},{Event,1,163},{Event,1,168},{Event,1,172},{Event,1,174},{Event,1,183},{Event,1,188},{Event,1,192},{Event,1,194},{Event,1,202},{Event,1,207},{Event,1,211},{Event,1,213},{Event,1,220},{Event,1,225},{Event,1,229},{Event,1,231},{Event,1,237},{Event,1,242},{Event,1,246},{Event,1,248},{Event,1,253},{Event,1,258},{Event,1,262},{Event,1,264},{Event,1,268},{Event,1,273},{Event,1,277},{Event,1,279},{Event,1,282},{Event,1,287},{Event,1,291},{Event,1,293},{Event,1,295},{Event,1,300},{Event,1,304},{Event,1,306},{Event,1,307},{Event,1,312},{Event,1,316},{Event,1,318},{Event,1,319},{Event,1,320},{Event,1,321},{Event,1,322},{Event,1,323},{Event,1,324},{Event,1,325},{Event,1,326},{Event,1,327},{Event,1,328},{Event,1,329},{Event,1,333},{Event,1,337},{Event,1,339},{Event,1,342},{Event,1,346},{Event,1,348},{Event,1,350},{Event,1,354},{Event,1,356},{Event,1,357},{Event,1,361},{Event,1,363},{Event,1,364},{Event,1,365},{Event,1,366},{Event,1,367},{Event,1,368},{Event,1,369},{Event,1,372},{Event,1,374},{Event,1,376},{Event,1,378},{Event,1,379},{Event,1,381},{Event,1,382},{Event,1,383},{Event,1,384}}