Decidability of a theory implies a bound on the lengths of proofs

[ How long is the bound? Does it depend on the expressions? ]

Expr  Expr vs. Theorem(s)  Theorem

ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},5,"StatesGraph"]
In[]:=
Out[]=
ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},5,"EvolutionEventsGraph"]
In[]:=
Out[]=
ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},5,"EvolutionCausalGraph"]
In[]:=
Out[]=

Pick out “Interesting” Theorems

Which cannot be deduced from ones earlier in the list? For Exprs, ask what the order of sizes are
ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},7]
In[]:=
{{A},{AB},{ABB},{AA,ABBB},{AAB,ABA,ABBBB},{AABB,ABAB,ABBA,ABBBBB},{AAA,AABBB,ABABB,ABBAB,ABBBA,ABBBBBB},{AAAB,AABA,AABBBB,ABAA,ABABBB,ABBABB,ABBBAB,ABBBBA,ABBBBBBB}}
Out[]=

Rulial multiway graph

ResourceFunction["MultiwaySystem"][Flatten[ResourceFunction["EnumerateSubstitutionSystemRules"][{22},2]],ResourceFunction["StringTuples"]["AB",4],4,"StatesGraph"]//LayeredGraphPlot
In[]:=
Out[]=
This is only inequivalent rules.....
ResourceFunction["MultiwaySystem"][Flatten[ResourceFunction["EnumerateSubstitutionSystemRules"][{22},2]],ResourceFunction["StringTuples"]["AB",2],4,"StatesGraph"]//LayeredGraphPlot
In[]:=
Out[]=
ResourceFunction["EnumerateSubstitutionSystemRules"][{22},2]
In[]:=
{{AAAA},{AAAB},{AABB},{ABAA},{ABAB},{ABBA}}
Out[]=

All possible rules

Outer[Rule,ResourceFunction["StringTuples"]["AB",2],ResourceFunction["StringTuples"]["AB",2]]//Flatten
In[]:=
{AAAA,AAAB,AABA,AABB,ABAA,ABAB,ABBA,ABBB,BAAA,BAAB,BABA,BABB,BBAA,BBAB,BBBA,BBBB}
Out[]=
ResourceFunction["MultiwaySystem"][Outer[Rule,ResourceFunction["StringTuples"]["AB",2],ResourceFunction["StringTuples"]["AB",2]]//Flatten,ResourceFunction["StringTuples"]["AB",4],8,"StatesGraph"]
In[]:=
Out[]=

Single Multiway System

[ Can be thought of either as a fibration, or as a foliation ]

Theorem Lengths

Euclid