Wolfram Cloud Document

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[newHypsevent,List,1]},Splice@PadRight[out,2,out]],eventhyp}]/@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[]=