In[]:=
thms=Flatten[ResourceFunction["EnumerateSubstitutionSystemRules"][#,2]&/@(List/@Rule@@@Catenate[Table[IntegerPartitions[n,{2}],{n,5}]])]/.RuleTwoWayRule
Out[]=
{AA,AB,AAA,AAB,ABA,AAAA,AAAB,AABA,AABB,ABAA,ABAB,AAAA,AAAB,AABB,ABAA,ABAB,ABBA,AAAAA,AAAAB,AAABA,AAABB,AABAA,AABAB,AABBA,ABABA,ABBAA,ABBAB,AAAAA,AAAAB,AAABB,AABAA,AABAB,AABBA,AABBB,ABAAA,ABAAB,ABABB}
In[]:=
rulesx1=ResourceFunction["EnumerateSubstitutionSystemRules"][{12,21},2]/.RuleTwoWayRule
Out[]=
{{AAA,AAA},{AAA,AAB},{AAA,ABA},{AAA,ABB},{AAA,BBA},{AAA,BBB},{AAB,AAA},{AAB,AAB},{AAB,ABA},{AAB,ABB},{AAB,BAA},{AAB,BAB},{AAB,BBA},{AAB,BBB},{ABB,AAA},{ABB,AAB},{ABB,ABA},{ABB,ABB},{ABB,BBA},{ABB,BBB}}
In[]:=
Outer[ResourceFunction["FindStringProof"][#2,#1]&,rulesx1,thms,1]
FindEquationalProof
:Invalid specification of propositions {True} and axioms AA⊙A,A⊙AA,
∀
{a.,b.,c.}
a.⊙(b.⊙c.)(a.⊙b.)⊙c..
FindEquationalProof
:Invalid specification of propositions {True} and axioms AA⊙A,A⊙AA,
∀
{a.,b.,c.}
a.⊙(b.⊙c.)(a.⊙b.)⊙c..
FindEquationalProof
:Invalid specification of propositions {True} and axioms AA⊙A,A⊙AA,
∀
{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[]=
{{AAA,AAA}{0,∞,3,∞,∞,4,∞,∞,∞,∞,∞,0,∞,∞,∞,0,∞,5,∞,∞,∞,∞,∞,∞,∞,∞,∞,3,∞,∞,∞,5,∞,∞,∞,∞,∞},{AAA,AAB}{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},{AAA,ABA}{0,∞,3,∞,3,4,∞,5,∞,7,∞,0,7,∞,7,0,∞,5,∞,12,∞,9,∞,8,8,9,∞,3,6,∞,3,5,∞,∞,9,9,∞},{AAA,ABB}{0,∞,3,∞,∞,4,∞,∞,4,∞,∞,0,∞,∞,∞,0,∞,5,∞,∞,8,∞,∞,∞,∞,∞,∞,3,∞,∞,∞,5,∞,∞,∞,∞,∞},{AAA,BBA}{0,∞,3,∞,∞,4,∞,∞,∞,∞,∞,0,∞,5,∞,0,6,5,∞,∞,∞,∞,∞,12,14,13,∞,3,∞,6,∞,5,9,∞,∞,9,∞},{AAA,BBB}{0,∞,3,∞,∞,4,∞,∞,∞,∞,∞,0,∞,∞,∞,0,∞,5,∞,∞,∞,∞,∞,∞,∞,∞,∞,3,∞,∞,∞,5,∞,∞,∞,∞,∞},{AAB,AAA}{0,∞,3,∞,3,4,∞,5,∞,7,∞,0,7,∞,7,0,∞,5,∞,12,∞,9,∞,8,8,9,∞,3,6,∞,3,5,∞,∞,9,9,∞},{AAB,AAB}{0,∞,∞,3,3,5,∞,∞,5,∞,9,0,∞,7,∞,0,6,∞,6,6,∞,10,∞,∞,∞,∞,11,∞,3,∞,3,∞,∞,5,8,∞,8},{AAB,ABA}{0,∞,∞,∞,3,∞,∞,∞,∞,∞,∞,0,∞,∞,∞,0,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,3,∞,∞,∞,5,∞,∞},{AAB,ABB}{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},{AAB,BAA}{0,∞,∞,∞,3,∞,∞,∞,∞,∞,∞,0,∞,∞,∞,0,5,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,3,∞,∞,∞,5,∞,∞},{AAB,BAB}{0,∞,8,∞,3,10,∞,9,∞,5,∞,0,7,∞,7,0,∞,11,∞,13,∞,12,∞,13,6,10,∞,8,9,∞,3,8,∞,∞,5,3,∞},{AAB,BBA}{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},{AAB,BBB}{0,∞,∞,∞,3,∞,∞,∞,∞,∞,∞,0,∞,∞,∞,0,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,3,∞,∞,∞,5,∞,∞},{ABB,AAA}{0,∞,3,∞,∞,4,∞,∞,∞,∞,∞,0,∞,5,∞,0,6,5,∞,∞,∞,∞,∞,12,14,13,∞,3,∞,6,∞,5,9,∞,∞,9,∞},{ABB,AAB}{0,∞,∞,3,∞,∞,∞,7,∞,12,∞,0,∞,∞,∞,0,6,8,∞,∞,8,∞,13,∞,∞,∞,∞,∞,3,∞,∞,∞,∞,5,∞,∞,11},{ABB,ABA}{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},{ABB,ABB}{0,∞,8,∞,∞,13,∞,∞,4,∞,9,0,∞,7,∞,0,6,16,∞,∞,8,∞,10,14,8,13,∞,10,∞,12,∞,3,8,∞,∞,9,∞},{ABB,BBA}{0,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,0,∞,∞,∞,0,6,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞,∞},{ABB,BBB}{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[]=
{AAABA,AAABB,AABAA,AABAB}
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 ...