let m, n be Nat; :: thesis: Ackermann ((m + 1),(n + 1)) = Ackermann (m,(Ackermann ((m + 1),n)))
( (m + 1) - 1 = m & (n + 1) - 1 = n ) ;
hence Ackermann ((m + 1),(n + 1)) = Ackermann (m,(Ackermann ((m + 1),n))) by Def1; :: thesis: verum