let g, f1, f2 be Element of HFuncs NAT; :: according to COMPUT_1:def 13 :: thesis: for b1 being set holds
( not g is_primitive-recursively_expressed_by f1,f2,b1 or not f1 in majorizedBy AckermannFunction or not f2 in majorizedBy AckermannFunction or g in majorizedBy AckermannFunction )
let i be Nat; :: thesis: ( not g is_primitive-recursively_expressed_by f1,f2,i or not f1 in majorizedBy AckermannFunction or not f2 in majorizedBy AckermannFunction or g in majorizedBy AckermannFunction )
assume that
A1: g is_primitive-recursively_expressed_by f1,f2,i and
A2: f1 in majorizedBy AckermannFunction and
A3: f2 in majorizedBy AckermannFunction ; :: thesis: g in majorizedBy AckermannFunction
reconsider g0 = g, f10 = f1, f20 = f2 as NAT * -defined to-naturals homogeneous Function ;
per cases ( f1 = {} or f1 <> {} ) ;
suppose f1 = {} ; :: thesis: g in majorizedBy AckermannFunction
then g = {} by A1, COMPUT_1:67;
then AckermannFunction majorizes g by Th41, COMPUT_1:18;
hence g in majorizedBy AckermannFunction ; :: thesis: verum
end;
suppose A4: f1 <> {} ; :: thesis: g in majorizedBy AckermannFunction
consider n being Element of NAT such that
A5: dom g0 c= n -tuples_on NAT and
A6: 1 <= i and
A7: i <= n and
(arity f10) + 1 = n and
n + 1 = arity f20 and
A8: for p being FinSequence of NAT st len p = n holds
( ( p +* (i,0) in dom g implies Del (p,i) in dom f1 ) & ( Del (p,i) in dom f1 implies p +* (i,0) in dom g ) & ( p +* (i,0) in dom g implies g . (p +* (i,0)) = f1 . (Del (p,i)) ) & ( for m being Nat holds
( ( p +* (i,(m + 1)) in dom g implies ( p +* (i,m) in dom g & (p +* (i,m)) ^ <*(g . (p +* (i,m)))*> in dom f2 ) ) & ( p +* (i,m) in dom g & (p +* (i,m)) ^ <*(g . (p +* (i,m)))*> in dom f2 implies p +* (i,(m + 1)) in dom g ) & ( p +* (i,(m + 1)) in dom g implies g . (p +* (i,(m + 1))) = f2 . ((p +* (i,m)) ^ <*(g . (p +* (i,m)))*>) ) ) ) ) by A1, COMPUT_1:def 9;
consider f1m being NAT * -defined to-naturals homogeneous Function such that
A9: f1 = f1m and
A10: AckermannFunction majorizes f1m by A2;
consider f2m being NAT * -defined to-naturals homogeneous Function such that
A11: f2 = f2m and
A12: AckermannFunction majorizes f2m by A3;
consider N1 being Element of NAT such that
A13: for F being non empty FinSequence of NAT st F in dom f1m holds
for a being Element of NAT st a = max (rng F) holds
f1m . F < AckermannFunction . (N1,a) by A10;
consider N2 being Element of NAT such that
A14: for F being non empty FinSequence of NAT st F in dom f2m holds
for a being Element of NAT st a = max (rng F) holds
f2m . F < AckermannFunction . (N2,a) by A12;
ex C being Element of NAT st
( ( arity f10 = 0 implies ( {} in dom f10 & C = f10 . {} ) ) & ( arity f10 <> 0 implies C = 0 ) )
proof
per cases ( arity f10 = 0 or arity f10 <> 0 ) ;
suppose A15: arity f10 = 0 ; :: thesis: ex C being Element of NAT st
( ( arity f10 = 0 implies ( {} in dom f10 & C = f10 . {} ) ) & ( arity f10 <> 0 implies C = 0 ) )
consider x being object such that
A16: x in dom f10 by A4, XBOOLE_0:def 1;
reconsider x = x as FinSequence of NAT by A16, FINSEQ_1:def 11;
len x = 0 by A15, A16, MARGREL1:def 25;
then A17: x = {} ;
then f10 . {} in rng f10 by A16, FUNCT_1:def 3;
then reconsider c = f10 . {} as Element of NAT ;
take c ; :: thesis: ( ( arity f10 = 0 implies ( {} in dom f10 & c = f10 . {} ) ) & ( arity f10 <> 0 implies c = 0 ) )
thus ( ( arity f10 = 0 implies ( {} in dom f10 & c = f10 . {} ) ) & ( arity f10 <> 0 implies c = 0 ) ) by A15, A16, A17; :: thesis: verum
end;
suppose A18: arity f10 <> 0 ; :: thesis: ex C being Element of NAT st
( ( arity f10 = 0 implies ( {} in dom f10 & C = f10 . {} ) ) & ( arity f10 <> 0 implies C = 0 ) )
take 0 ; :: thesis: ( ( arity f10 = 0 implies ( {} in dom f10 & 0 = f10 . {} ) ) & ( arity f10 <> 0 implies 0 = 0 ) )
thus ( ( arity f10 = 0 implies ( {} in dom f10 & 0 = f10 . {} ) ) & ( arity f10 <> 0 implies 0 = 0 ) ) by A18; :: thesis: verum
end;
end;
end;
then consider C being Element of NAT such that
A19: ( arity f10 = 0 implies ( {} in dom f10 & C = f10 . {} ) ) and
( arity f10 <> 0 implies C = 0 ) ;
set M = max ((max (N1,N2)),C);
set R = (max ((max (N1,N2)),C)) + 5;
set S = ((max ((max (N1,N2)),C)) + 5) + 1;
A20: N1 <= max (N1,N2) by XXREAL_0:25;
A21: max (N1,N2) <= max ((max (N1,N2)),C) by XXREAL_0:25;
A22: N1 <= max ((max (N1,N2)),C) by A20, A21, XXREAL_0:2;
A23: N2 <= max (N1,N2) by XXREAL_0:25;
max (N1,N2) <= max ((max (N1,N2)),C) by XXREAL_0:25;
then N2 <= max ((max (N1,N2)),C) by A23, XXREAL_0:2;
then A24: N2 < (max ((max (N1,N2)),C)) + 5 by NAT_1:16, XXREAL_0:2;
A25: C <= max ((max (N1,N2)),C) by XXREAL_0:25;
N1 <= (max ((max (N1,N2)),C)) + 5 by A22, NAT_1:16, XXREAL_0:2;
then A26: N1 <= ((max ((max (N1,N2)),C)) + 5) + 1 by NAT_1:12;
C < (max ((max (N1,N2)),C)) + 5 by A25, NAT_1:16, XXREAL_0:2;
then A27: C < ((max ((max (N1,N2)),C)) + 5) + 1 by NAT_1:13;
AckermannFunction majorizes g0
proof
take N = (((max ((max (N1,N2)),C)) + 5) + 1) + 4; :: according to ACKERMAN:def 14 :: thesis: for F being non empty FinSequence of NAT st F in dom g0 holds
for a being Element of NAT st a = max (rng F) holds
g0 . F < AckermannFunction . (N,a)
let F be non empty FinSequence of NAT ; :: thesis: ( F in dom g0 implies for a being Element of NAT st a = max (rng F) holds
g0 . F < AckermannFunction . (N,a) )
assume A28: F in dom g0 ; :: thesis: for a being Element of NAT st a = max (rng F) holds
g0 . F < AckermannFunction . (N,a)
let a be Element of NAT ; :: thesis: ( a = max (rng F) implies g0 . F < AckermannFunction . (N,a) )
assume A29: a = max (rng F) ; :: thesis: g0 . F < AckermannFunction . (N,a)
defpred S1[ Nat] means for p being FinSequence of NAT st len p = n & ( for x being Nat st x in rng p holds
x <= a ) & p +* (i,c1) in dom g0 holds
g0 . (p +* (i,c1)) < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + c1);
A30: S1[ 0 ]
proof
let p be FinSequence of NAT ; :: thesis: ( len p = n & ( for x being Nat st x in rng p holds
x <= a ) & p +* (i,0) in dom g0 implies g0 . (p +* (i,0)) < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + 0) )
assume that
A31: len p = n and
A32: for x being Nat st x in rng p holds
x <= a and
A33: p +* (i,0) in dom g0 ; :: thesis: g0 . (p +* (i,0)) < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + 0)
A34: ( ( p +* (i,0) in dom g0 implies Del (p,i) in dom f10 ) & ( Del (p,i) in dom f10 implies p +* (i,0) in dom g0 ) & ( p +* (i,0) in dom g0 implies g0 . (p +* (i,0)) = f10 . (Del (p,i)) ) ) by A8, A31;
reconsider D = Del (p,i) as FinSequence of NAT by FINSEQ_3:105;
per cases ( D = {} or D <> {} ) ;
suppose A35: D = {} ; :: thesis: g0 . (p +* (i,0)) < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + 0)
len D = arity f10 by A33, A34, MARGREL1:def 25;
hence g0 . (p +* (i,0)) < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + 0) by A27, A19, A34, A35, XXREAL_0:2, Th20; :: thesis: verum
end;
suppose D <> {} ; :: thesis: g0 . (p +* (i,0)) < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + 0)
then reconsider D = D as non empty FinSequence of NAT ;
A36: max (rng D) in rng D by XXREAL_2:def 8;
then reconsider d = max (rng D) as Element of NAT ;
rng D c= rng p by FINSEQ_3:106;
then H1(N1,d) <= H1(N1,a) by A32, A36, Th19;
then A37: f1m . D < H1(N1,a) by A9, A13, A33, A34, XXREAL_0:2;
H1(N1,a) <= H1(((max ((max (N1,N2)),C)) + 5) + 1,a) by A26, Th24;
hence g0 . (p +* (i,0)) < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + 0) by A9, A33, A34, A37, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A38: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A39: S1[m] ; :: thesis: S1[m + 1]
let p be FinSequence of NAT ; :: thesis: ( len p = n & ( for x being Nat st x in rng p holds
x <= a ) & p +* (i,(m + 1)) in dom g0 implies g0 . (p +* (i,(m + 1))) < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + (m + 1)) )
assume that
A40: len p = n and
A41: for x being Nat st x in rng p holds
x <= a and
A42: p +* (i,(m + 1)) in dom g0 ; :: thesis: g0 . (p +* (i,(m + 1))) < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + (m + 1))
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A43: p +* (i,mm) in dom g0 by A8, A40, A42;
reconsider U = p +* (i,mm) as FinSequence of NAT ;
reconsider v = g . U as Element of NAT by A43, PARTFUN1:4;
reconsider W = U ^ <*v*> as non empty FinSequence of NAT ;
A44: W in dom f20 by A42, A8, A40;
A45: g0 . U < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m) by A39, A40, A41, A43;
A46: max (rng W) in rng W by XXREAL_2:def 8;
then reconsider b = max (rng W) as Element of NAT ;
A47: b < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m)
proof
A48: rng W = (rng U) \/ (rng <*v*>) by FINSEQ_1:31;
per cases ( b in rng U or b in rng <*v*> ) by A46, A48, XBOOLE_0:def 3;
suppose A49: b in rng U ; :: thesis: b < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m)
rng U c= (rng p) \/ {m} by FUNCT_7:100;
then ( b in rng p or b in {m} ) by A49, XBOOLE_0:def 3;
then A50: ( b <= a or b = m ) by A41, TARSKI:def 1;
a <= a + m by NAT_1:11;
then b <= a + m by A50, XXREAL_0:2, NAT_1:11;
hence b < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m) by Th16, XXREAL_0:2; :: thesis: verum
end;
suppose A51: b in rng <*v*> ; :: thesis: b < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m)
rng <*v*> = {v} by FINSEQ_1:38;
hence b < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m) by A45, A51, TARSKI:def 1; :: thesis: verum
end;
end;
end;
H1(N2,b) < H1(N2,H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m)) by A47, Th18;
then A52: f2m . W < H1(N2,H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m)) by A14, A11, A44, XXREAL_0:2;
H1(N2,H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m)) < H1((max ((max (N1,N2)),C)) + 5,H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m)) by A24, Th23;
then A53: f2m . W < H1((max ((max (N1,N2)),C)) + 5,H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m)) by A52, XXREAL_0:2;
H1((max ((max (N1,N2)),C)) + 5,H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m)) = H1(((max ((max (N1,N2)),C)) + 5) + 1,(a + m) + 1) by Th7
.= H1(((max ((max (N1,N2)),C)) + 5) + 1,a + (m + 1)) ;
hence g0 . (p +* (i,(m + 1))) < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + (m + 1)) by A11, A42, A8, A40, A53; :: thesis: verum
end;
A54: for m being Nat holds S1[m] from NAT_1:sch 2(A30, A38);
 A55: len F = n by A5, A28, CARD_1:def 7;
i in Seg n by A6, A7, FINSEQ_1:1;
then A56: i in dom F by A55, FINSEQ_1:def 3;
then F . i in rng F by FUNCT_1:def 3;
then reconsider m = F . i as Element of NAT ;
A57: for x being Nat st x in rng F holds
x <= a by A29, XXREAL_2:def 8;
A58: F = F +* (i,m) by FUNCT_7:35;
m in rng F by A56, FUNCT_1:def 3;
then a + m <= a + a by A57, XREAL_1:6;
then H1(((max ((max (N1,N2)),C)) + 5) + 1,a + m) <= H1(((max ((max (N1,N2)),C)) + 5) + 1,a + a) by Th19;
then A59: g0 . F < H1(((max ((max (N1,N2)),C)) + 5) + 1,a + a) by A28, A54, A55, A57, A58, XXREAL_0:2;
H1(((max ((max (N1,N2)),C)) + 5) + 1,a + a) < H1((((max ((max (N1,N2)),C)) + 5) + 1) + 4,a) by Th27;
hence g0 . F < AckermannFunction . (N,a) by A59, XXREAL_0:2; :: thesis: verum
end;
hence g in majorizedBy AckermannFunction ; :: thesis: verum
end;
end;