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

proof

let n be Nat; :: thesis: H₁( 0 ,n) < H₁(0 + 1,n)
A2: H₁( 0 ,n) = n + 1 by Def1;
H₁(1,n) = n + 2 by Th9;
hence H₁( 0 ,n) < H₁(0 + 1,n) by A2, XREAL_1:6; :: thesis: verum

end;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
defpred S₂[ Nat] means H₁(k + 1,$1) < H₁(k + 2,$1);
A5: S₂[ 0 ]

proof

( H₁(k + 1, 0 ) = H₁(k,1) & H₁((k + 1) + 1, 0 ) = H₁(k + 1,1) ) by Th6;
hence H₁(k + 1, 0 ) < H₁(k + 2, 0 ) by A4; :: thesis: verum

end;

A6: for b being Nat st S₂[b] holds
S₂[b + 1]

proof

let b be Nat; :: thesis: ( S₂[b] implies S₂[b + 1] )
assume A7: S₂[b] ; :: thesis: S₂[b + 1]
A8: H₁(k + 1,b + 1) = H₁(k,H₁(k + 1,b)) by Th7;
H₁(k,H₁(k + 1,b)) < H₁(k,H₁(k + 2,b)) by A7, Th18;
then H₁(k,H₁(k + 1,b)) < H₁(k + 1,H₁((k + 1) + 1,b)) by A4, XXREAL_0:2;
hence H₁(k + 1,b + 1) < H₁(k + 2,b + 1) by A8, Th7; :: thesis: verum

end;

for b being Nat holds S₂[b] from NAT_1:sch 2(A5, A6);
hence S₁[k + 1] ; :: thesis: verum

end;

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