let c, n 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[ Nat] means 0 const $1 in P;
defpred S3[ Nat] means for c being Element of NAT holds $1 const c in P;
A1: P is composition_closed by Def14;
A2: for i being Nat st S2[i] holds
S2[i + 1]
proof
reconsider 1succ1 = 1 succ 1 as quasi_total Element of HFuncs NAT by Th28;
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
A3: 1 succ 1 in P by Def14;
A4: <*> NAT is Element of 0 -tuples_on NAT by FINSEQ_2:131;
then A5: (0 const i) . {} = i ;
reconsider 0consti = 0 const i as Element of HFuncs NAT by Th27;
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 Th33
.= len F by FINSEQ_1:39 ;
A8: rng F = {(0 const i)} by FINSEQ_1:39;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
now :: thesis: for h being Element of HFuncs NAT st h in rng F holds
h is quasi_total
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 i1 by A8, TARSKI:def 1;
hence h is quasi_total by Th28; :: thesis: verum
end;
then reconsider g = 1succ1 * <:F:> as quasi_total Element of HFuncs NAT by A7, Th45;
A9: arity (0 const (i + 1)) = 0 by Th31;
A10: (0 const (i + 1)) . {} = i + 1 by A4;
A11: dom (1 succ 1) = 1 -tuples_on NAT by Def7;
A12: arity (0 const i1) = 0 by Th31;
dom (0 const i1) = 0 -tuples_on NAT ;
then A14: <:F:> . {} = <*i*> by A4, A5, FINSEQ_3:141;
reconsider ii = <*i1*> 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, FUNCT_1:13;
then A16: g . {} = (ii /. 1) + 1 by A14, Def7
.= i1 + 1 by FINSEQ_4:16 ;
dom (0 const i) = 0 -tuples_on NAT ;
then <:<*(0 const i)*>:> . {} = ii by A4, A5, FINSEQ_3:141;
then A18: {} in dom g by A4, A15, A11, FUNCT_1:11;
0 const i in rng F by A8, TARSKI:def 1;
then arity F = 0 by A12, Def4;
then arity g = 0 by A18, Th43, RELAT_1:38;
then 0 const (i + 1) = (1 succ 1) * <:<*(0 const i)*>:> by A9, A10, A18, A16, Th47, RELAT_1:38;
hence S2[i + 1] by A1, A6, A8, A3, A7; :: thesis: verum
end;
A19: P is primitive-recursion_closed by Def14;
A20: now :: thesis: for n being Nat st S3[n] holds
S3[n + 1]
let n be 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
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
set g = (nn + 1) const i;
set f1 = nn const i;
set j = n + 1;
set f2 = (nn + 2) proj (nn + 2);
A23: n + (1 + 1) = (n + 1) + 1 ;
then 1 <= n + 2 by NAT_1:11;
then A24: (nn + 2) proj (nn + 2) in P by Def14;
A25: arity ((nn + 2) proj (nn + 2)) = n + 2 by Th36;
A26: dom ((nn + 2) proj (nn + 2)) = (n + 2) -tuples_on NAT by Th35;
A27: arity (nn const i) = n by Th31;
A29: arity ((nn + 1) const i) = n + 1 by Th31;
A30: (nn + 1) const i is_primitive-recursively_expressed_by nn const i,(nn + 2) proj (nn + 2),n + 1
proof
take m = arity ((nn + 1) const i); :: according to COMPUT_1:def 9 :: thesis: ( dom ((nn + 1) const i) c= m -tuples_on NAT & n + 1 >= 1 & n + 1 <= m & (arity (nn const i)) + 1 = m & m + 1 = arity ((nn + 2) proj (nn + 2)) & ( for p being FinSequence of NAT st len p = m holds
( ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies Del (p,(n + 1)) in dom (nn const i) ) & ( Del (p,(n + 1)) in dom (nn const i) implies p +* ((n + 1),0) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),0)) = (nn const i) . (Del (p,(n + 1))) ) & ( for n being Nat holds
( ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) ) ) & ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) implies p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),(n + 1))) = ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*>) ) ) ) ) ) )
thus dom ((nn + 1) const i) c= m -tuples_on NAT by Th20; :: thesis: ( n + 1 >= 1 & n + 1 <= m & (arity (nn const i)) + 1 = m & m + 1 = arity ((nn + 2) proj (nn + 2)) & ( for p being FinSequence of NAT st len p = m holds
( ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies Del (p,(n + 1)) in dom (nn const i) ) & ( Del (p,(n + 1)) in dom (nn const i) implies p +* ((n + 1),0) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),0)) = (nn const i) . (Del (p,(n + 1))) ) & ( for n being Nat holds
( ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) ) ) & ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) implies p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),(n + 1))) = ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*>) ) ) ) ) ) )
thus ( n + 1 >= 1 & n + 1 <= m ) by Th31, NAT_1:11; :: thesis: ( (arity (nn const i)) + 1 = m & m + 1 = arity ((nn + 2) proj (nn + 2)) & ( for p being FinSequence of NAT st len p = m holds
( ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies Del (p,(n + 1)) in dom (nn const i) ) & ( Del (p,(n + 1)) in dom (nn const i) implies p +* ((n + 1),0) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),0)) = (nn const i) . (Del (p,(n + 1))) ) & ( for n being Nat holds
( ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) ) ) & ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) implies p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),(n + 1))) = ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*>) ) ) ) ) ) )
thus ( (arity (nn const i)) + 1 = m & m + 1 = arity ((nn + 2) proj (nn + 2)) ) by A27, A25, A23, Th31; :: thesis: for p being FinSequence of NAT st len p = m holds
( ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies Del (p,(n + 1)) in dom (nn const i) ) & ( Del (p,(n + 1)) in dom (nn const i) implies p +* ((n + 1),0) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),0)) = (nn const i) . (Del (p,(n + 1))) ) & ( for n being Nat holds
( ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) ) ) & ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) implies p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),(n + 1))) = ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*>) ) ) ) )
let p be FinSequence of NAT ; :: thesis: ( len p = m implies ( ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies Del (p,(n + 1)) in dom (nn const i) ) & ( Del (p,(n + 1)) in dom (nn const i) implies p +* ((n + 1),0) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),0)) = (nn const i) . (Del (p,(n + 1))) ) & ( for n being Nat holds
( ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) ) ) & ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) implies p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),(n + 1))) = ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*>) ) ) ) ) )
assume len p = m ; :: thesis: ( ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies Del (p,(n + 1)) in dom (nn const i) ) & ( Del (p,(n + 1)) in dom (nn const i) implies p +* ((n + 1),0) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),0)) = (nn const i) . (Del (p,(n + 1))) ) & ( for n being Nat holds
( ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) ) ) & ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) implies p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),(n + 1))) = ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),n)) ^ <*(((nn + 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 ((nn + 1) const i) implies Del (p,(n + 1)) in dom (nn const i) ) by A31, Th9; :: thesis: ( ( Del (p,(n + 1)) in dom (nn const i) implies p +* ((n + 1),0) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),0)) = (nn const i) . (Del (p,(n + 1))) ) & ( for n being Nat holds
( ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) ) ) & ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) implies p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),(n + 1))) = ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*>) ) ) ) )
thus ( Del (p,(n + 1)) in dom (nn const i) implies p +* ((n + 1),0) in dom ((nn + 1) const i) ) by A31, A32, Lm7; :: thesis: ( p +* ((n + 1),0) in dom ((nn + 1) const i) iff ((nn + 1) const i) . (p +* ((n + 1),0)) = (nn const i) . (Del (p,(n + 1))) )
(nn const i) . (Del (p,(n + 1))) = i by A31, A32, Th9, FUNCOP_1:7;
hence ( p +* ((n + 1),0) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),0)) = (nn const i) . (Del (p,(n + 1))) ) by FUNCOP_1:7; :: thesis: for n being Nat holds
( ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) ) ) & ( p +* ((n + 1),n) in dom ((nn + 1) const i) & (p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*> in dom ((nn + 2) proj (nn + 2)) implies p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),(n + 1)) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),(n + 1))) = ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),n)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),n)))*>) ) )
let m be Nat; :: thesis: ( ( p +* ((n + 1),(m + 1)) in dom ((nn + 1) const i) implies ( p +* ((n + 1),m) in dom ((nn + 1) const i) & (p +* ((n + 1),m)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),m)))*> in dom ((nn + 2) proj (nn + 2)) ) ) & ( p +* ((n + 1),m) in dom ((nn + 1) const i) & (p +* ((n + 1),m)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),m)))*> in dom ((nn + 2) proj (nn + 2)) implies p +* ((n + 1),(m + 1)) in dom ((nn + 1) const i) ) & ( p +* ((n + 1),(m + 1)) in dom ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),(m + 1))) = ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),m)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),m)))*>) ) )
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A33: p +* ((n + 1),mm) in (n + 1) -tuples_on NAT by A31, A32, Lm7;
then A34: (p +* ((n + 1),mm)) ^ <*i*> is Tuple of n + 2, NAT by A23;
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 ((nn + 1) const i) implies ((nn + 1) const i) . (p +* ((n + 1),(m + 1))) = ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),m)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),m)))*>) )
hereby :: thesis: ( p +* ((n + 1),m) in dom ((nn + 1) const i) & (p +* ((n + 1),m)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),m)))*> in dom ((nn + 2) proj (nn + 2)) implies p +* ((n + 1),(m + 1)) in dom ((nn + 1) const i) )
assume p +* ((n + 1),(m + 1)) in dom ((nn + 1) const i) ; :: thesis: ( p +* ((n + 1),m) in dom ((nn + 1) const i) & (p +* ((n + 1),m)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),m)))*> in dom ((nn + 2) proj (nn + 2)) )
p +* ((n + 1),mm) in dom ((nn + 1) const i) by A31, A32, Lm7;
hence p +* ((n + 1),m) in dom ((nn + 1) const i) ; :: thesis: (p +* ((n + 1),m)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),m)))*> in dom ((nn + 2) proj (nn + 2))
((nn + 1) const i) . (p +* ((n + 1),mm)) = i by A31, A32, Lm7, FUNCOP_1:7;
hence (p +* ((n + 1),m)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),m)))*> in dom ((nn + 2) proj (nn + 2)) by A26, A34, FINSEQ_2:131; :: thesis: verum
end;
thus ( p +* ((n + 1),m) in dom ((nn + 1) const i) & (p +* ((n + 1),m)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),m)))*> in dom ((nn + 2) proj (nn + 2)) implies p +* ((n + 1),(m + 1)) in dom ((nn + 1) const i) ) by A31, A32, Lm7; :: thesis: verum
end;
assume p +* ((n + 1),(m + 1)) in dom ((nn + 1) const i) ; :: thesis: ((nn + 1) const i) . (p +* ((n + 1),(m + 1))) = ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),m)) ^ <*(((nn + 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 ((nn + 1) const i) . (p +* ((n + 1),(m + 1))) = i by A31, A32, Lm7, FUNCOP_1:7
.= ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),m)) ^ <*i*>) by A36, A35, Th37
.= ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),mm)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),mm)))*>) by A31, A32, Lm7, FUNCOP_1:7
.= ((nn + 2) proj (nn + 2)) . ((p +* ((n + 1),m)) ^ <*(((nn + 1) const i) . (p +* ((n + 1),m)))*>) ; :: thesis: verum
end;
A37: nn const i in P by A21;
(n + 1) const i is Element of HFuncs NAT by Th27;
hence (n + 1) const i in P by A19, A30, A37, A24; :: thesis: verum
end;
end;
A38: S2[ 0 ] by Def14;
for i being Nat holds S2[i] from NAT_1:sch 2(A38, A2);
 then A39: S3[ 0 ] ;
for n being Nat holds S3[n] from NAT_1:sch 2(A39, A20);
 hence n const c in P ; :: thesis: verum