let m, n be Nat; :: thesis: Ackermann (m,(n + 1)) <= Ackermann ((m + 1),n)
defpred S₁[ Nat] means for m being Nat holds H₁(m,$1 + 1) <= H₁(m + 1,$1);
A1: S₁[ 0 ] by Th6;
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 A3: S₁[k] ; :: thesis: S₁[k + 1]
let m be Nat; :: thesis: H₁(m,(k + 1) + 1) <= H₁(m + 1,k + 1)
(k + 1) + 1 <= H₁(m,k + 1) by Th16, NAT_1:13;
then A4: H₁(m,(k + 1) + 1) <= H₁(m,H₁(m,k + 1)) by Th19;
H₁(m,H₁(m,k + 1)) <= H₁(m,H₁(m + 1,k)) by A3, Th19;
then H₁(m,(k + 1) + 1) <= H₁(m,H₁(m + 1,k)) by A4, XXREAL_0:2;
hence H₁(m,(k + 1) + 1) <= H₁(m + 1,k + 1) by Th7; :: thesis: verum

end;

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