Zの定義

f(0)=z
f(a+1)=f(a)+z
f(0:n+2)=f(z:n+1)
f(0:n+1,a+1)=f(f(0:n+1,a):n+1)
f(#c,b+1,0:n+1)=f(#c,b,z:n+1)
f(#c,b+1,0:n,a+1)=f(#c,b,f(b+1,0:n,a):n+1)
f([0])=f(z:z)
f([a+1])=f(f([a]):f([a]))
f([0],0:n+1)=f([z:z],z:n)
f([a+1],0:n+1)=f([f([a],0:n+1):f([a],0:n+1)],f([a],0:n+1):n)
f([0],#d,b+1,0:n)=f([z:z],#d,b,z:n)
f([a+1],#d,b+1,0:n)=f([f([a],#d,b+1,0:n):f([a],#d,b+1,0:n)],#d,b,f([a],#d,b+1,0:n):n)
f(0:n+1,[0])=f(z:n,[z:z],z:z)
f(0:n+1,[a+1])=f(f(0:n+1,[a]):n,[f(0:n+1,[a]):f(0:n+1,[a])],f(0:n+1,[a]):f(0:n+1,[a]))
f(#e,b+1,0:n,[0])=f(#e,b,z:n,[z:z],z:z)
f(#e,b+1,0:n,[a+1])=f(#e,b,f(#e,b+1,0:n,[a]):n,[f(#e,b+1,0:n,[a]):f(#e,b+1,0:n,[a])],f(#e,b+1,0:n,[a]):f(#e,b+1,0:n,[a]))
f(#e,[0:n+2],#d)=f(#e,[z:n+1],#d)
f(#e,[0:n+1,a+1],#d)=f(#e,[f([0:n+1,a]):n+1],#d)
f(#e,[#c,b+1,0:n+1],#d)=f(#e,[#c,b,z:n+1],#d)
f(#e,[#c,b+1,0:n,a+1],#d)=f(#e,[#c,b,f(b+1,0:n,a):n+1],#d)

Z=f(z:z,[z:z],z:z)