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 // ClearAll​​SubsetReplaceList[list_List, rule_ ? RuleQ] :=​​ SubsetReplace[list, # -> Replace[#, rule]] & /@ DeleteDuplicates @ ResourceFunction["SelectSubsets"][list, MatchQ[First[rule]]]
MultiSubsetReplace // ClearAll​​MultiSubsetReplace[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=
wm22
Head: List
Length: 562
Byte count: 296848
;
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],ImageSizeFull]
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"]