let n, c be Element of NAT ; :: thesis: for P being non empty primitive-recursively_closed Subset of (HFuncs NAT ) holds n const c in P
let P be non empty primitive-recursively_closed Subset of (HFuncs NAT ); :: thesis: n const c in P
defpred S2[ Element of NAT ] means 0 const $1 in P;
defpred S3[ Element of NAT ] means for c being Element of NAT holds $1 const c in P;
A1: P is composition_closed by Def17;
A2: for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
reconsider 1succ1 = 1 succ 1 as quasi_total Element of HFuncs NAT by Th32;
let i be Element of NAT ; :: thesis: ( S2[i] implies S2[i + 1] )
A3: 1 succ 1 in P by Def17;
A4: <*> NAT is Element of 0 -tuples_on NAT by FINSEQ_2:151;
then A5: (0 const i) . {} = i by FUNCOP_1:13;
reconsider 0consti = 0 const i as Element of HFuncs NAT by Th31;
set F = <*(0 const i)*>;
<*0consti*> is FinSequence of HFuncs NAT ;
then reconsider F = <*(0 const i)*> as with_the_same_arity FinSequence of HFuncs NAT ;
assume 0 const i in P ; :: thesis: S2[i + 1]
then A6: {(0 const i)} c= P by ZFMISC_1:37;
A7: arity (1 succ 1) = 1 by Th38
.= len F by FINSEQ_1:56 ;
A8: rng F = {(0 const i)} by FINSEQ_1:56;
now
let h be Element of HFuncs NAT ; :: thesis: ( h in rng F implies h is quasi_total )
assume h in rng F ; :: thesis: h is quasi_total
then h = 0 const i by A8, TARSKI:def 1;
hence h is quasi_total by Th32; :: thesis: verum
end;
then reconsider g = 1succ1 * <:F:> as quasi_total Element of HFuncs NAT by A7, Th50;
A9: arity (0 const (i + 1)) = 0 by Th35;
A10: (0 const (i + 1)) . {} = i + 1 by A4, FUNCOP_1:13;
A11: dom (1 succ 1) = 1 -tuples_on NAT by Def10;
A12: arity (0 const i) = 0 by Th35;
then A13: dom (0 const i) = 0 -tuples_on NAT by Th26;
then A14: <:F:> . {} = <*i*> by A4, A5, FUNCT_6:61;
reconsider ii = <*i*> as Element of 1 -tuples_on NAT by FINSEQ_2:151;
A15: dom <:<*(0 const i)*>:> = dom (0 const i) by FUNCT_6:61;
then g . {} = (1 succ 1) . (<:F:> . {} ) by A4, A13, FUNCT_1:23;
then A16: g . {} = (ii /. 1) + 1 by A14, Def10
.= i + 1 by FINSEQ_4:25 ;
A17: dom (0 const i) = 0 -tuples_on NAT by A12, Th26;
then <:<*(0 const i)*>:> . {} = ii by A4, A5, FUNCT_6:61;
then A18: {} in dom g by A4, A15, A17, A11, FUNCT_1:21;
0 const i in rng F by A8, TARSKI:def 1;
then arity F = 0 by A12, Def7;
then arity g = 0 by A18, Th48, RELAT_1:60;
then 0 const (i + 1) = (1 succ 1) * <:<*(0 const i)*>:> by A9, A10, A18, A16, Th52, RELAT_1:60;
hence S2[i + 1] by A1, A6, A8, A3, A7, Def15; :: thesis: verum
end;
A19: P is primitive-recursion_closed by Def17;
A20: now
let n be Element of NAT ; :: thesis: ( S3[n] implies S3[n + 1] )
assume A21: S3[n] ; :: thesis: S3[n + 1]
thus S3[n + 1] :: thesis: verum
proof
let i be Element of NAT ; :: thesis: (n + 1) const i in P
set g = (n + 1) const i;
set f1 = n const i;
set j = n + 1;
set f2 = (n + 2) proj (n + 2);
A22: dom ((n + 1) const i) = (n + 1) -tuples_on NAT by FUNCOP_1:19;
A23: n + (1 + 1) = (n + 1) + 1 ;
then 1 <= n + 2 by NAT_1:11;
then A24: (n + 2) proj (n + 2) in P by Def17;
A25: arity ((n + 2) proj (n + 2)) = n + 2 by Th41;
A26: dom ((n + 2) proj (n + 2)) = (n + 2) -tuples_on NAT by Th40;
A27: arity (n const i) = n by Th35;
A28: dom (n const i) = n -tuples_on NAT by FUNCOP_1:19;
A29: arity ((n + 1) const i) = n + 1 by Th35;
A30: (n + 1) const i is_primitive-recursively_expressed_by n const i,(n + 2) proj (n + 2),n + 1
proof
take m = arity ((n + 1) const i); :: according to COMPUT_1:def 12 :: thesis: ( dom ((n + 1) const i) c= m -tuples_on NAT & n + 1 >= 1 & n + 1 <= m & (arity (n const i)) + 1 = m & m + 1 = arity ((n + 2) proj (n + 2)) & ( for p being FinSequence of NAT st len p = m holds
( ( p +* (n + 1),0 in dom ((n + 1) const i) implies Del p,(n + 1) in dom (n const i) ) & ( Del p,(n + 1) in dom (n const i) implies p +* (n + 1),0 in dom ((n + 1) const i) ) & ( p +* (n + 1),0 in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),0 ) = (n const i) . (Del p,(n + 1)) ) & ( for n being Element of NAT holds
( ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) ) ) & ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) implies p +* (n + 1),(n + 1) in dom ((n + 1) const i) ) & ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),(n + 1)) = ((n + 2) proj (n + 2)) . ((p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*>) ) ) ) ) ) )
thus dom ((n + 1) const i) c= m -tuples_on NAT by Th24; :: thesis: ( n + 1 >= 1 & n + 1 <= m & (arity (n const i)) + 1 = m & m + 1 = arity ((n + 2) proj (n + 2)) & ( for p being FinSequence of NAT st len p = m holds
( ( p +* (n + 1),0 in dom ((n + 1) const i) implies Del p,(n + 1) in dom (n const i) ) & ( Del p,(n + 1) in dom (n const i) implies p +* (n + 1),0 in dom ((n + 1) const i) ) & ( p +* (n + 1),0 in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),0 ) = (n const i) . (Del p,(n + 1)) ) & ( for n being Element of NAT holds
( ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) ) ) & ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) implies p +* (n + 1),(n + 1) in dom ((n + 1) const i) ) & ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),(n + 1)) = ((n + 2) proj (n + 2)) . ((p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*>) ) ) ) ) ) )
thus ( n + 1 >= 1 & n + 1 <= m ) by Th35, NAT_1:11; :: thesis: ( (arity (n const i)) + 1 = m & m + 1 = arity ((n + 2) proj (n + 2)) & ( for p being FinSequence of NAT st len p = m holds
( ( p +* (n + 1),0 in dom ((n + 1) const i) implies Del p,(n + 1) in dom (n const i) ) & ( Del p,(n + 1) in dom (n const i) implies p +* (n + 1),0 in dom ((n + 1) const i) ) & ( p +* (n + 1),0 in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),0 ) = (n const i) . (Del p,(n + 1)) ) & ( for n being Element of NAT holds
( ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) ) ) & ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) implies p +* (n + 1),(n + 1) in dom ((n + 1) const i) ) & ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),(n + 1)) = ((n + 2) proj (n + 2)) . ((p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*>) ) ) ) ) ) )
thus ( (arity (n const i)) + 1 = m & m + 1 = arity ((n + 2) proj (n + 2)) ) by A27, A25, A23, Th35; :: thesis: for p being FinSequence of NAT st len p = m holds
( ( p +* (n + 1),0 in dom ((n + 1) const i) implies Del p,(n + 1) in dom (n const i) ) & ( Del p,(n + 1) in dom (n const i) implies p +* (n + 1),0 in dom ((n + 1) const i) ) & ( p +* (n + 1),0 in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),0 ) = (n const i) . (Del p,(n + 1)) ) & ( for n being Element of NAT holds
( ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) ) ) & ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) implies p +* (n + 1),(n + 1) in dom ((n + 1) const i) ) & ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),(n + 1)) = ((n + 2) proj (n + 2)) . ((p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*>) ) ) ) )
let p be FinSequence of NAT ; :: thesis: ( len p = m implies ( ( p +* (n + 1),0 in dom ((n + 1) const i) implies Del p,(n + 1) in dom (n const i) ) & ( Del p,(n + 1) in dom (n const i) implies p +* (n + 1),0 in dom ((n + 1) const i) ) & ( p +* (n + 1),0 in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),0 ) = (n const i) . (Del p,(n + 1)) ) & ( for n being Element of NAT holds
( ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) ) ) & ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) implies p +* (n + 1),(n + 1) in dom ((n + 1) const i) ) & ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),(n + 1)) = ((n + 2) proj (n + 2)) . ((p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*>) ) ) ) ) )
assume len p = m ; :: thesis: ( ( p +* (n + 1),0 in dom ((n + 1) const i) implies Del p,(n + 1) in dom (n const i) ) & ( Del p,(n + 1) in dom (n const i) implies p +* (n + 1),0 in dom ((n + 1) const i) ) & ( p +* (n + 1),0 in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),0 ) = (n const i) . (Del p,(n + 1)) ) & ( for n being Element of NAT holds
( ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) ) ) & ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) implies p +* (n + 1),(n + 1) in dom ((n + 1) const i) ) & ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),(n + 1)) = ((n + 2) proj (n + 2)) . ((p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*>) ) ) ) )
then A31: p is Element of (n + 1) -tuples_on NAT by A29, FINSEQ_2:110;
A32: n + 1 >= 1 by NAT_1:11;
hence ( p +* (n + 1),0 in dom ((n + 1) const i) implies Del p,(n + 1) in dom (n const i) ) by A28, A31, Th12; :: thesis: ( ( Del p,(n + 1) in dom (n const i) implies p +* (n + 1),0 in dom ((n + 1) const i) ) & ( p +* (n + 1),0 in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),0 ) = (n const i) . (Del p,(n + 1)) ) & ( for n being Element of NAT holds
( ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) ) ) & ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) implies p +* (n + 1),(n + 1) in dom ((n + 1) const i) ) & ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),(n + 1)) = ((n + 2) proj (n + 2)) . ((p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*>) ) ) ) )
thus ( Del p,(n + 1) in dom (n const i) implies p +* (n + 1),0 in dom ((n + 1) const i) ) by A22, A31, A32, Lm7; :: thesis: ( p +* (n + 1),0 in dom ((n + 1) const i) iff ((n + 1) const i) . (p +* (n + 1),0 ) = (n const i) . (Del p,(n + 1)) )
(n const i) . (Del p,(n + 1)) = i by A31, A32, Th12, FUNCOP_1:13;
hence ( p +* (n + 1),0 in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),0 ) = (n const i) . (Del p,(n + 1)) ) by A31, A32, Lm7, FUNCOP_1:13; :: thesis: for n being Element of NAT holds
( ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) ) ) & ( p +* (n + 1),n in dom ((n + 1) const i) & (p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*> in dom ((n + 2) proj (n + 2)) implies p +* (n + 1),(n + 1) in dom ((n + 1) const i) ) & ( p +* (n + 1),(n + 1) in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),(n + 1)) = ((n + 2) proj (n + 2)) . ((p +* (n + 1),n) ^ <*(((n + 1) const i) . (p +* (n + 1),n))*>) ) )
let m be Element of NAT ; :: thesis: ( ( p +* (n + 1),(m + 1) in dom ((n + 1) const i) implies ( p +* (n + 1),m in dom ((n + 1) const i) & (p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*> in dom ((n + 2) proj (n + 2)) ) ) & ( p +* (n + 1),m in dom ((n + 1) const i) & (p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*> in dom ((n + 2) proj (n + 2)) implies p +* (n + 1),(m + 1) in dom ((n + 1) const i) ) & ( p +* (n + 1),(m + 1) in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),(m + 1)) = ((n + 2) proj (n + 2)) . ((p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*>) ) )
A33: p +* (n + 1),m in (n + 1) -tuples_on NAT by A31, A32, Lm7;
then B34: (p +* (n + 1),m) ^ <*i*> is Tuple of n + 2, NAT by A23, FINSEQ_2:127;
then A34: (p +* (n + 1),m) ^ <*i*> is Element of (n + 2) -tuples_on NAT by FINSEQ_2:151;
hereby :: thesis: ( p +* (n + 1),(m + 1) in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),(m + 1)) = ((n + 2) proj (n + 2)) . ((p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*>) )
hereby :: thesis: ( p +* (n + 1),m in dom ((n + 1) const i) & (p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*> in dom ((n + 2) proj (n + 2)) implies p +* (n + 1),(m + 1) in dom ((n + 1) const i) )
assume p +* (n + 1),(m + 1) in dom ((n + 1) const i) ; :: thesis: ( p +* (n + 1),m in dom ((n + 1) const i) & (p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*> in dom ((n + 2) proj (n + 2)) )
thus p +* (n + 1),m in dom ((n + 1) const i) by A22, A31, A32, Lm7; :: thesis: (p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*> in dom ((n + 2) proj (n + 2))
((n + 1) const i) . (p +* (n + 1),m) = i by A31, A32, Lm7, FUNCOP_1:13;
hence (p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*> in dom ((n + 2) proj (n + 2)) by A26, B34, FINSEQ_2:151; :: thesis: verum
end;
thus ( p +* (n + 1),m in dom ((n + 1) const i) & (p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*> in dom ((n + 2) proj (n + 2)) implies p +* (n + 1),(m + 1) in dom ((n + 1) const i) ) by A22, A31, A32, Lm7; :: thesis: verum
end;
assume p +* (n + 1),(m + 1) in dom ((n + 1) const i) ; :: thesis: ((n + 1) const i) . (p +* (n + 1),(m + 1)) = ((n + 2) proj (n + 2)) . ((p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*>)
len (p +* (n + 1),m) = n + 1 by A33, FINSEQ_1:def 18;
then A35: ((p +* (n + 1),m) ^ <*i*>) . ((n + 1) + 1) = i by FINSEQ_1:59;
thus ((n + 1) const i) . (p +* (n + 1),(m + 1)) = i by A31, A32, Lm7, FUNCOP_1:13
.= ((n + 2) proj (n + 2)) . ((p +* (n + 1),m) ^ <*i*>) by A35, A34, Th42
.= ((n + 2) proj (n + 2)) . ((p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*>) by A31, A32, Lm7, FUNCOP_1:13 ; :: thesis: verum
end;
A36: n const i in P by A21;
(n + 1) const i is Element of HFuncs NAT by Th31;
hence (n + 1) const i in P by A19, A30, A36, A24, Def16; :: thesis: verum
end;
end;
A37: S2[ 0 ] by Def17;
for i being Element of NAT holds S2[i] from NAT_1:sch 1(A37, A2);
 then A38: S3[ 0 ] ;
for n being Element of NAT holds S3[n] from NAT_1:sch 1(A38, A20);
 hence n const c in P ; :: thesis: verum