// Ackermann function on unary natural numbers
// fun ack(0,y) = y+1
//   | ack(x,0) = ack(x-1,1)        
//   | ack(x,y) = ack(x-1,ack(x,y-1));
//
ack(r,y)>< Z => r~S(y);
ack(r,y)>< S(x) => ack_Sx(r, x)~y;
ack_Sx(r,x)>< Z => ack(r, S(Z))~x;
ack_Sx(r,x)>< S(y) => dup(x1,x2)~x, ack(r,cnt)~x1, ack_Sx(cnt,x2)~y;


dup(a1,a2)>< Z => a1~Z, a2~Z;
dup(a1,a2)>< S(x) => a1~S(w1), a2~S(w2), dup(w1,w2)~x;

// Ack 3 5
ack(r, S(S(S(S(S(Z))))))~S(S(S(Z)));
prnat r;
exit;