WOLFRAM NOTEBOOK

In[]:=
thms=Flatten[ResourceFunction["EnumerateSubstitutionSystemRules"][#,2]&/@(List/@Rule@@@Catenate[Table[IntegerPartitions[n,{2}],{n,5}]])]/.RuleTwoWayRule
Out[]=
{AA,AB,AAA,AAB,ABA,AAAA,AAAB,AABA,AABB,ABAA,ABAB,AAAA,AAAB,AABB,ABAA,ABAB,ABBA,AAAAA,AAAAB,AAABA,AAABB,AABAA,AABAB,AABBA,ABABA,ABBAA,ABBAB,AAAAA,AAAAB,AAABB,AABAA,AABAB,AABBA,AABBB,ABAAA,ABAAB,ABABB}
In[]:=
rulesx1=ResourceFunction["EnumerateSubstitutionSystemRules"][{12,21},2]/.RuleTwoWayRule
Out[]=
{{AAA,AAA},{AAA,AAB},{AAA,ABA},{AAA,ABB},{AAA,BBA},{AAA,BBB},{AAB,AAA},{AAB,AAB},{AAB,ABA},{AAB,ABB},{AAB,BAA},{AAB,BAB},{AAB,BBA},{AAB,BBB},{ABB,AAA},{ABB,AAB},{ABB,ABA},{ABB,ABB},{ABB,BBA},{ABB,BBB}}
In[]:=
Outer[ResourceFunction["FindStringProof"][#2,#1]&,rulesx1,thms,1]
FindEquationalProof
:Invalid specification of propositions {True} and axioms AAA,AAA,
{a.,b.,c.}
a.(b.c.)(a.b.)c..
FindEquationalProof
:Invalid specification of propositions {True} and axioms AAA,AAA,
{a.,b.,c.}
a.(b.c.)(a.b.)c..
FindEquationalProof
:Invalid specification of propositions {True} and axioms AAA,AAA,
{a.,b.,c.}
a.(b.c.)(a.b.)c..
General
:Further output of FindEquationalProof::invs will be suppressed during this calculation.
Out[]=
$Aborted
In[]:=
ResourceFunction["ParallelMapMonitored"][Function[ru,ResourceFunction["FindStringProof"][#,ru]&/@thms],rulesx1]
In[]:=
Map[If[Head[#]===FindEquationalProof,0,If[Head[#]===Failure,Infinity,#["ProofLength"]]]&,%,{2}]
Out[]=
{{0,,3,,,4,,,,,,0,,,,0,,5,,,,,,,,,,3,,,,5,,,,,},{0,5,3,6,6,4,7,11,11,11,11,0,5,6,5,0,6,5,8,13,13,13,13,12,12,12,12,3,8,7,6,5,7,10,6,9,10},{0,,3,,3,4,,5,,7,,0,7,,7,0,,5,,12,,9,,8,8,9,,3,6,,3,5,,,9,9,},{0,,3,,,4,,,4,,,0,,,,0,,5,,,8,,,,,,,3,,,,5,,,,,},{0,,3,,,4,,,,,,0,,5,,0,6,5,,,,,,12,14,13,,3,,6,,5,9,,,9,},{0,,3,,,4,,,,,,0,,,,0,,5,,,,,,,,,,3,,,,5,,,,,},{0,,3,,3,4,,5,,7,,0,7,,7,0,,5,,12,,9,,8,8,9,,3,6,,3,5,,,9,9,},{0,,,3,3,5,,,5,,9,0,,7,,0,6,,6,6,,10,,,,,11,,3,,3,,,5,8,,8},{0,,,,3,,,,,,,0,,,,0,,,,,,,,,,,,,,,3,,,,5,,},{0,5,6,9,3,10,11,7,10,9,10,0,5,6,5,0,6,12,13,11,12,11,12,10,10,10,11,8,9,10,3,8,6,7,5,8,9},{0,,,,3,,,,,,,0,,,,0,5,,,,,,,,,,,,,,3,,,,5,,},{0,,8,,3,10,,9,,5,,0,7,,7,0,,11,,13,,12,,13,6,10,,8,9,,3,8,,,5,3,},{0,,8,,3,9,,9,,9,,0,7,9,7,0,11,10,,12,,13,,11,10,10,,8,12,10,3,8,13,10,5,9,10},{0,,,,3,,,,,,,0,,,,0,,,,,,,,,,,,,,,3,,,,5,,},{0,,3,,,4,,,,,,0,,5,,0,6,5,,,,,,12,14,13,,3,,6,,5,9,,,9,},{0,,,3,,,,7,,12,,0,,,,0,6,8,,,8,,13,,,,,,3,,,,,5,,,11},{0,,8,,3,9,,9,,9,,0,7,9,7,0,11,10,,12,,13,,11,10,10,,8,12,10,3,8,13,10,5,9,10},{0,,8,,,13,,,4,,9,0,,7,,0,6,16,,,8,,10,14,8,13,,10,,12,,3,8,,,9,},{0,,,,,,,,,,,0,,,,0,6,,,,,,,,,,,,,,,,,,,,},{0,5,8,7,9,9,11,10,12,10,12,0,5,6,5,0,6,14,12,13,12,13,12,11,14,14,13,8,7,8,9,6,10,7,9,6,7}}
In[]:=
Thread[rulesx1%]
Out[]=
{{AAA,AAA}{0,,3,,,4,,,,,,0,,,,0,,5,,,,,,,,,,3,,,,5,,,,,},{AAA,AAB}{0,5,3,6,6,4,7,11,11,11,11,0,5,6,5,0,6,5,8,13,13,13,13,12,12,12,12,3,8,7,6,5,7,10,6,9,10},{AAA,ABA}{0,,3,,3,4,,5,,7,,0,7,,7,0,,5,,12,,9,,8,8,9,,3,6,,3,5,,,9,9,},{AAA,ABB}{0,,3,,,4,,,4,,,0,,,,0,,5,,,8,,,,,,,3,,,,5,,,,,},{AAA,BBA}{0,,3,,,4,,,,,,0,,5,,0,6,5,,,,,,12,14,13,,3,,6,,5,9,,,9,},{AAA,BBB}{0,,3,,,4,,,,,,0,,,,0,,5,,,,,,,,,,3,,,,5,,,,,},{AAB,AAA}{0,,3,,3,4,,5,,7,,0,7,,7,0,,5,,12,,9,,8,8,9,,3,6,,3,5,,,9,9,},{AAB,AAB}{0,,,3,3,5,,,5,,9,0,,7,,0,6,,6,6,,10,,,,,11,,3,,3,,,5,8,,8},{AAB,ABA}{0,,,,3,,,,,,,0,,,,0,,,,,,,,,,,,,,,3,,,,5,,},{AAB,ABB}{0,5,6,9,3,10,11,7,10,9,10,0,5,6,5,0,6,12,13,11,12,11,12,10,10,10,11,8,9,10,3,8,6,7,5,8,9},{AAB,BAA}{0,,,,3,,,,,,,0,,,,0,5,,,,,,,,,,,,,,3,,,,5,,},{AAB,BAB}{0,,8,,3,10,,9,,5,,0,7,,7,0,,11,,13,,12,,13,6,10,,8,9,,3,8,,,5,3,},{AAB,BBA}{0,,8,,3,9,,9,,9,,0,7,9,7,0,11,10,,12,,13,,11,10,10,,8,12,10,3,8,13,10,5,9,10},{AAB,BBB}{0,,,,3,,,,,,,0,,,,0,,,,,,,,,,,,,,,3,,,,5,,},{ABB,AAA}{0,,3,,,4,,,,,,0,,5,,0,6,5,,,,,,12,14,13,,3,,6,,5,9,,,9,},{ABB,AAB}{0,,,3,,,,7,,12,,0,,,,0,6,8,,,8,,13,,,,,,3,,,,,5,,,11},{ABB,ABA}{0,,8,,3,9,,9,,9,,0,7,9,7,0,11,10,,12,,13,,11,10,10,,8,12,10,3,8,13,10,5,9,10},{ABB,ABB}{0,,8,,,13,,,4,,9,0,,7,,0,6,16,,,8,,10,14,8,13,,10,,12,,3,8,,,9,},{ABB,BBA}{0,,,,,,,,,,,0,,,,0,6,,,,,,,,,,,,,,,,,,,,},{ABB,BBB}{0,5,8,7,9,9,11,10,12,10,12,0,5,6,5,0,6,14,12,13,12,13,12,11,14,14,13,8,7,8,9,6,10,7,9,6,7}}
In[]:=
ResourceFunction["MultiwaySystem"][{"A""AA","AA""B"},{"A"},7,"StatesGraph"]
Out[]=
In[]:=
ResourceFunction["MultiwaySystem"][{"A"->"AA","AA""B","AA""A","B""AA"},{"A"},7,"StatesGraph"]//LayeredGraphPlot
Out[]=
In[]:=
Extract[thms,Position[{0,5,3,6,6,4,7,11,11,11,11,0,5,6,5,0,6,5,8,13,13,13,13,12,12,12,12,3,8,7,6,5,7,10,6,9,10},13]]
Out[]=
{AAABA,AAABB,AABAA,AABAB}
In[]:=
With[{g=ResourceFunction["MultiwaySystem"][{"A"->"AA","AA""B","AA""A","B""AA"},{"A"},7,"StatesGraph"]},HighlightGraph[g,Subgraph[g,PathGraph[FindShortestPath[g,"A","AAAB"]]]]]
Out[]=
In[]:=
With[{g=ResourceFunction["FindStringProof"]["A""AAAB",{"A"->"AA","AA""B","AA""A","B""AA"}]["ProofGraph"]},Graph[g,VertexSize.1,VertexLabels(#[[1]]Placed[(#[[2,1,2,1,2]]//.CircleDot[a_,b_]Row[{a,b}]),Center]&/@Options[g,"AnnotationRules"][[1,2]])]]

Applying rules to equations, rather than terms ...

Wolfram Cloud

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 »

You are using a browser not supported by the Wolfram Cloud. Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.