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[]=

"ABB"

{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[]=

{ABABABA,ABABAA,AABABA,AABAA,ABAABA,ABAAA}

In[]:=

NestList[Union[Flatten[{#,Outer[StringApply,#,#]}]]&,{"A"->"AA","AA"->"A"},2]

Out[]=

{{AAA,AAA},{AA,AAA,AAAA,AAA,AAAA,AAAAA,AAAA,AAAAA},{AA,AAA,AAAA,AAAAA,AAAAAA,AAA,AAAA,AAAAA,AAAAAA,AAAAAAA,AAAA,AAAAA,AAAAAA,AAAAAAA,AAAAAAAA,AAAAA,AAAAAA,AAAAAAA,AAAAAAAA,AAAAAAAAA,AAAAAA,AAAAAAA,AAAAAAAA,AAAAAAAAA}}

In[]:=

NestList[Union[Flatten[{#,Outer[StringApply,#,#]}]]&,{"A"->"AA"},2]

Out[]=

{{AAA},{AAA,AAAA,AAAA,AAAAA},{AAA,AAAA,AAAAA,AAAAAA,AAAA,AAAAA,AAAAAA,AAAAAAA,AAAAA,AAAAAA,AAAAAAA,AAAAAAAA,AAAAAA,AAAAAAA,AAAAAAAA,AAAAAAAAA}}

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 ]

[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 ]]

[[ 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

Ruliology of Accumulative String-Rule Substitution Systems

#### [[ similar to multiway based on numbers ]]

[[ similar to multiway based on numbers ]]

## Proofs on Strings

Proofs on Strings

Something is wrong with this::::

### Writing out a proof

Writing out a proof

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

## Application to Hypergraphs

Application to Hypergraphs

link-eme

#### Alternative view of strings

Alternative view of strings

Then there is a metarule picks up linked pieces

## Analogy

Analogy

#### combinators / WM : machine code

combinators / WM : machine code

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

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

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

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

### Analog of particles is probably robust mathematical concepts

Analog of particles is probably robust mathematical concepts

## Estimate the Size of Mathematics

Estimate the Size of Mathematics

#### Metamath / LEAN : assembler

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

Metamath / LEAN : assembler

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

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

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

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

### What fraction of math have we explored

What fraction of math have we explored

## Eme Level

Eme Level

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

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

### Emic level [“morphological level”]

Emic level [“morphological level”]

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

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

### < What can happen at the eme level >

< What can happen at the eme level >