ack(Z,n) -> S(n)
ack(S(m),Z) -> ack(m,S(Z))
ack(S(m),S(n)) -> ack(m,ack(S(m),n))

[Z] = 1
[S](x) = x+1