theorem Th12: :: ACKERMAN:12

for n being Nat holds Ackermann (4,n) = (2 |^|^ (n + 3)) - 3