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:131;
then A5: (0 const i) . {} = i by FUNCOP_1:7;
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:31;
A7: arity (1 succ 1) = 1 by Th38
.= len F by FINSEQ_1:39 ;
A8: rng F = {(0 const i)} by FINSEQ_1:39;
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:7;
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, FINSEQ_3:141;
reconsider ii = <*i*> as Element of 1 -tuples_on NAT by FINSEQ_2:131;
A15: dom <:<*(0 const i)*>:> = dom (0 const i) by FINSEQ_3:141;
then g . {} = (1 succ 1) . (<:F:> . {}) by A4, A13, FUNCT_1:13;
then A16: g . {} = (ii /. 1) + 1 by A14, Def10
.= i + 1 by FINSEQ_4:16 ;
A17: dom (0 const i) = 0 -tuples_on NAT by A12, Th26;
then <:<*(0 const i)*>:> . {} = ii by A4, A5, FINSEQ_3:141;
then A18: {} in dom g by A4, A15, A17, A11, FUNCT_1:11;
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:38;
then 0 const (i + 1) = (1 succ 1) * <:<*(0 const i)*>:> by A9, A10, A18, A16, Th52, RELAT_1:38;
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:13;
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:13;
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 9 :: 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:92;
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:7;
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:7; :: 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 A34: (p +* ((n + 1),m)) ^ <*i*> is Tuple of n + 2, NAT by A23, FINSEQ_2:107;
then A35: (p +* ((n + 1),m)) ^ <*i*> is Element of (n + 2) -tuples_on NAT by FINSEQ_2:131;
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:7;
hence (p +* ((n + 1),m)) ^ <*(((n + 1) const i) . (p +* ((n + 1),m)))*> in dom ((n + 2) proj (n + 2)) by A26, A34, FINSEQ_2:131; :: 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, CARD_1:def 7;
then A36: ((p +* ((n + 1),m)) ^ <*i*>) . ((n + 1) + 1) = i by FINSEQ_1:42;
thus ((n + 1) const i) . (p +* ((n + 1),(m + 1))) = i by A31, A32, Lm7, FUNCOP_1:7
.= ((n + 2) proj (n + 2)) . ((p +* ((n + 1),m)) ^ <*i*>) by A36, A35, Th42
.= ((n + 2) proj (n + 2)) . ((p +* ((n + 1),m)) ^ <*(((n + 1) const i) . (p +* ((n + 1),m)))*>) by A31, A32, Lm7, FUNCOP_1:7 ; :: thesis: verum
end;
A37: 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, A37, A24, Def16; :: thesis: verum
end;
end;
A38: S2[ 0 ] by Def17;
for i being Element of NAT holds S2[i] from NAT_1:sch 1(A38, A2);
 then A39: S3[ 0 ] ;
for n being Element of NAT holds S3[n] from NAT_1:sch 1(A39, A20);
 hence n const c in P ; :: thesis: verum