let c, n be Element of NAT ; 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); 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;
( 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
;
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;
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;
verum
end;
A19:
P is primitive-recursion_closed
by Def14;
A20:
now for n being Nat st S3[n] holds
S3[n + 1]let n be
Nat;
( S3[n] implies S3[n + 1] )assume A21:
S3[
n]
;
S3[n + 1]thus
S3[
n + 1]
verumproof
let i be
Element of
NAT ;
(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);
COMPUT_1:def 9 ( 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;
( 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;
( (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;
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 ;
( 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
;
( ( 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;
( ( 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;
( 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;
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;
( ( 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 ( 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 ( 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)
;
( 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)
;
(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;
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;
verum
end;
assume
p +* (
(n + 1),
(m + 1))
in dom ((nn + 1) const i)
;
((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)))*>)
;
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;
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
; verum