:: deftheorem Def1 defines AckermannFunction ACKERMAN:def 1 :
for b₁ being BinOp of NAT holds
( b₁ = AckermannFunction iff for m, n being Nat holds
( b₁ . (0,n) = n + 1 & ( m > 0 implies b₁ . (m,0) = b₁ . ((m - 1),1) ) & ( m > 0 & n > 0 implies b₁ . (m,n) = b₁ . ((m - 1),(b₁ . (m,(n - 1)))) ) ) );