let m, n be Nat; :: thesis: Ackermann (m,n) < Ackermann (m,(n + 1))
defpred S₁[ Nat] means H₁($1,n) < H₁($1,n + 1);
A1: S₁[ 0 ]

proof

( H₁( 0 ,n) = n + 1 & H₁( 0 ,n + 1) = (n + 1) + 1 ) by Def1;
hence H₁( 0 ,n) < H₁( 0 ,n + 1) by NAT_1:16; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
H₁(k + 1,n + 1) = H₁(k,H₁(k + 1,n)) by Th7;
hence H₁(k + 1,n) < H₁(k + 1,n + 1) by Th16; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence Ackermann (m,n) < Ackermann (m,(n + 1)) ; :: thesis: verum