Cosubstitution
Cosubstitution
In[]:=
coSubstitutionLemmas[a_⊕b_b_⊕a_,x_⊕y_y_⊕x_]
Out[]=
{Right,{1,1},1}(y_⊕x_)⊕b_b_⊕(x_⊕y_),{Right,{1,2},1}a_⊕(y_⊕x_)(x_⊕y_)⊕a_,{Right,{1},1}y_⊕x_y_⊕x_,{Right,{2,1},1}a_⊕(x_⊕y_)(y_⊕x_)⊕a_,{Right,{2,2},1}(x_⊕y_)⊕b_b_⊕(y_⊕x_),{Right,{2},1}y_⊕x_y_⊕x_,{Left,{1,1},1}(x_⊕y_)⊕b_b_⊕(y_⊕x_),{Left,{1,2},1}a_⊕(x_⊕y_)(y_⊕x_)⊕a_,{Left,{1},1}x_⊕y_x_⊕y_,{Left,{2,1},1}a_⊕(y_⊕x_)(x_⊕y_)⊕a_,{Left,{2,2},1}(y_⊕x_)⊕b_b_⊕(x_⊕y_),{Left,{2},1}x_⊕y_x_⊕y_
In[]:=
coSubstitutionLemmas[a_b_,x_y_]
Out[]=
{Right,{1},1}y_b_,{Right,{2},1}a_y_,{Left,{1},1}x_b_,{Left,{2},1}a_x_
In[]:=
coSubstitutionLemmas[a_a_,x_y_]
Out[]=
{Right,{1},1}y_x_,{Right,{2},1}x_y_,{Left,{1},1}x_y_,{Left,{2},1}y_x_
In[]:=
coSubstitutionLemmas[a_a_⊕a_,x_y_]
Out[]=
{Right,{1},1}y_x_⊕x_,{Right,{2,1},1}x_y_⊕x_,{Right,{2,2},1}x_x_⊕y_,{Left,{1},1}x_y_⊕y_,{Left,{2,1},1}y_x_⊕y_,{Left,{2,2},1}y_y_⊕x_
These are non-accumulative
These are non-accumulative
In[]:=
NestGraph[Flatten[{Values[coSubstitutionLemmas[#,x_⊕y_y_⊕x_,"Uniquify"->True,"Canonicalize"->True]]}]&,a_⊕b_b_⊕a_,1,GraphLayout->"SpringElectricalEmbedding",VertexLabelsAutomatic]
Out[]=
In[]:=
NestGraph[Flatten[{Values[coSubstitutionLemmas[#,x_⊕y_y_⊕x_,"Canonicalize"->True]]}]&,a_⊕b_b_⊕a_,1,GraphLayout->"SpringElectricalEmbedding",VertexLabelsAutomatic]
Out[]=
In[]:=
NestGraph[Flatten[{Values[coSubstitutionLemmas[#,x_⊕y_y_⊕x_,"Canonicalize"->True]]}]&,a_⊕b_b_⊕a_,2,GraphLayout->"SpringElectricalEmbedding",VertexLabelsAutomatic]
Out[]=
In[]:=
NestGraph[Flatten[{Values[substitutionLemmas[#,x_⊕y_y_⊕x_,"Uniquify"->True,"Canonicalize"->True]]}]&,a_⊕b_b_⊕a_,1,GraphLayout->"SpringElectricalEmbedding",VertexLabelsAutomatic]
Out[]=
In[]:=
NestGraph[Flatten[{Values[substitutionLemmas[#,x_⊕y_y_⊕x_,"Uniquify"->True,"Canonicalize"->True]]}]&,a_⊕b_b_⊕a_,2,GraphLayout->"SpringElectricalEmbedding",VertexLabelsAutomatic]
Out[]=
In[]:=
NestGraph[Flatten[{Values[substitutionLemmas[#,x_⊕y_y_⊕x_,"Canonicalize"->True]]}]&,a_⊕b_b_⊕a_,2,GraphLayout->"SpringElectricalEmbedding",VertexLabelsAutomatic]
Out[]=
In[]:=
NestGraph[Flatten[{Values[coSubstitutionLemmas[#,x_⊕y_y_⊕x_,"Canonicalize"->True]]}]&,a_⊕b_b_⊕a_,3,GraphLayout->"SpringElectricalEmbedding"]
Out[]=
In[]:=
NestGraph[Flatten[{Values[coSubstitutionLemmas[#,x_⊕y_y_⊕x_,"Canonicalize"->True]]}]&,a_⊕b_b_⊕a_,4,GraphLayout->"SpringElectricalEmbedding",VertexLabels->Placed["Name",Tooltip]]
Out[]=
In[]:=
NestGraph[Flatten[{Values[coSubstitutionLemmas[#,x_⊕y_y_⊕x_,"Canonicalize"->True]]}]&,a_⊕b_b_⊕a_,4,GraphLayout->"LayeredDigraphEmbedding",AspectRatio1]
Out[]=
Accumulative case
Accumulative case
In[]:=
ResourceFunction["TokenEventGraph"][{{u_,v_}:>Values[substitutionLemmas[u,v,"Uniquify"->True,"Canonicalize"->True]]},{x_⊕y_y_⊕x_},1,"TokenLabeling"->False,"TokenMultiplicity"->Automatic,AspectRatio->1]
Out[]=
[[[ cell converted to bitmap to avoid absurd size ... ]]]
[[ Needs graph isomorphism ]]