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