You are using a browser not supported by the Wolfram Cloud
Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.
I understand and wish to continue anyway »
WOLFRAM NOTEBOOK
In[]:=
twoWayRuleFix[expr_]:=expr/.{TwoWayRule->LeftRightArrow,p_Pattern:>First@p}EdgeFix[g_]:=VertexReplace[g,Thread[Verbatim/@VertexList[g]->twoWayRuleFix/@VertexList[g]]]
In[]:=
findProof//ClearAllfindProof[teg_Graph,axioms_List,hyp_,n_:1]:=Module[{events,eventHyps,hitHyps,m=Replace[n,All->Infinity]},If[m<=0,Return[{}]];If[MemberQ[axioms,hyp],Return[{{}}]];If[VertexCount[teg,hyp]==0,Return[Missing["Hypothesis"]]];If[VertexCount[teg,Alternatives@@axioms]==0,Return[Missing["Axioms"]]];events=VertexInComponent[teg,hyp,{1}];eventHyps=AssociationMap[VertexInComponent[teg,#,{1}]&,events];FoldWhile[With[{proofs=#1,event=#2[[1]],newHyps=#2[[2]]},With[{subProofs=Enclose[FoldPairList[{k,newHyp}|->With[{hypProofs=ConfirmBy[findProof[VertexDelete[teg,events],axioms,newHyp,k],Length[#]>0&]},{hypProofs,Ceiling[Max[k,0]/Length[hypProofs]]}],m-Length[proofs],Union@newHyps],{{}}&]},Join[proofs,ResourceFunction["MultisetUnion"]@@@(Append[{With[{out=Thread[newHypsevent,List,1]},Splice@PadRight[out,2,out]],eventhyp}]/@Tuples[subProofs/._Missing->{}])]]]&,{},Normal@KeySortBy[Last]@eventHyps,Length/*LessThan[m]]]
In[]:=
extendGraph[g_Graph,edges_List]:=EdgeAdd[g,ResourceFunction["MultisetComplement"][edges,EdgeList@g]]
In[]:=
removeEvents[teg_Graph]:=EdgeAdd[VertexDelete[teg,HoldPattern[{"Event",__}]],Catenate[DirectedEdge@@@Tuples[{VertexInComponent[teg,#,{1}],VertexOutComponent[teg,#,{1}]}]&/@VertexList[teg,{"Event",__}]]]
Substitution lemmas
String TwoWayRules
In[]:=
StringApply[lhs1_<->rhs1_,lhs2_<->rhs2_]:=TwoWayRule@@@Join[{{lhs2,rhs2}},{#,rhs2}&/@StringReplaceList[lhs2,lhs1->rhs1],{lhs2,#}&/@StringReplaceList[rhs2,lhs1->rhs1],{#,rhs2}&/@StringReplaceList[lhs2,rhs1->lhs1],{lhs2,#}&/@StringReplaceList[rhs2,rhs1->lhs1]]
In[]:=
StringApply[rules1_List,rules2_List]:=Flatten[Outer[StringApply,rules1,rules2],2]
In[]:=
rgg3=ResourceFunction["TokenEventGraph"][{{r1_,r2_}:>StringApply[r1,r2]},{"AB"<->"B"},3,"TokenMultiplicity"->Automatic,"EventDeduplication"->True,"TokenLabeling"->False,AspectRatio->1]
Out[]=
In[]:=
proofs=findProof[rgg3,{"AB"<->"B"},"AAAAB""AAAB",3];//AbsoluteTiming
Out[]=
{40.9749,Null}
In[]:=
Subgraph[extendGraph[rgg3,#],#,VertexLabelsAutomatic,ImageSizeScaled[.3]]&/@proofs
Out[]=
,
,
In[]:=
HighlightGraph[extendGraph[EdgeFix@rgg3,#],Style[#,Red,Thickness[.01]],ImageSizeScaled[.3]]&/@proofs
Out[]=
,
,