let r, n be Nat; :: thesis: Ackermann (r,(n + n)) < Ackermann ((r + 4),n)
A1: n + n < H₁(2,n)

proof

2 * n = n + n ;
then H₁(2,n) = (n + n) + 3 by Th10;
hence n + n < H₁(2,n) by NAT_1:16; :: thesis: verum

end;

H₁(r,n + n) < H₁(r,H₁(2,n)) by A1, Th18;
then H₁(r,n + n) < H₁((r + 2) + 2,n) by Th25, XXREAL_0:2;
hence Ackermann (r,(n + n)) < Ackermann ((r + 4),n) ; :: thesis: verum