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
exprlhs->rhs
Position[expr,lhs]vsPosition[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_⊗1,a_⊗1,"Canonicalize"->True]
a_
a_
Out[]=
{{Right,Right},{1}}1⊗1,{{Right,Right},{2,1}}(a_⊗)⊗1,{{Right,Right},{}}11,{{Right,Left},{1}}(a_⊗)⊗1,{{Right,Left},{2,1}}1⊗1,{{Left,Left},{}}a_⊗b_⊗
a_⊗
a_
a_
1
a_
1
a_⊗
a_
a_
b_
In[]:=
coSubstitutionLemmas[a_⊗1,1->a_⊗,"Canonicalize"->True]
a_
a_
Out[]=
{{1,1},1}(1⊗)⊗1,{{1,2,1},1}1⊗1,{{2},1}a_⊗a_⊗
1
1
1⊗
1
a_
a_
In[]:=
substitutionLemmas[a_⊗1,a_⊗1,"Canonicalize"->True]
a_
a_
Out[]=
{Right,{1},1}11,{Left,{2},1}a_⊗b_⊗
a_
b_