let m, n be Nat; :: thesis: AckermannFunction majorizes m const n
set g = m const n;
take N = n + 1; :: according to ACKERMAN:def 14 :: thesis: for F being non empty FinSequence of NAT st F in dom (m const n) holds
for a being Element of NAT st a = max (rng F) holds
(m const n) . F < AckermannFunction . (N,a)
let F be non empty FinSequence of NAT ; :: thesis: ( F in dom (m const n) implies for a being Element of NAT st a = max (rng F) holds
(m const n) . F < AckermannFunction . (N,a) )
assume A1: F in dom (m const n) ; :: thesis: for a being Element of NAT st a = max (rng F) holds
(m const n) . F < AckermannFunction . (N,a)
let a be Element of NAT ; :: thesis: ( a = max (rng F) implies (m const n) . F < AckermannFunction . (N,a) )
assume a = max (rng F) ; :: thesis: (m const n) . F < AckermannFunction . (N,a)
n < n + 1 by NAT_1:13;
then n < H₁(n + 1,a) by Th20, XXREAL_0:2;
hence (m const n) . F < AckermannFunction . (N,a) by A1, FUNCOP_1:7; :: thesis: verum