"Rules of Equality:

            Symmetry: If r=s is a theorem, then so is s=r.

            Transitivity: If r=s and s=t are theorems, then so is r=t.

"Rules of Successorship:

            Add S: If r=t is a theorem, then Sr=St is a theorem.

            Drop S: If Sr=St is a theorem, then r=t is a theorem

Aa:Ab:(a+Sb)=S(a+b)
Ab:(S0+Sb)=S(S0+b)
(S0+S0)=S(S0+0)
Aa:(a+0)=a
(S0+0)=S0
S(S0+0)=SS0
(S0+S0)=SS0

Aa:Ab:(a•Sb)=((a•b)+a)
Ab:(S0•Sb)=((S0•b)+S0)
(S0•S0)=((S0•0)+S0)
Aa:Ab:(a+Sb)=S(a+b)
Ab:((S0•0)+Sb)=S((S0•0)+b)
((S0•0)+S0)=S((S0•0)+0)
Aa:(a+0)=a
((S0•0)+0)=(S0•0)
Aa(a•0)=0
(S0•0)=0
((S0•0)+0)=0
S((S0•0)+0)=S0
((S0•0)+S0)=S)
(S0•S0)=S0