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[]:=
PatVar[n_]:=Pattern[#,_]&[Symbol[FromLetterNumber[n]]]
In[]:=
PrepWMRule[rule_]:=With[{reps=MapIndexed[#->PatVar[First[#2]]&,Union[Level[rule,{-1}]]]},rule/.reps]
In[]:=
DecodeWMRule[rule_]:=rule/.p_Pattern:>LetterNumber[ToString[First[p]]]
In[]:=
makeHypergraphRule[lhs_,rhs_]:=makeReplaceRule[{OrderlessPatternSequence@@lhs},Splice@rhs]
SubsetReplaceList // ClearAllSubsetReplaceList[list_List, rule_ ? RuleQ] := SubsetReplace[list, # -> Replace[#, rule]] & /@ DeleteDuplicates @ ResourceFunction["SelectSubsets"][list, MatchQ[First[rule]]]
MultiSubsetReplace // ClearAllMultiSubsetReplace[list_List, rule_ ? RuleQ] := AssociationMap[SubsetReplace[list, # -> Replace[#, rule]] &, DeleteDuplicates @ ResourceFunction["SelectSubsets"][list, MatchQ[First[rule]]]]
In[]:=
Options[substitutionLemmasWM]={Heads->False,"Identity"->False,"Uniquify"->False,"Canonicalize"->False};substitutionLemmasWM[expr_List,rule_?RuleQ,OptionsPattern[]]:=Cond[TrueQ@OptionValue["Canonicalize"],canonicalizePatterns]/@MultiSubsetReplace[expr,Cond[TrueQ@OptionValue["Uniquify"],ReplacePart[#,{2}->Block[{$ModuleNumber=1},uniquifyPatterns[Extract[#,{2}]]]]&][rule]]substitutionLemmasWM[lhs_List<->rhs_List,rule_?RuleQ,OptionsPattern[]]:=With[{newRule=Cond[TrueQ@OptionValue["Uniquify"],ReplacePart[#,{2}->Block[{$ModuleNumber=1},uniquifyPatterns[Extract[#,{2}]]]]&][rule]},Cond[TrueQ@OptionValue["Canonicalize"],canonicalizePatterns]/@Join[#<->rhs&/@KeyMap[{{1},#}&]@MultiSubsetReplace[lhs,newRule],lhs<->#&/@KeyMap[{{2},#}&]@MultiSubsetReplace[rhs,newRule]]]substitutionLemmasWM[expr_,twr_TwoWayRule,opts:OptionsPattern[]]:=Association@@{KeyMap[Prepend[Right]]@substitutionLemmasWM[expr,makeHypergraphRule@@twr,opts],KeyMap[Prepend[Left]]@substitutionLemmasWM[expr,makeHypergraphRule@@Reverse@twr,opts],If[TrueQ@OptionValue["Identity"],{None,{},1}->expr,Nothing]}substitutionLemmasWM[expr_,rules_List,opts:OptionsPattern[]]:=Association@MapIndexed[{rule,pos}|->KeyMap[Prepend[First@pos],substitutionLemmasWM[expr,rule,opts]],rules]substitutionLemmasWM[rule:_TwoWayRule|_?RuleQ|_List,opts:OptionsPattern[]][expr_]:=substitutionLemmasWM[expr,rule,opts]
In[]:=
wm22=;
In[]:=
GraphicsRow[ResourceFunction["TokenEventGraph"][{u_,v_}:>Join[Values[substitutionLemmasWM[u,PrepWMRule@v,"Uniquify"->True,"Canonicalize"->True]],Values[substitutionLemmasWM[v,PrepWMRule@u,"Uniquify"->True,"Canonicalize"->True]]],#,1,"TokenMultiplicity"->Automatic,"TokenLabeling"->True,"EventDeduplication"->True,"TokenRenderingFunction"->Map[ResourceFunction["WolframModelPlot"][#,ImageSize->32]&]]&/@RandomSample[TwoWayRule@@@wm22,3],ImageSizeFull]
Out[]=
In[]:=
substitutionLemmasWM[{{1,2}}<->{{1,2},{2,3}},PrepWMRule[{{1,2}}<->{{1,2},{2,3}}],"Uniquify"->True,"Canonicalize"->True]
Out[]=
{Right,{1},{{1,2}}}{{1,2},{2,3}}{{1,2},{2,{3,4,4,4,4,4}}},{Right,{2},{{1,2}}}{{1,2}}{{1,2},{1,{2,3,3,3,3,3}},{4,1}},{Right,{2},{{2,3}}}{{1,2}}{{1,2},{2,3},{3,{3,4,4,4,4,4}}},{Left,{2},{{1,2},{2,3}}}{{1,2}}{{1,2}}
In[]:=
ResourceFunction["TokenEventGraph"][{u_,v_}:>Join[Values[substitutionLemmasWM[u,PrepWMRule@v,"Uniquify"->True,"Canonicalize"->True]],Values[substitutionLemmasWM[v,PrepWMRule@u,"Uniquify"->True,"Canonicalize"->True]]],{{1,2}}<->{{1,2},{2,3}},2,"TokenMultiplicity"->Automatic,"TokenLabeling"->True,"EventDeduplication"->True,"TokenRenderingFunction"->Map[ResourceFunction["WolframModelPlot"][#,ImageSize->32]&],GraphLayout->"SpringElectricalEmbedding"]
Out[]=
In[]:=
ResourceFunction["TokenEventGraph"][{u_,v_}:>Join[Values[substitutionLemmasWM[u,PrepWMRule@v,"Uniquify"->True,"Canonicalize"->True]],Values[substitutionLemmasWM[v,PrepWMRule@u,"Uniquify"->True,"Canonicalize"->True]]],{{1,2}}<->{{1,2},{2,3}},2,"TokenMultiplicity"->Automatic,"TokenLabeling"->False,"EventDeduplication"->True,"TokenRenderingFunction"->Map[ResourceFunction["WolframModelPlot"][#,ImageSize->32]&],GraphLayout->"SpringElectricalEmbedding"]