let m, n be Nat; :: thesis: m < Ackermann (m,n)
defpred S1[ Nat] means for m being Nat holds m < H1(m,$1);
A1: S1[ 0 ]
proof
let m be Nat; :: thesis: m < H1(m, 0 )
defpred S2[ Nat] means $1 < H1($1, 0 );
A2: S2[ 0 ]
proof
H1( 0 , 0 ) = 0 + 1 by Def1;
hence S2[ 0 ] ; :: thesis: verum
end;
A3: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume S2[k] ; :: thesis: S2[k + 1]
then A4: k + 1 <= H1(k, 0 ) by NAT_1:13;
A5: H1(k, 0 ) < H1(k,0 + 1) by Th17;
H1(k + 1, 0 ) = H1(k,1) by Th6;
hence k + 1 < H1(k + 1, 0 ) by A4, A5, XXREAL_0:2; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(A2, A3);
 hence m < H1(m, 0 ) ; :: thesis: verum
end;
A6: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; :: thesis: S1[n + 1]
defpred S2[ Nat] means $1 < H1($1,n + 1);
A8: S2[ 0 ]
proof
H1( 0 ,n + 1) = (n + 1) + 1 by Def1;
hence 0 < H1( 0 ,n + 1) ; :: thesis: verum
end;
A9: for a being Nat st S2[a] holds
S2[a + 1]
proof
let a be Nat; :: thesis: ( S2[a] implies S2[a + 1] )
assume S2[a] ; :: thesis: S2[a + 1]
A10: H1(a,H1(a + 1,n)) = H1(a + 1,n + 1) by Th7;
H1(a + 1,n) < H1(a,H1(a + 1,n)) by Th16;
hence S2[a + 1] by A7, A10, XXREAL_0:2; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A8, A9);
 hence S1[n + 1] ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A1, A6);
 hence m < Ackermann (m,n) ; :: thesis: verum