Out[]=
Cosubstitution - series of related substitutions
Out[]=
In[]:=
ResourceFunction["MultiReplace"][f[1,f[2,3]],f[___,x_,___]x]
Out[]=
{2}{f[1,2],f[1,3]},{}{1,f[2,3]}
In[]:=
MultiCoReplace[f[___,x_,___],f[1,f[2,3]]x,"OuterMatchPattern"->Except[_Pattern]]
Out[]=
{1}{f[x,x_,___]},{2}{f[___,f[1,f[2,3]],___]},{3}{f[___,x_,x]},{}{1,f[2,3]}
In[]:=
MultiUnify[f[___,x_,___],f[1,f[2,3]],"OuterMatchPattern"->Except[_Pattern]]
Out[]=
{1}{},{2}{x_f[1,f[2,3]]},{3}{},{}{x_f[2,3]}
In[]:=
MultiUnify[f[x_,y_],f[y_,x_]]
Out[]=
{1,2}{},{1}{x_f[y_,x_]},{2,2}{},{2}{y_f[y_,x_]},{}{x_y_,y_x_}
In[]:=
MatchQ[y_,g[x_]]
Out[]=
False
In[]:=
MultiUnify[f[g[x_],y_],f[y_,h[x_]]]
Out[]=
{1,1,2}{},{1,1}{x_f[y_,h[x_]]},{2,2}{},{2}{y_f[y_,h[x_]]}
f[x_,y_]​​z_->z
expr​​lhs->rhs
Position[expr,lhs]​​vs​​Position[expr,subpatt_/;MatchQ[lhs,subpatt]]
teddy[brown]->blob
In[]:=
TreePosition[​​Tree[star,{teddy[color_],ball[surface_],snowflake[color_]}],ornament_/;MatchQ[teddy[brown],ornament]]
Out[]=
{{1}}
In[]:=
Tree[star,{teddy[brown],ball[surface_],snowflake[brown]}]
Out[]=
teddy[brown]->blob
In[]:=
Tree[star,{blob,ball[surface_],snowflake[brown]}]
Out[]=
In[]:=
Position[f[g[x_],y_],g[z_]]​​ReplacePart[f[g[x_],y_],{1}->XXX]
Out[]=
{{1}}
Out[]=
f[XXX,y_]
In[]:=
Position[f[g[x_],x_],subpatt_/;MatchQ[g[z_],subpatt]&&Head[subpatt]=!=Pattern&&subpatt=!=Blank[]]​​f[g[x_],x_]/.Verbatim[x_]->z_​​ReplacePart[f[g[z_],z_],{1}->XXX]
Out[]=
{{1}}
Out[]=
f[g[z_],z_]
Out[]=
f[XXX,z_]
In[]:=
MultiUnify[f[x_,y_],z_]
Out[]=
{1,2}{},{1}{x_z_},{2,2}{},{2}{y_z_}
In[]:=
{1}{x_z_}
Out[]=
{1}{x_z_}
In[]:=
f[x_,y_]/.{Verbatim[x_]z_}
Out[]=
f[z_,y_]
In[]:=
f[Replace[z_,x_->z],y_]
Out[]=
f[z,y_]
In[]:=
MultiCoReplace[f[g[x_],y_,y_],f[y_,h[x_]]->y,"OuterMatchPattern"->Except[_Pattern]]
Out[]=
{1,1}{f[g[y],y_,y_]},{2}{f[g[x_],f[y_,h[x_]],f[y_,h[x_]]]},{3}{f[g[x_],f[y_,h[x_]],f[y_,h[x_]]]}
In[]:=
MultiUnify[f[x_,y_],f[1,f[2,x_]],"OuterMatchPattern"->Except[_Pattern]]
Out[]=
{1}{x_f[1,f[2,x_]]},{2}{y_f[1,f[2,x_]]},{}{x_1,y_f[2,x_]}
In[]:=
MultiUnify[f[g[x_],y_,g[x_]],g[x_],"OuterMatchPattern"->Except[_Pattern]]
Out[]=
{1,1}{x_g[x_]},{1}{x_x_},{2}{y_g[x_]},{3,1}{x_g[x_]},{3}{x_x_}
In[]:=
Values@coSubstitutionLemmas[f[g[x_],y_,g[x_]]->1,g[x_]->h[x_]]
Out[]=
{f[g[h[g[x_]]],y_,g[g[x_]]]1,f[h[x_],y_,g[x_]]1,f[g[x_],h[x_],g[x_]]1,f[g[g[x_]],y_,g[h[g[x_]]]]1,f[g[x_],y_,h[x_]]1}
In[]:=
Values@criticalPairLemmas[f[g[x_],y_,g[x_]]->1,g[x_]->h[x_],"Canonicalize"->True]
Out[]=
{f[g[h[a_]],b_,g[g[a_]]]1,f[h[a_],b_,g[a_]]1,f[g[a_],h[b_],g[a_]]1,f[g[g[a_]],b_,g[h[a_]]]1,f[g[a_],b_,h[a_]]1}
In[]:=
criticalPairLemmas[a_⊗
a_
1,a_⊗
a_
1,"Canonicalize"->True]
Out[]=
{{Right,Right},{1}}1⊗
a_⊗
a_
1,{{Right,Right},{2,1}}(a_⊗
a_
)⊗
1
1,{{Right,Right},{}}11,{{Right,Left},{1}}(a_⊗
a_
)⊗
1
1,{{Right,Left},{2,1}}1⊗
a_⊗
a_
1,{{Left,Left},{}}a_⊗
a_
b_⊗
b_

In[]:=
coSubstitutionLemmas[a_⊗
a_
1,1->a_⊗
a_
,"Canonicalize"->True]
Out[]=
{{1,1},1}(1⊗
1
)⊗
1
1,{{1,2,1},1}1⊗
1⊗
1
1,{{2},1}a_⊗
a_
a_⊗
a_

In[]:=
substitutionLemmas[a_⊗
a_
1,a_⊗
a_
1,"Canonicalize"->True]
Out[]=
{Right,{1},1}11,{Left,{2},1}a_⊗
a_
b_⊗
b_
