In[]:=
teg=ResourceFunction["TokenEventGraph"][{{u_,v_}:>Values[substitutionLemmas[u,v,"Uniquify"->True,"Canonicalize"->True]]},{(a_·b_)<->(b_)},3,"TokenLabeling"->False,"TokenMultiplicity"->Automatic,"EventDeduplication"->True,AspectRatio->1];​​labeledTeg=ResourceFunction["TokenEventGraph"][{{u_,v_}:>Values[substitutionLemmas[u,v,"Uniquify"->True,"Canonicalize"->True]]},{(a_·b_)<->(b_)},3,"TokenLabeling"->True,"TokenMultiplicity"->Automatic,"EventDeduplication"->True,AspectRatio->1];
In[]:=
teg
Out[]=
In[]:=
HighlightGraph[EdgeFix[teg],Style[twoWayRuleFix[a_·(b_·(c_·(d_·(e_·((f_·(g_·h_))·i_)))))i_],Red,PointSize[.03]]]
Out[]=
In[]:=
proof=findProof[EdgeFix@teg,{(a·b)↔(b)},a·(b·(c·(d·(e·((f·(g·h))·i)))))↔i(*a·(b·(c·(d·((e·f)·g))))↔h·(i·g)*)(*a·(b·((c·d)·((e·f)·g)))↔h·(i·g)*)]
Out[]=
{(a·b↔b){Event,1,1},(a·b↔b){Event,1,1},(a·b↔b){Event,1,519},(a·b↔b){Event,1,519},(a·(b·c)↔c){Event,1,3},(a·(b·c)↔c){Event,1,15},(a·(b·c)↔c){Event,1,15},(a·(b·(c·(d·e)))↔e){Event,1,616},(a·((b·(c·d))·e)↔e){Event,1,616},((a·b)·c↔c){Event,1,3},((a·b)·c↔d·(e·c)){Event,1,460},((a·b)·(c·(d·e))↔e){Event,1,460},{Event,1,1}(a·(b·c)↔c),{Event,1,3}((a·b)·c↔d·(e·c)),{Event,1,3}((a·b)·(c·(d·e))↔e),{Event,1,15}(a·((b·(c·d))·e)↔e),{Event,1,460}(a·(b·(c·(d·e)))↔e),{Event,1,519}((a·b)·c↔c),{Event,1,616}(a·(b·(c·(d·(e·((f·(g·h))·i)))))↔i)}
In[]:=
ResourceFunction["MultiwaySystem"][{"AB"->"B","B"->"AB"},{"AB","B"},3,"StatesGraph"]
Out[]=
"ABB"
{lhs,rhs}
In[]:=
Clear[StringApply]
In[]:=
StringApply[lhs1_->rhs1_,lhs2_->rhs2_]:=Rule@@@Tuples[{Prepend[StringReplaceList[lhs2,lhs1->rhs1],lhs2],Prepend[StringReplaceList[rhs2,lhs1->rhs1],rhs2]}]
In[]:=
StringApply["AB"->"A","ABAB"->"ABA"]
Out[]=
{ABABABA,ABABAA,AABABA,AABAA,ABAABA,ABAAA}
In[]:=
NestList[Union[Flatten[{#,Outer[StringApply,#,#]}]]&,{"A"->"AA","AA"->"A"},2]
Out[]=
{{AAA,AAA},{AA,AAA,AAAA,AAA,AAAA,AAAAA,AAAA,AAAAA},{AA,AAA,AAAA,AAAAA,AAAAAA,AAA,AAAA,AAAAA,AAAAAA,AAAAAAA,AAAA,AAAAA,AAAAAA,AAAAAAA,AAAAAAAA,AAAAA,AAAAAA,AAAAAAA,AAAAAAAA,AAAAAAAAA,AAAAAA,AAAAAAA,AAAAAAAA,AAAAAAAAA}}
In[]:=
NestList[Union[Flatten[{#,Outer[StringApply,#,#]}]]&,{"A"->"AA"},2]
Out[]=
{{AAA},{AAA,AAAA,AAAA,AAAAA},{AAA,AAAA,AAAAA,AAAAAA,AAAA,AAAAA,AAAAAA,AAAAAAA,AAAAA,AAAAAA,AAAAAAA,AAAAAAAA,AAAAAA,AAAAAAA,AAAAAAAA,AAAAAAAAA}}
In[]:=
ResourceFunction["TokenEventGraph"][{{r1_Rule,r2_Rule}:>StringApply[r1,r2]},{"A"->"AA"},2,"TokenMultiplicity"->Automatic,AspectRatio->1]
Out[]=
In[]:=
ResourceFunction["TokenEventGraph"][{{r1_Rule,r2_Rule}:>StringApply[r1,r2]},{"A"->"AA"},1,"TokenMultiplicity"->Automatic,AspectRatio->1]
Out[]=
In[]:=
ResourceFunction["TokenEventGraph"][{{r1_Rule,r2_Rule}:>StringApply[r1,r2]},{"A"->"B"},2,"TokenMultiplicity"->Automatic,AspectRatio->1]
Out[]=

[Whatever you start from, you get “reflexivity” A↔A ]

[[ Strings have the extra features that they can be spliced at any point ]] [[ whereas expressions with binary operators can only have “predefined subtrees” extracted ]]

Ruliology of Accumulative String-Rule Substitution Systems

[[ similar to multiway based on numbers ]]

Proofs on Strings

Something is wrong with this::::

Writing out a proof

rule XXX applied to XXX gives XXX [[ the rule is applied at position ____ ]]

Application to Hypergraphs

link-eme

Alternative view of strings

Then there is a metarule picks up linked pieces

Analogy

combinators / WM : machine code

string rewrites / symbolic system : assembler [still has names]

Identifying high-level constructs from the machine code is reverse engineering

Analog of particles is probably robust mathematical concepts

Estimate the Size of Mathematics

Metamath / LEAN : assembler
Machine code: take every identifier and represent it “in binary” [ emic ]

At a low level there may be lots of emes to create math ideas that are “obvious” from our physical experience

Just as lots of space emes [“spacemes”] are needed to build space

Math as it exists today vs. the region of physical space that we’ve explored

What fraction of math have we explored

Eme Level

An eme: a fundamental element with distinct “UUID” [“morpheme”]

Emic level [“morphological level”]

[[ Language of things you can make out of emes ]] [“morphology”] [ emology ] < rules at the eme level >

< What can happen at the eme level >