defpred S₁[ Nat] means for G being FinSequence of HFuncs NAT st len G = $1 & rng G c= majorizedBy AckermannFunction holds
ex N being Element of NAT st
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 (N,a);
A1: S₁[ 0 ]

proof

let G be FinSequence of HFuncs NAT; :: thesis: ( len G = 0 & rng G c= majorizedBy AckermannFunction implies ex N being Element of NAT st
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 (N,a) )
assume that
A2: len G = 0 and
rng G c= majorizedBy AckermannFunction ; :: thesis: ex N being Element of NAT st
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 (N,a)
take N = 0 ; :: thesis: 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 (N,a)
let g be NAT * -defined to-naturals homogeneous Function; :: thesis: ( g in rng G implies 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 (N,a) )
assume A3: g in rng G ; :: thesis: 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 (N,a)
G = {} by A2;
hence 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 (N,a) by A3; :: thesis: verum

end;

A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
let G be FinSequence of HFuncs NAT; :: thesis: ( len G = k + 1 & rng G c= majorizedBy AckermannFunction implies ex N being Element of NAT st
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 (N,a) )
assume that
A6: len G = k + 1 and
A7: rng G c= majorizedBy AckermannFunction ; :: thesis: ex N being Element of NAT st
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 (N,a)
reconsider Pfx = G | (Seg k) as FinSequence of HFuncs NAT by FINSEQ_1:18;
A8: len Pfx = k by A6, FINSEQ_3:53;
rng Pfx c= rng G by RELAT_1:70;
then consider N1 being Element of NAT such that
A9: for g being NAT * -defined to-naturals homogeneous Function st g in rng Pfx 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 (N1,a) by A5, A8, A7, XBOOLE_1:1;
1 <= k + 1 by NAT_1:11;
then k + 1 in dom G by A6, FINSEQ_3:25;
then G . (k + 1) in rng G by FUNCT_1:def 3;
then G . (k + 1) in majorizedBy AckermannFunction by A7;
then consider gx being NAT * -defined to-naturals homogeneous Function such that
A10: G . (k + 1) = gx and
A11: AckermannFunction majorizes gx ;
consider N2 being Element of NAT such that
A12: for F being non empty FinSequence of NAT st F in dom gx holds
for a being Element of NAT st a = max (rng F) holds
gx . F < AckermannFunction . (N2,a) by A11;
take N = max (N1,N2); :: thesis: 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 (N,a)
let g be NAT * -defined to-naturals homogeneous Function; :: thesis: ( g in rng G implies 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 (N,a) )
assume A13: g in rng G ; :: thesis: 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 (N,a)
let F be non empty FinSequence of NAT ; :: thesis: ( F in dom g implies for a being Element of NAT st a = max (rng F) holds
g . F < Ackermann (N,a) )
assume A14: F in dom g ; :: thesis: for a being Element of NAT st a = max (rng F) holds
g . F < Ackermann (N,a)
let a be Element of NAT ; :: thesis: ( a = max (rng F) implies g . F < Ackermann (N,a) )
assume A15: a = max (rng F) ; :: thesis: g . F < Ackermann (N,a)
consider j being object such that
A16: j in dom G and
A17: G . j = g by A13, FUNCT_1:def 3;
reconsider j = j as Nat by A16;
dom G = Seg (k + 1) by A6, FINSEQ_1:def 3;
then A18: ( 1 <= j & j <= k + 1 ) by A16, FINSEQ_1:1;

per cases ( j <= k or not j <= k ) ;

suppose j <= k ; :: thesis: g . F < Ackermann (N,a)

then A19: j in Seg k by A18, FINSEQ_1:1;
then A20: j in dom Pfx by A6, FINSEQ_3:54;
(G | (Seg k)) . j = G . j by A19, FUNCT_1:49;
then A21: g in rng Pfx by A17, A20, FUNCT_1:def 3;
H₁(N1,a) <= H₁(N,a) by XXREAL_0:25, Th24;
hence g . F < Ackermann (N,a) by A9, A14, A15, A21, XXREAL_0:2; :: thesis: verum

end;

suppose not j <= k ; :: thesis: g . F < Ackermann (N,a)

then k + 1 <= j by NAT_1:13;
then A22: j = k + 1 by A18, XXREAL_0:1;
H₁(N2,a) <= H₁(N,a) by XXREAL_0:25, Th24;
hence g . F < Ackermann (N,a) by A10, A12, A14, A15, A17, A22, XXREAL_0:2; :: thesis: verum

end;

end;

end;

let G be FinSequence of HFuncs NAT; :: thesis: ( rng G c= majorizedBy AckermannFunction implies ex N being Element of NAT st
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 (N,a) )
assume A23: rng G c= majorizedBy AckermannFunction ; :: thesis: ex N being Element of NAT st
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 (N,a)
for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A4);
then S₁[ len G] ;
hence ex N being Element of NAT st
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 (N,a) by A23; :: thesis: verum