theorem :: ACKERMAN:8

for n being Nat holds Ackermann (0,n) = n + 1 by Def1;