let h be Element of HFuncs NAT; :: according to COMPUT_1:def 12 :: thesis: for b1 being FinSequence of HFuncs omega holds
( not h in majorizedBy AckermannFunction or not arity h = len b1 or not rng b1 c= majorizedBy AckermannFunction or <:b1:> * h in majorizedBy AckermannFunction )
let G be with_the_same_arity FinSequence of HFuncs NAT; :: thesis: ( not h in majorizedBy AckermannFunction or not arity h = len G or not rng G c= majorizedBy AckermannFunction or <:G:> * h in majorizedBy AckermannFunction )
assume that
A1: h in majorizedBy AckermannFunction and
A2: arity h = len G and
A3: rng G c= majorizedBy AckermannFunction ; :: thesis: <:G:> * h in majorizedBy AckermannFunction
reconsider hG0 = h * <:G:> as Element of HFuncs NAT by COMPUT_1:42;
reconsider hG = hG0 as NAT * -defined to-naturals homogeneous Function ;
per cases ( arity h = 0 or arity h <> 0 ) ;
suppose arity h = 0 ; :: thesis: <:G:> * h in majorizedBy AckermannFunction
then arity G = 0 by A2, COMPUT_1:26;
then A4: dom hG c= 0 -tuples_on NAT by COMPUT_1:42;
end;
suppose A7: arity h <> 0 ; :: thesis: <:G:> * h in majorizedBy AckermannFunction
consider h1 being NAT * -defined to-naturals homogeneous Function such that
A8: h = h1 and
A9: AckermannFunction majorizes h1 by A1;
consider Nh being Element of NAT such that
A10: for F being non empty FinSequence of NAT st F in dom h1 holds
for a being Element of NAT st a = max (rng F) holds
h1 . F < AckermannFunction . (Nh,a) by A9;
consider Ng being Element of NAT such that
A11: for g being NAT * -defined to-naturals homogeneous Function st g in rng G holds
for F being non empty FinSequence of NAT st F in dom g holds
for a being Element of NAT st a = max (rng F) holds
g . F < Ackermann (Ng,a) by A3, Th42;
AckermannFunction majorizes hG
proof
take N = (Nh + Ng) + 2; :: according to ACKERMAN:def 14 :: thesis: for F being non empty FinSequence of NAT st F in dom hG holds
for a being Element of NAT st a = max (rng F) holds
hG . F < AckermannFunction . (N,a)
let F be non empty FinSequence of NAT ; :: thesis: ( F in dom hG implies for a being Element of NAT st a = max (rng F) holds
hG . F < AckermannFunction . (N,a) )
assume A12: F in dom hG ; :: thesis: for a being Element of NAT st a = max (rng F) holds
hG . F < AckermannFunction . (N,a)
let a be Element of NAT ; :: thesis: ( a = max (rng F) implies hG . F < AckermannFunction . (N,a) )
assume A13: a = max (rng F) ; :: thesis: hG . F < AckermannFunction . (N,a)
reconsider GF = G as Function-yielding Function ;
set Y = <:GF:> . F;
A14: ( F in dom <:GF:> & <:GF:> . F in dom h ) by A12, FUNCT_1:11;
then reconsider Y = <:GF:> . F as FinSequence of NAT by FINSEQ_1:def 11;
arity h = len Y by A14, MARGREL1:def 25;
then reconsider Y = Y as non empty FinSequence of NAT by A7;
A15: max (rng Y) in rng Y by XXREAL_2:def 8;
reconsider b = max (rng Y) as Element of NAT by A15;
consider i being object such that
A16: i in dom Y and
A17: Y . i = b by A15, FUNCT_1:def 3;
A18: Y in rng <:GF:> by A14, FUNCT_1:def 3;
rng <:GF:> c= product (rngs GF) by FUNCT_6:29;
then dom Y = dom (rngs GF) by A18, CARD_3:9;
then A19: dom Y = dom G by FUNCT_6:60;
reconsider i = i as Nat by A16;
reconsider Gi0 = G . i as Element of HFuncs NAT by A16, A19, FINSEQ_2:11;
reconsider Gi = Gi0 as NAT * -defined to-naturals homogeneous Function ;
A20: Gi in rng G by A16, A19, FUNCT_1:def 3;
A21: F in dom Gi by A14, A20, FUNCT_6:32;
Y . i = Gi . F by A14, A16, A19, FUNCT_6:34;
then H1(Nh,b) < H1(Nh,H1(Ng,a)) by A17, A11, A13, A20, A21, Th18;
then h1 . Y < H1(Nh,H1(Ng,a)) by A8, A10, A14, XXREAL_0:2;
then h1 . Y < H1(N,a) by Th25, XXREAL_0:2;
hence hG . F < AckermannFunction . (N,a) by A8, A12, FUNCT_1:12; :: thesis: verum
end;
hence <:G:> * h in majorizedBy AckermannFunction ; :: thesis: verum
end;
end;