```
S = ∀z r.result[res=adder(z,r)]
adder = ∀n m.result[case(m,n,result) = plus]
plus = ∀n m. if(m=0) then result[n] else result[s=plus(n, pred(m)), res=S(s)]
```
And so when we add 2 (S(S(0))) and 3 (S(S(S(0)))), we start with:
```
Z
|
S -> S -> S -> Z
|
S -> S -> Z
```
and then we would reduce it to:
```
Z
|
S -> S -> S -> S -> S -> Z
```
or am I missing something?
I think you are right about the rules, just expressing them in a different way, not by local interaction between neighboring nodes, but by first-order logic!
When we add 2 (S(S(0))) and 3 (S(S(S(0)))).
I think we start with:
```
Add
| -- S -- S -- Z
| -- S -- S -- S -- Z
```
and then we would reduce it to:
```
S -- S -- S -- S -- S -- Z
```
At the top right corner of the homepage, there is a link to "Docs" -- https://readonly.link/articles/https://cdn.inet.cic.run/docs...
Maybe this article can help.
I was on mobile and I think I accidentally clicked the gh link for the doc, and thought the readme was the doc
would be cool to have a server-rendered page