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

proof

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

end;

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

proof

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

proof

H₁(m + 1, 0 ) = H₁(m,1) by Th6;
hence 0 < H₁(m + 1, 0 ) by A3; :: thesis: verum

end;

A5: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume S₂[n] ; :: thesis: S₂[n + 1]
then A6: n + 1 <= H₁(m + 1,n) by NAT_1:13;
H₁(m,H₁(m + 1,n)) = H₁(m + 1,n + 1) by Th7;
hence S₂[n + 1] by A3, A6, XXREAL_0:2; :: thesis: verum

end;

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

end;

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