up to \(ψ_0(0,ψ_0(1,0))\)[]
\(0 \to 0\)
\(ψ_0(0,0) \to 0\)
\(ψ_0(0,0)+ψ_0(0,0) \to ψ_0(0,0)\)
\(ψ_0(0,0)+ψ_0(0,0)+ψ_0(0,0) \to ψ_0(0,0)+ψ_0(0,0)\)
\(ψ_0(0,ψ_0(0,0)) \to ψ_0(0,0)+ψ_0(0,0)+...+ψ_0(0,0)+ψ_0(0,0)\)
\(ψ_0(0,ψ_0(0,0)+ψ_0(0,0)) \to ψ_0(0,ψ_0(0,0))+ψ_0(0,ψ_0(0,0))+...+ψ_0(0,ψ_0(0,0))+ψ_0(0,ψ_0(0,0))\)
\(ψ_0(0,ψ_0(0,ψ_0(0,0))) \to ψ_0(0,ψ_0(0,0)+ψ_0(0,0)+...+ψ_0(0,0)+ψ_0(0,0))\)
\(ψ_0(0,ψ_0(1,0)) \to ψ_0(0,ψ_0(0,ψ_0(0,...)))\)
up to \(ψ_0(0,ψ_0(2,0))\)[]
\(ψ_0(0,ψ_0(1,0)+ψ_0(0,ψ_0(1,0))) \to ψ_0(0,ψ_0(1,0)+ψ_0(0,ψ_0(0,ψ_0(0,...)))\)
\(ψ_0(0,ψ_0(1,0)+ψ_0(1,0)) \to ψ_0(0,ψ_0(1,0)+ψ_0(0,ψ_0(1,0)+ψ_0(0,ψ_0(1,0)+...)))\)
\(ψ_0(0,ψ_0(1,ψ_0(1,0))) \to ψ_0(0,ψ_0(1,ψ_0(0,ψ_0(1,...))))\)
\(ψ_0(0,ψ_0(1,ψ_0(1,0)+ψ_0(1,0))) \to ψ_0(0,ψ_0(1,ψ_0(1,0)+ψ_0(0,ψ_0(1,ψ_0(1,0)+...))))\)
\(ψ_0(0,ψ_0(1,ψ_0(1,ψ_0(1,0)))) \to ψ_0(0,ψ_0(1,ψ_0(1,ψ_0(1,ψ_0(0,ψ_0(1,ψ_0(1,ψ_0(1,...))))))))\)
\(ψ_0(0,ψ_0(2,0)) \to ψ_0(0,ψ_0(1,ψ_0(1,...)))\)
up to \(ψ_0(0,ψ_0(3,0))\)[]
\(ψ_0(0,ψ_0(2,0)+ψ_0(1,0)) \to ψ_0(0,ψ_0(2,0)+ψ_0(0,ψ_0(2,0)+....))\)
\(ψ_0(0,ψ_0(2,0)+ψ_0(1,ψ_0(2,0))) \to ψ_0(0,ψ_0(2,0)+ψ_0(1,ψ_0(1,ψ_0(1,...))))\)
\(ψ_0(0,ψ_0(2,0)+ψ_0(2,0)) \to ψ_0(0,ψ_0(2,0)+ψ_0(1,ψ_0(2,0)+ψ_0(1,ψ_0(2,0)+...)))\)
\(ψ_0(0,ψ_0(2,ψ_0(0,ψ_0(1,0)))) \to ψ_0(0,ψ_0(2,ψ_0(0,ψ_0(0,ψ_0(0,...)))))\)
\(ψ_0(0,ψ_0(2,ψ_0(0,ψ_0(2,0)))) \to ψ_0(0,ψ_0(2,ψ_0(0,ψ_0(1,ψ_0(1,...)))))\)
\(ψ_0(0,ψ_0(2,ψ_0(1,0))) \to ψ_0(0,ψ_0(2,ψ_0(0,ψ_0(2,ψ_0(0,ψ_0(2,...))))))\)
\(ψ_0(0,ψ_0(3,0)) \to ψ_0(0,ψ_0(2,ψ_0(2,...)))\)
up to \(ψ_0(0,ψ_1(0,0))\)[]
\(ψ_0(0,ψ_0(ψ_0(0,ψ_0(0,0))+ψ_0(0,0),0)) \to ψ_0(0,ψ_0(ψ_0(0,ψ_0(0,0)),ψ_0(ψ_0(0,ψ_0(0,0)),...)))\)
\(ψ_0(0,ψ_0(ω+1,0)+ψ_0(1,0)) \to ψ_0(0,ψ_0(ω+1,0)+ψ_0(0,ψ_0(ω+1,0)+ψ_0(0,ψ_0(ω+1,0)+...)))\)
\(ψ_0(0,ψ_1(0,0)) \to ψ_0(0,ψ_0(ψ_0(...,0),0))\)
up to \(ψ_0(0,ψ_2(0,0))\)[]
\(ψ_0(0,ψ_1(0,0)+ψ_0(ψ_1(0,0),ψ_1(0,0))) \to ψ_0(0,ψ_1(0,0)+ψ_0(ψ_1(0,0),ψ_0(ψ_0(...,0),0)))\)
\(ψ_0(0,ψ_1(0,0)+ψ_1(0,0)) \to ψ_0(0,ψ_1(0,0)+ψ_0(ψ_1(0,0)+ψ_0(ψ_1(0,0)+...,0),0))\)
\(ψ_0(0,ψ_1(0,ψ_0(0,0))) \to ψ_0(0,ψ_1(0,0)+ψ_1(0,0)+ψ_1(0,0)+...)\)
\(ψ_0(0,ψ_1(0,ψ_0(1,0))) \to ψ_0(0,ψ_1(0,ψ_0(0,ψ_1(0,ψ_0(0,ψ_1(0,...))))))\)
\(ψ_0(0,ψ_1(0,ψ_1(0,0))) \to ψ_0(0,ψ_1(0,ψ_0(ψ_1(0,ψ_0(ψ_1(0,ψ_0(ψ_1(0,...),0)),0)),0)))\)
\(ψ_0(0,ψ_1(1,0)) \to ψ_0(0,ψ_1(0,ψ_1(0,...)))\)
\(ψ_0(0,ψ_1(ψ_0(1,0),0)) \to ψ_0(0,ψ_1(ψ_0(0,ψ_1(ψ_0(0,ψ_1(ψ_0(0,...),0)),0)),0))\)
\(ψ_0(0,ψ_1(ψ_1(0,0),0)) \to ψ_0(0,ψ_1(ψ_0(ψ_1(ψ_0(ψ_1(ψ_0(...,0),0),0),0),0),0))\)
\(ψ_0(0,ψ_2(0,0)) \to ψ_0(0,ψ_1(ψ_1(...,0),0))\)
up to \(ψ_0(0,ψ_{ψ_0(1,0)}(0,0))\)[]
\(ψ_0(0,ψ_{ψ_0(1,0)}(0,0)) \to ψ_0(0,ψ_{ψ_0(0,ψ_{ψ_0(0,ψ_{ψ_0(0,...)}(0,0))}(0,0))}(0,0))\)