let m, n be Nat; :: thesis: ( 1 <= n & n <= m implies AckermannFunction majorizes m succ n )
assume A1: ( 1 <= n & n <= m ) ; :: thesis: AckermannFunction majorizes m succ n
set g = m succ n;
take N = n + 1; :: according to ACKERMAN:def 14 :: thesis: for F being non empty FinSequence of NAT st F in dom (m succ n) holds
for a being Element of NAT st a = max (rng F) holds
(m succ n) . F < AckermannFunction . (N,a)
let F be non empty FinSequence of NAT ; :: thesis: ( F in dom (m succ n) implies for a being Element of NAT st a = max (rng F) holds
(m succ n) . F < AckermannFunction . (N,a) )
assume A2: F in dom (m succ n) ; :: thesis: for a being Element of NAT st a = max (rng F) holds
(m succ n) . F < AckermannFunction . (N,a)
let a be Element of NAT ; :: thesis: ( a = max (rng F) implies (m succ n) . F < AckermannFunction . (N,a) )
assume A3: a = max (rng F) ; :: thesis: (m succ n) . F < AckermannFunction . (N,a)
A4: dom (m succ n) = m -tuples_on NAT by COMPUT_1:def 7;
then A5: (m succ n) . F = (F . n) + 1 by A2, COMPUT_1:def 7;
len F = m by A2, A4, FINSEQ_2:132;
then n in dom F by A1, FINSEQ_3:25;
then F . n in rng F by FUNCT_1:def 3;
then F . n <= a by A3, XXREAL_2:def 8;
then A6: (F . n) + 1 <= a + 1 by XREAL_1:6;
a + 1 < a + 2 by XREAL_1:6;
then (F . n) + 1 < a + 2 by A6, XXREAL_0:2;
then A7: (m succ n) . F < H₁(1,a) by A5, Th9;
H₁(1,a) <= H₁(N,a) by Th24, NAT_1:11;
hence (m succ n) . F < AckermannFunction . (N,a) by A7, XXREAL_0:2; :: thesis: verum