From Jonathan:

In[]:=
convertStringToOperator[string_String]:=Module[{expression,list},​​list=StringSplit[string,""];​​expression=list;​​While[Length[list]>1,​​expression=expression/.list(CenterDot[First[list],Rest[list]]);​​list=Rest[list]];​​expression/.listFirst[list]]​​FindStringProof[theorems_List,axioms_List]:=Module[{stringTheorems,stringAxioms},​​stringTheorems=(convertStringToOperator[First[#]]==convertStringToOperator[Last[#]])&/@theorems;​​stringAxioms=(convertStringToOperator[First[#]]==convertStringToOperator[Last[#]])&/@axioms;​​FindEquationalProof[stringTheorems,Join[{stringAxioms,ForAll[{a,b,c},CenterDot[a,CenterDot[b,c]]CenterDot[CenterDot[a,b],c]]}]]]​​FindStringProof[theorem_,axioms_List]:=FindStringProof[{theorem},axioms]/;!ListQ[theorem]​​FindStringProof[theorems_List,axiom_]:=FindStringProof[theorems,{axiom}]/;!ListQ[axiom]​​FindStringProof[theorem_,axiom_]:=FindStringProof[{theorem},{axiom}]/;(!ListQ[theorem]&&!ListQ[axiom])
In[]:=
FindStringProof[{"AA""AABBBB"},{"A""AB"}]
Out[]=
ProofObject
Logic: EquationalLogic
Steps: 11
Theorem: A·AA·(A·(B·(B·(B·B))))

In[]:=
%["ProofGraph"]
Out[]=

More

Proof Diagram

In[]:=
StringProofDiagram[statements_,axioms_]:=With[{pf=FindStringProof[statements,axioms]},Graph[pf["ProofGraph"],VertexLabels->Thread[VertexList[pf["ProofGraph"]]->Map[#/.(s_Symbol:>ToString[StandardForm[Style[If[s=!=True,Subscript[StringTake[SymbolName[s],1],StringDrop[SymbolName[s],1]],True],Italic,Gray]]])&,Normal[Values[pf["ProofDataset"][All,"Statement"]]],{-1}]/.EqualLongLeftRightArrow/.CenterDotStringJoin],VertexSizeSmall]]
In[]:=
Graph[StringProofDiagram[{"AA""AABBBB"},{"A""AB"}]]
Out[]=
In[]:=
ResourceFunction["MultiwaySystem"][{"A""AB"},"AA",5,"StatesGraph"]
Out[]=

Causal Invariant Case

In[]:=
ResourceFunction["MultiwaySystem"][{"A""BBB","BB""A"},"A",5,"StatesGraph"]
Out[]=
In[]:=
StringProofDiagram[{"A""AA"},{"A""BBB","BB""A"}]
Out[]=

NKS Book Case

https://www.wolframscience.com/nks/p776--implications-for-mathematics-and-its-foundations/
(This doesn’t seem to involve the very shortest strings)

Long Path Cases

Consider Equational Multiway Systems

Model Theory for Strings

Allow any x·y for any k-ary function, assuming it is associative......
[ Think of in terms of a monoid FSM ? ]