begin
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem
canceled;
theorem Th5:
for
a,
x,
y,
z being
set for
f,
g being
Function st
f +* (
a,
x)
= g +* (
a,
y) holds
f +* (
a,
z)
= g +* (
a,
z)
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
begin
:: deftheorem Def1 defines compatible COMPUT_1:def 1 :
for X being set holds
( X is compatible iff for f, g being Function st f in X & g in X holds
f tolerates g );
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
begin
:: deftheorem COMPUT_1:def 2 :
canceled;
:: deftheorem Def3 defines len-total COMPUT_1:def 3 :
for f being NAT * -defined Relation holds
( f is len-total iff for x, y being FinSequence of NAT st len x = len y & x in dom f holds
y in dom f );
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
Lm1:
for D being non empty set
for f being homogeneous PartFunc of (D *),D holds
( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on D )
theorem Th25:
theorem Th26:
theorem
theorem Th28:
:: deftheorem COMPUT_1:def 4 :
canceled;
:: deftheorem COMPUT_1:def 5 :
canceled;
:: deftheorem Def6 defines with_the_same_arity COMPUT_1:def 6 :
for R being Relation holds
( R is with_the_same_arity iff for f, g being Function st f in rng R & g in rng R holds
( ( not f is empty or g is empty or dom g = {{}} ) & ( not f is empty & not g is empty implies ex n being Element of NAT ex X being non empty set st
( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) ) ) );
:: deftheorem Def7 defines arity COMPUT_1:def 7 :
for F being with_the_same_arity Relation
for b2 being Element of NAT holds
( ( ex f being homogeneous Function st f in rng F implies ( b2 = arity F iff for f being homogeneous Function st f in rng F holds
b2 = arity f ) ) & ( ( for f being homogeneous Function holds not f in rng F ) implies ( b2 = arity F iff b2 = 0 ) ) );
theorem
:: deftheorem defines HFuncs COMPUT_1:def 8 :
for X being set holds HFuncs X = { f where f is Element of PFuncs ((X *),X) : f is homogeneous } ;
theorem
theorem Th31:
theorem Th32:
theorem Th33:
:: deftheorem defines const COMPUT_1:def 9 :
for n, m being Element of NAT holds n const m = (n -tuples_on NAT) --> m;
theorem Th34:
theorem Th35:
:: deftheorem Def10 defines succ COMPUT_1:def 10 :
for n, i being Element of NAT
for b3 being NAT * -defined to-naturals homogeneous Function holds
( b3 = n succ i iff ( dom b3 = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds b3 . p = (p /. i) + 1 ) ) );
theorem
canceled;
theorem Th37:
theorem Th38:
:: deftheorem defines proj COMPUT_1:def 11 :
for n, i being Element of NAT holds n proj i = proj ((n |-> NAT),i);
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem
theorem Th45:
theorem Th46:
theorem
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
begin
definition
let g,
f1,
f2 be
NAT * -defined to-naturals homogeneous Function;
let i be
Element of
NAT ;
pred g is_primitive-recursively_expressed_by f1,
f2,
i means :
Def12:
ex
n being
Element of
NAT st
(
dom g c= n -tuples_on NAT &
i >= 1 &
i <= n &
(arity f1) + 1
= n &
n + 1
= arity f2 & ( 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
n being
Element of
NAT holds
( (
p +* (
i,
(n + 1))
in dom g implies (
p +* (
i,
n)
in dom g &
(p +* (i,n)) ^ <*(g . (p +* (i,n)))*> in dom f2 ) ) & (
p +* (
i,
n)
in dom g &
(p +* (i,n)) ^ <*(g . (p +* (i,n)))*> in dom f2 implies
p +* (
i,
(n + 1))
in dom g ) & (
p +* (
i,
(n + 1))
in dom g implies
g . (p +* (i,(n + 1))) = f2 . ((p +* (i,n)) ^ <*(g . (p +* (i,n)))*>) ) ) ) ) ) );
end;
:: deftheorem Def12 defines is_primitive-recursively_expressed_by COMPUT_1:def 12 :
for g, f1, f2 being NAT * -defined to-naturals homogeneous Function
for i being Element of NAT holds
( g is_primitive-recursively_expressed_by f1,f2,i iff ex n being Element of NAT st
( dom g c= n -tuples_on NAT & i >= 1 & i <= n & (arity f1) + 1 = n & n + 1 = arity f2 & ( 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 n being Element of NAT holds
( ( p +* (i,(n + 1)) in dom g implies ( p +* (i,n) in dom g & (p +* (i,n)) ^ <*(g . (p +* (i,n)))*> in dom f2 ) ) & ( p +* (i,n) in dom g & (p +* (i,n)) ^ <*(g . (p +* (i,n)))*> in dom f2 implies p +* (i,(n + 1)) in dom g ) & ( p +* (i,(n + 1)) in dom g implies g . (p +* (i,(n + 1))) = f2 . ((p +* (i,n)) ^ <*(g . (p +* (i,n)))*>) ) ) ) ) ) ) );
defpred S1[ Element of NAT , Element of HFuncs NAT, Element of HFuncs NAT, FinSequence of NAT , Element of NAT , homogeneous Function] means ( ( $5 in dom $4 & $4 +* ($5,$1) in dom $2 & ($4 +* ($5,$1)) ^ <*($2 . ($4 +* ($5,$1)))*> in dom $6 implies $3 = $2 +* (($4 +* ($5,($1 + 1))) .--> ($6 . (($4 +* ($5,$1)) ^ <*($2 . ($4 +* ($5,$1)))*>))) ) & ( ( not $5 in dom $4 or not $4 +* ($5,$1) in dom $2 or not ($4 +* ($5,$1)) ^ <*($2 . ($4 +* ($5,$1)))*> in dom $6 ) implies $3 = $2 ) );
definition
let f1,
f2 be
NAT * -defined to-naturals homogeneous Function;
let i be
Element of
NAT ;
let p be
FinSequence of
NAT ;
func primrec (
f1,
f2,
i,
p)
-> Element of
HFuncs NAT means :
Def13:
ex
F being
Function of
NAT,
(HFuncs NAT) st
(
it = F . (p /. i) & (
i in dom p &
Del (
p,
i)
in dom f1 implies
F . 0 = (p +* (i,0)) .--> (f1 . (Del (p,i))) ) & ( ( not
i in dom p or not
Del (
p,
i)
in dom f1 ) implies
F . 0 = {} ) & ( for
m being
Element of
NAT holds
( (
i in dom p &
p +* (
i,
m)
in dom (F . m) &
(p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom f2 implies
F . (m + 1) = (F . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>))) ) & ( ( not
i in dom p or not
p +* (
i,
m)
in dom (F . m) or not
(p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom f2 ) implies
F . (m + 1) = F . m ) ) ) );
existence
ex b1 being Element of HFuncs NAT ex F being Function of NAT,(HFuncs NAT) st
( b1 = F . (p /. i) & ( i in dom p & Del (p,i) in dom f1 implies F . 0 = (p +* (i,0)) .--> (f1 . (Del (p,i))) ) & ( ( not i in dom p or not Del (p,i) in dom f1 ) implies F . 0 = {} ) & ( for m being Element of NAT holds
( ( i in dom p & p +* (i,m) in dom (F . m) & (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom f2 implies F . (m + 1) = (F . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>))) ) & ( ( not i in dom p or not p +* (i,m) in dom (F . m) or not (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom f2 ) implies F . (m + 1) = F . m ) ) ) )
uniqueness
for b1, b2 being Element of HFuncs NAT st ex F being Function of NAT,(HFuncs NAT) st
( b1 = F . (p /. i) & ( i in dom p & Del (p,i) in dom f1 implies F . 0 = (p +* (i,0)) .--> (f1 . (Del (p,i))) ) & ( ( not i in dom p or not Del (p,i) in dom f1 ) implies F . 0 = {} ) & ( for m being Element of NAT holds
( ( i in dom p & p +* (i,m) in dom (F . m) & (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom f2 implies F . (m + 1) = (F . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>))) ) & ( ( not i in dom p or not p +* (i,m) in dom (F . m) or not (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom f2 ) implies F . (m + 1) = F . m ) ) ) ) & ex F being Function of NAT,(HFuncs NAT) st
( b2 = F . (p /. i) & ( i in dom p & Del (p,i) in dom f1 implies F . 0 = (p +* (i,0)) .--> (f1 . (Del (p,i))) ) & ( ( not i in dom p or not Del (p,i) in dom f1 ) implies F . 0 = {} ) & ( for m being Element of NAT holds
( ( i in dom p & p +* (i,m) in dom (F . m) & (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom f2 implies F . (m + 1) = (F . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>))) ) & ( ( not i in dom p or not p +* (i,m) in dom (F . m) or not (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom f2 ) implies F . (m + 1) = F . m ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def13 defines primrec COMPUT_1:def 13 :
for f1, f2 being NAT * -defined to-naturals homogeneous Function
for i being Element of NAT
for p being FinSequence of NAT
for b5 being Element of HFuncs NAT holds
( b5 = primrec (f1,f2,i,p) iff ex F being Function of NAT,(HFuncs NAT) st
( b5 = F . (p /. i) & ( i in dom p & Del (p,i) in dom f1 implies F . 0 = (p +* (i,0)) .--> (f1 . (Del (p,i))) ) & ( ( not i in dom p or not Del (p,i) in dom f1 ) implies F . 0 = {} ) & ( for m being Element of NAT holds
( ( i in dom p & p +* (i,m) in dom (F . m) & (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom f2 implies F . (m + 1) = (F . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>))) ) & ( ( not i in dom p or not p +* (i,m) in dom (F . m) or not (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom f2 ) implies F . (m + 1) = F . m ) ) ) ) );
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
definition
let f1,
f2 be
NAT * -defined to-naturals homogeneous Function;
let i be
Element of
NAT ;
func primrec (
f1,
f2,
i)
-> Element of
HFuncs NAT means :
Def14:
ex
G being
Function of
(((arity f1) + 1) -tuples_on NAT),
(HFuncs NAT) st
(
it = Union G & ( for
p being
Element of
((arity f1) + 1) -tuples_on NAT holds
G . p = primrec (
f1,
f2,
i,
p) ) );
existence
ex b1 being Element of HFuncs NAT ex G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st
( b1 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) )
uniqueness
for b1, b2 being Element of HFuncs NAT st ex G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st
( b1 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) ) & ex G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st
( b2 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) ) holds
b1 = b2
end;
:: deftheorem Def14 defines primrec COMPUT_1:def 14 :
for f1, f2 being NAT * -defined to-naturals homogeneous Function
for i being Element of NAT
for b4 being Element of HFuncs NAT holds
( b4 = primrec (f1,f2,i) iff ex G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st
( b4 = Union G & ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) ) );
theorem Th59:
theorem Th60:
theorem Th61:
Lm2:
now
let f1,
f2 be non
empty NAT * -defined to-naturals homogeneous Function;
for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Element of NAT
for F1, F being Function of NAT,(HFuncs NAT) st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) & ( for M being Element of NAT holds S1[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),i,f2] ) & ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = {((p +* (i,m)) +* (i,0))} --> (f1 . (Del ((p +* (i,m)),i))) ) & ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Element of NAT holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] ) holds
F1 = Flet p be
Element of
((arity f1) + 1) -tuples_on NAT;
for i, m being Element of NAT
for F1, F being Function of NAT,(HFuncs NAT) st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) & ( for M being Element of NAT holds S1[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),i,f2] ) & ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = {((p +* (i,m)) +* (i,0))} --> (f1 . (Del ((p +* (i,m)),i))) ) & ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Element of NAT holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] ) holds
F1 = Flet i,
m be
Element of
NAT ;
for F1, F being Function of NAT,(HFuncs NAT) st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) & ( for M being Element of NAT holds S1[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),i,f2] ) & ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = {((p +* (i,m)) +* (i,0))} --> (f1 . (Del ((p +* (i,m)),i))) ) & ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Element of NAT holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] ) holds
F1 = Fset pm1 =
p +* (
i,
(m + 1));
set pm =
p +* (
i,
m);
let F1,
F be
Function of
NAT,
(HFuncs NAT);
( ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) & ( for M being Element of NAT holds S1[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),i,f2] ) & ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = {((p +* (i,m)) +* (i,0))} --> (f1 . (Del ((p +* (i,m)),i))) ) & ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Element of NAT holds S1[M,F . M,F . (M + 1),p +* (i,m),i,f2] ) implies F1 = F )assume that A1:
(
i in dom (p +* (i,(m + 1))) &
Del (
(p +* (i,(m + 1))),
i)
in dom f1 implies
F1 . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) )
and A2:
( ( not
i in dom (p +* (i,(m + 1))) or not
Del (
(p +* (i,(m + 1))),
i)
in dom f1 ) implies
F1 . 0 = {} )
and A3:
for
M being
Element of
NAT holds
S1[
M,
F1 . M,
F1 . (M + 1),
p +* (
i,
(m + 1)),
i,
f2]
and A4:
(
i in dom (p +* (i,m)) &
Del (
(p +* (i,m)),
i)
in dom f1 implies
F . 0 = {((p +* (i,m)) +* (i,0))} --> (f1 . (Del ((p +* (i,m)),i))) )
and A5:
( ( not
i in dom (p +* (i,m)) or not
Del (
(p +* (i,m)),
i)
in dom f1 ) implies
F . 0 = {} )
and A6:
for
M being
Element of
NAT holds
S1[
M,
F . M,
F . (M + 1),
p +* (
i,
m),
i,
f2]
;
F1 = FA7:
dom p = dom (p +* (i,m))
by FUNCT_7:32;
A8:
(p +* (i,m)) +* (
i,
0) =
p +* (
i,
0)
by FUNCT_7:36
.=
(p +* (i,(m + 1))) +* (
i,
0)
by FUNCT_7:36
;
A9:
dom p = dom (p +* (i,(m + 1)))
by FUNCT_7:32;
A10:
Del (
(p +* (i,m)),
i) =
Del (
p,
i)
by Th6
.=
Del (
(p +* (i,(m + 1))),
i)
by Th6
;
for
x being
set st
x in NAT holds
F . x = F1 . x
proof
let x be
set ;
( x in NAT implies F . x = F1 . x )
defpred S2[
Element of
NAT ]
means F . $1
= F1 . $1;
A11:
for
k being
Element of
NAT st
S2[
k] holds
S2[
k + 1]
proof
let k be
Element of
NAT ;
( S2[k] implies S2[k + 1] )
assume A12:
S2[
k]
;
S2[k + 1]
A13:
(p +* (i,m)) +* (
i,
(k + 1)) =
p +* (
i,
(k + 1))
by FUNCT_7:36
.=
(p +* (i,(m + 1))) +* (
i,
(k + 1))
by FUNCT_7:36
;
A14:
(p +* (i,m)) +* (
i,
k) =
p +* (
i,
k)
by FUNCT_7:36
.=
(p +* (i,(m + 1))) +* (
i,
k)
by FUNCT_7:36
;
per cases
( ( i in dom (p +* (i,m)) & (p +* (i,m)) +* (i,k) in dom (F . k) & ((p +* (i,m)) +* (i,k)) ^ <*((F . k) . ((p +* (i,m)) +* (i,k)))*> in dom f2 ) or not i in dom (p +* (i,m)) or not (p +* (i,m)) +* (i,k) in dom (F . k) or not ((p +* (i,m)) +* (i,k)) ^ <*((F . k) . ((p +* (i,m)) +* (i,k)))*> in dom f2 )
;
suppose A15:
(
i in dom (p +* (i,m)) &
(p +* (i,m)) +* (
i,
k)
in dom (F . k) &
((p +* (i,m)) +* (i,k)) ^ <*((F . k) . ((p +* (i,m)) +* (i,k)))*> in dom f2 )
;
S2[k + 1]
hence F . (k + 1) =
(F . k) +* (((p +* (i,m)) +* (i,(k + 1))) .--> (f2 . (((p +* (i,m)) +* (i,k)) ^ <*((F . k) . ((p +* (i,m)) +* (i,k)))*>)))
by A6
.=
F1 . (k + 1)
by A3, A7, A9, A12, A14, A13, A15
;
verum
end;
end;
end;
A17:
S2[
0 ]
by A1, A2, A4, A5, A7, A8, A10, FUNCT_7:32;
A18:
for
k being
Element of
NAT holds
S2[
k]
from NAT_1:sch 1(A17, A11);
assume
x in NAT
;
F . x = F1 . x
hence
F . x = F1 . x
by A18;
verum
end;
hence
F1 = F
by FUNCT_2:18;
verum
end;
Lm3:
now
let f1,
f2 be non
empty NAT * -defined to-naturals homogeneous Function;
for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Element of NAT st i in dom p holds
for F being Function of NAT,(HFuncs NAT) st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Element of NAT holds S1[M,F . M,F . (M + 1),p +* (i,(m + 1)),i,f2] ) holds
( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) )let p be
Element of
((arity f1) + 1) -tuples_on NAT;
for i, m being Element of NAT st i in dom p holds
for F being Function of NAT,(HFuncs NAT) st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Element of NAT holds S1[M,F . M,F . (M + 1),p +* (i,(m + 1)),i,f2] ) holds
( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) )let i,
m be
Element of
NAT ;
( i in dom p implies for F being Function of NAT,(HFuncs NAT) st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Element of NAT holds S1[M,F . M,F . (M + 1),p +* (i,(m + 1)),i,f2] ) holds
( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) ) )assume A1:
i in dom p
;
for F being Function of NAT,(HFuncs NAT) st ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Element of NAT holds S1[M,F . M,F . (M + 1),p +* (i,(m + 1)),i,f2] ) holds
( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) )set pm =
p +* (
i,
m);
set pm1 =
p +* (
i,
(m + 1));
let F be
Function of
NAT,
(HFuncs NAT);
( ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) ) & ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F . 0 = {} ) & ( for M being Element of NAT holds S1[M,F . M,F . (M + 1),p +* (i,(m + 1)),i,f2] ) implies ( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) ) )assume that A2:
(
i in dom (p +* (i,(m + 1))) &
Del (
(p +* (i,(m + 1))),
i)
in dom f1 implies
F . 0 = {((p +* (i,(m + 1))) +* (i,0))} --> (f1 . (Del ((p +* (i,(m + 1))),i))) )
and A3:
( ( not
i in dom (p +* (i,(m + 1))) or not
Del (
(p +* (i,(m + 1))),
i)
in dom f1 ) implies
F . 0 = {} )
and A4:
for
M being
Element of
NAT holds
S1[
M,
F . M,
F . (M + 1),
p +* (
i,
(m + 1)),
i,
f2]
;
( (F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m)) & not p +* (i,(m + 1)) in dom (F . m) )thus
(F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m))
not p +* (i,(m + 1)) in dom (F . m)
proof
per cases
( ( i in dom (p +* (i,(m + 1))) & (p +* (i,(m + 1))) +* (i,m) in dom (F . m) & ((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 ) or not i in dom (p +* (i,(m + 1))) or not (p +* (i,(m + 1))) +* (i,m) in dom (F . m) or not ((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 )
;
suppose A5:
(
i in dom (p +* (i,(m + 1))) &
(p +* (i,(m + 1))) +* (
i,
m)
in dom (F . m) &
((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 )
;
(F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m))
A6:
p +* (
i,
(m + 1))
= (p +* (i,(m + 1))) +* (
i,
(m + 1))
by FUNCT_7:36;
A7:
(p +* (i,(m + 1))) . i = m + 1
by A1, FUNCT_7:33;
(p +* (i,m)) . i = m
by A1, FUNCT_7:33;
then
p +* (
i,
m)
<> p +* (
i,
(m + 1))
by A7;
then A8:
not
p +* (
i,
m)
in dom ({((p +* (i,(m + 1))) +* (i,(m + 1)))} --> (f2 . (((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*>)))
by A6, TARSKI:def 1;
F . (m + 1) = (F . m) +* (((p +* (i,(m + 1))) +* (i,(m + 1))) .--> (f2 . (((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*>)))
by A4, A5;
hence
(F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m))
by A8, FUNCT_4:12;
verum
end;
suppose
( not
i in dom (p +* (i,(m + 1))) or not
(p +* (i,(m + 1))) +* (
i,
m)
in dom (F . m) or not
((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 )
;
(F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m))
hence
(F . (m + 1)) . (p +* (i,m)) = (F . m) . (p +* (i,m))
by A4;
verum
end;
end;
end;
A9:
for
m,
k being
Element of
NAT st
p +* (
i,
k)
in dom (F . m) holds
k <= m
proof
defpred S2[
Element of
NAT ]
means for
k being
Element of
NAT st
p +* (
i,
k)
in dom (F . $1) holds
k <= $1;
A10:
for
m being
Element of
NAT st
S2[
m] holds
S2[
m + 1]
proof
let m be
Element of
NAT ;
( S2[m] implies S2[m + 1] )
assume A11:
S2[
m]
;
S2[m + 1]
let k be
Element of
NAT ;
( p +* (i,k) in dom (F . (m + 1)) implies k <= m + 1 )
assume A12:
p +* (
i,
k)
in dom (F . (m + 1))
;
k <= m + 1
per cases
( ( i in dom (p +* (i,(m + 1))) & (p +* (i,(m + 1))) +* (i,m) in dom (F . m) & ((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 ) or not i in dom (p +* (i,(m + 1))) or not (p +* (i,(m + 1))) +* (i,m) in dom (F . m) or not ((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 )
;
suppose
(
i in dom (p +* (i,(m + 1))) &
(p +* (i,(m + 1))) +* (
i,
m)
in dom (F . m) &
((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 )
;
k <= m + 1
then
F . (m + 1) = (F . m) +* (((p +* (i,(m + 1))) +* (i,(m + 1))) .--> (f2 . (((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*>)))
by A4;
then
dom (F . (m + 1)) = (dom (F . m)) \/ (dom ({((p +* (i,(m + 1))) +* (i,(m + 1)))} --> (f2 . (((p +* (i,(m + 1))) +* (i,m)) ^ <*((F . m) . ((p +* (i,(m + 1))) +* (i,m)))*>))))
by FUNCT_4:def 1;
then A13:
dom (F . (m + 1)) = (dom (F . m)) \/ {((p +* (i,(m + 1))) +* (i,(m + 1)))}
by FUNCOP_1:19;
thus
k <= m + 1
verum
end;
end;
end;
A18:
S2[
0 ]
proof
let k be
Element of
NAT ;
( p +* (i,k) in dom (F . 0) implies k <= 0 )
assume A19:
p +* (
i,
k)
in dom (F . 0)
;
k <= 0
per cases
( ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 ) or not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 )
;
suppose
(
i in dom (p +* (i,(m + 1))) &
Del (
(p +* (i,(m + 1))),
i)
in dom f1 )
;
k <= 0
then
dom (F . 0) = {((p +* (i,(m + 1))) +* (i,0))}
by A2, FUNCOP_1:19;
then A20:
p +* (
i,
k) =
(p +* (i,(m + 1))) +* (
i,
0)
by A19, TARSKI:def 1
.=
p +* (
i,
0)
by FUNCT_7:36
;
k =
(p +* (i,k)) . i
by A1, FUNCT_7:33
.=
0
by A1, A20, FUNCT_7:33
;
hence
k <= 0
;
verum
end;
end;
end;
thus
for
n being
Element of
NAT holds
S2[
n]
from NAT_1:sch 1(A18, A10); verum
end;
thus
not
p +* (
i,
(m + 1))
in dom (F . m)
verum
end;
Lm4:
now
let f1,
f2 be non
empty NAT * -defined to-naturals homogeneous Function;
for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Element of NAT st i in dom p holds
for G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Element of NAT holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n))))let p be
Element of
((arity f1) + 1) -tuples_on NAT;
for i, m being Element of NAT st i in dom p holds
for G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Element of NAT holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n))))let i,
m be
Element of
NAT ;
( i in dom p implies for G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Element of NAT holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n)))) )assume A1:
i in dom p
;
for G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Element of NAT holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n))))let G be
Function of
(((arity f1) + 1) -tuples_on NAT),
(HFuncs NAT);
( ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) implies for k, n being Element of NAT holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n)))) )assume A2:
for
p being
Element of
((arity f1) + 1) -tuples_on NAT holds
G . p = primrec (
f1,
f2,
i,
p)
;
for k, n being Element of NAT holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n))))thus
for
k,
n being
Element of
NAT holds
dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n))))
verum
proof
let k be
Element of
NAT ;
for n being Element of NAT holds dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + n))))
set pk =
p +* (
i,
k);
defpred S2[
Element of
NAT ]
means dom (G . (p +* (i,k))) c= dom (G . (p +* (i,(k + $1))));
A3:
now
let n be
Element of
NAT ;
( S2[n] implies S2[b1 + 1] )assume A4:
S2[
n]
;
S2[b1 + 1]set m =
k + n;
set pkn1 =
p +* (
i,
((k + n) + 1));
set pkn =
p +* (
i,
(k + n));
consider F being
Function of
NAT,
(HFuncs NAT) such that A5:
primrec (
f1,
f2,
i,
(p +* (i,(k + n))))
= F . ((p +* (i,(k + n))) /. i)
and A6:
(
i in dom (p +* (i,(k + n))) &
Del (
(p +* (i,(k + n))),
i)
in dom f1 implies
F . 0 = ((p +* (i,(k + n))) +* (i,0)) .--> (f1 . (Del ((p +* (i,(k + n))),i))) )
and A7:
( ( not
i in dom (p +* (i,(k + n))) or not
Del (
(p +* (i,(k + n))),
i)
in dom f1 ) implies
F . 0 = {} )
and A8:
for
M being
Element of
NAT holds
S1[
M,
F . M,
F . (M + 1),
p +* (
i,
(k + n)),
i,
f2]
by Def13;
dom p = dom (p +* (i,((k + n) + 1)))
by FUNCT_7:32;
then A9:
(p +* (i,((k + n) + 1))) /. i =
(p +* (i,((k + n) + 1))) . i
by A1, PARTFUN1:def 8
.=
(k + n) + 1
by A1, FUNCT_7:33
;
consider F1 being
Function of
NAT,
(HFuncs NAT) such that A10:
primrec (
f1,
f2,
i,
(p +* (i,((k + n) + 1))))
= F1 . ((p +* (i,((k + n) + 1))) /. i)
and A11:
(
i in dom (p +* (i,((k + n) + 1))) &
Del (
(p +* (i,((k + n) + 1))),
i)
in dom f1 implies
F1 . 0 = ((p +* (i,((k + n) + 1))) +* (i,0)) .--> (f1 . (Del ((p +* (i,((k + n) + 1))),i))) )
and A12:
( ( not
i in dom (p +* (i,((k + n) + 1))) or not
Del (
(p +* (i,((k + n) + 1))),
i)
in dom f1 ) implies
F1 . 0 = {} )
and A13:
for
M being
Element of
NAT holds
S1[
M,
F1 . M,
F1 . (M + 1),
p +* (
i,
((k + n) + 1)),
i,
f2]
by Def13;
F1 = F
by A6, A7, A8, A11, A12, A13, Lm2;
then A14:
G . (p +* (i,(k + (n + 1)))) = F . ((k + n) + 1)
by A2, A10, A9;
dom p = dom (p +* (i,(k + n)))
by FUNCT_7:32;
then (p +* (i,(k + n))) /. i =
(p +* (i,(k + n))) . i
by A1, PARTFUN1:def 8
.=
k + n
by A1, FUNCT_7:33
;
then A15:
G . (p +* (i,(k + n))) = F . (k + n)
by A2, A5;
per cases
( ( i in dom (p +* (i,(k + n))) & (p +* (i,(k + n))) +* (i,(k + n)) in dom (F . (k + n)) & ((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> in dom f2 ) or not i in dom (p +* (i,(k + n))) or not (p +* (i,(k + n))) +* (i,(k + n)) in dom (F . (k + n)) or not ((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> in dom f2 )
;
suppose
(
i in dom (p +* (i,(k + n))) &
(p +* (i,(k + n))) +* (
i,
(k + n))
in dom (F . (k + n)) &
((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> in dom f2 )
;
S2[b1 + 1]
then
F . ((k + n) + 1) = (F . (k + n)) +* (((p +* (i,(k + n))) +* (i,((k + n) + 1))) .--> (f2 . (((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*>)))
by A8;
then
dom (F . ((k + n) + 1)) = (dom (F . (k + n))) \/ (dom ({((p +* (i,(k + n))) +* (i,((k + n) + 1)))} --> (f2 . (((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*>))))
by FUNCT_4:def 1;
then
dom (F . (k + n)) c= dom (F . ((k + n) + 1))
by XBOOLE_1:7;
hence
S2[
n + 1]
by A4, A14, A15, XBOOLE_1:1;
verum
end;
end;
end;
A16:
S2[
0 ]
;
thus
for
n being
Element of
NAT holds
S2[
n]
from NAT_1:sch 1(A16, A3); verum
end;
end;
Lm5:
now
let f1,
f2 be non
empty NAT * -defined to-naturals homogeneous Function;
for p being Element of ((arity f1) + 1) -tuples_on NAT
for i, m being Element of NAT st i in dom p holds
for G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Element of NAT st not p +* (i,k) in dom (G . (p +* (i,k))) holds
not p +* (i,k) in dom (G . (p +* (i,(k + n))))let p be
Element of
((arity f1) + 1) -tuples_on NAT;
for i, m being Element of NAT st i in dom p holds
for G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Element of NAT st not p +* (i,k) in dom (G . (p +* (i,k))) holds
not p +* (i,k) in dom (G . (p +* (i,(k + n))))let i,
m be
Element of
NAT ;
( i in dom p implies for G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Element of NAT st not p +* (i,k) in dom (G . (p +* (i,k))) holds
not p +* (i,k) in dom (G . (p +* (i,(k + n)))) )assume A1:
i in dom p
;
for G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) st ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) holds
for k, n being Element of NAT st not p +* (i,k) in dom (G . (p +* (i,k))) holds
not p +* (i,k) in dom (G . (p +* (i,(k + n))))let G be
Function of
(((arity f1) + 1) -tuples_on NAT),
(HFuncs NAT);
( ( for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) ) implies for k, n being Element of NAT st not p +* (i,k) in dom (G . (p +* (i,k))) holds
not p +* (i,k) in dom (G . (p +* (i,(k + n)))) )assume A2:
for
p being
Element of
((arity f1) + 1) -tuples_on NAT holds
G . p = primrec (
f1,
f2,
i,
p)
;
for k, n being Element of NAT st not p +* (i,k) in dom (G . (p +* (i,k))) holds
not p +* (i,k) in dom (G . (p +* (i,(k + n))))thus
for
k,
n being
Element of
NAT st not
p +* (
i,
k)
in dom (G . (p +* (i,k))) holds
not
p +* (
i,
k)
in dom (G . (p +* (i,(k + n))))
verum
proof
let k be
Element of
NAT ;
for n being Element of NAT st not p +* (i,k) in dom (G . (p +* (i,k))) holds
not p +* (i,k) in dom (G . (p +* (i,(k + n))))
set pk =
p +* (
i,
k);
defpred S2[
Element of
NAT ]
means ( not
p +* (
i,
k)
in dom (G . (p +* (i,k))) implies not
p +* (
i,
k)
in dom (G . (p +* (i,(k + $1)))) );
A3:
for
n being
Element of
NAT st
S2[
n] holds
S2[
n + 1]
proof
let n be
Element of
NAT ;
( S2[n] implies S2[n + 1] )
assume that A4:
S2[
n]
and A5:
not
p +* (
i,
k)
in dom (G . (p +* (i,k)))
;
not p +* (i,k) in dom (G . (p +* (i,(k + (n + 1)))))
set m =
k + n;
set pkn =
p +* (
i,
(k + n));
consider F being
Function of
NAT,
(HFuncs NAT) such that A6:
primrec (
f1,
f2,
i,
(p +* (i,(k + n))))
= F . ((p +* (i,(k + n))) /. i)
and A7:
(
i in dom (p +* (i,(k + n))) &
Del (
(p +* (i,(k + n))),
i)
in dom f1 implies
F . 0 = ((p +* (i,(k + n))) +* (i,0)) .--> (f1 . (Del ((p +* (i,(k + n))),i))) )
and A8:
( ( not
i in dom (p +* (i,(k + n))) or not
Del (
(p +* (i,(k + n))),
i)
in dom f1 ) implies
F . 0 = {} )
and A9:
for
M being
Element of
NAT holds
S1[
M,
F . M,
F . (M + 1),
p +* (
i,
(k + n)),
i,
f2]
by Def13;
A10:
dom p = dom (p +* (i,(k + n)))
by FUNCT_7:32;
then (p +* (i,(k + n))) /. i =
(p +* (i,(k + n))) . i
by A1, PARTFUN1:def 8
.=
k + n
by A1, FUNCT_7:33
;
then A11:
not
p +* (
i,
k)
in dom (F . (k + n))
by A2, A4, A5, A6;
set pkn1 =
p +* (
i,
((k + n) + 1));
consider F1 being
Function of
NAT,
(HFuncs NAT) such that A12:
primrec (
f1,
f2,
i,
(p +* (i,((k + n) + 1))))
= F1 . ((p +* (i,((k + n) + 1))) /. i)
and A13:
(
i in dom (p +* (i,((k + n) + 1))) &
Del (
(p +* (i,((k + n) + 1))),
i)
in dom f1 implies
F1 . 0 = ((p +* (i,((k + n) + 1))) +* (i,0)) .--> (f1 . (Del ((p +* (i,((k + n) + 1))),i))) )
and A14:
( ( not
i in dom (p +* (i,((k + n) + 1))) or not
Del (
(p +* (i,((k + n) + 1))),
i)
in dom f1 ) implies
F1 . 0 = {} )
and A15:
for
M being
Element of
NAT holds
S1[
M,
F1 . M,
F1 . (M + 1),
p +* (
i,
((k + n) + 1)),
i,
f2]
by Def13;
dom p = dom (p +* (i,((k + n) + 1)))
by FUNCT_7:32;
then A16:
(p +* (i,((k + n) + 1))) /. i =
(p +* (i,((k + n) + 1))) . i
by A1, PARTFUN1:def 8
.=
(k + n) + 1
by A1, FUNCT_7:33
;
F1 = F
by A7, A8, A9, A13, A14, A15, Lm2;
then A17:
G . (p +* (i,(k + (n + 1)))) = F . ((k + n) + 1)
by A2, A12, A16;
per cases
( ( i in dom (p +* (i,(k + n))) & (p +* (i,(k + n))) +* (i,(k + n)) in dom (F . (k + n)) & ((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> in dom f2 ) or not i in dom (p +* (i,(k + n))) or not (p +* (i,(k + n))) +* (i,(k + n)) in dom (F . (k + n)) or not ((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> in dom f2 )
;
suppose
(
i in dom (p +* (i,(k + n))) &
(p +* (i,(k + n))) +* (
i,
(k + n))
in dom (F . (k + n)) &
((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*> in dom f2 )
;
not p +* (i,k) in dom (G . (p +* (i,(k + (n + 1)))))
then
F . ((k + n) + 1) = (F . (k + n)) +* (((p +* (i,(k + n))) +* (i,((k + n) + 1))) .--> (f2 . (((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*>)))
by A9;
then
dom (F . ((k + n) + 1)) = (dom (F . (k + n))) \/ (dom ({((p +* (i,(k + n))) +* (i,((k + n) + 1)))} --> (f2 . (((p +* (i,(k + n))) +* (i,(k + n))) ^ <*((F . (k + n)) . ((p +* (i,(k + n))) +* (i,(k + n))))*>))))
by FUNCT_4:def 1;
then A18:
dom (F . ((k + n) + 1)) = (dom (F . (k + n))) \/ {((p +* (i,(k + n))) +* (i,((k + n) + 1)))}
by FUNCOP_1:19;
k <= k + n
by NAT_1:11;
then A19:
k <> (k + n) + 1
by NAT_1:13;
A20:
(p +* (i,k)) . i = k
by A1, FUNCT_7:33;
((p +* (i,(k + n))) +* (i,((k + n) + 1))) . i = (k + n) + 1
by A1, A10, FUNCT_7:33;
then
not
p +* (
i,
k)
in {((p +* (i,(k + n))) +* (i,((k + n) + 1)))}
by A19, A20, TARSKI:def 1;
hence
not
p +* (
i,
k)
in dom (G . (p +* (i,(k + (n + 1)))))
by A11, A17, A18, XBOOLE_0:def 3;
verum
end;
end;
end;
A21:
S2[
0 ]
;
thus
for
n being
Element of
NAT holds
S2[
n]
from NAT_1:sch 1(A21, A3); verum
end;
end;
Lm6:
for i, m being Element of NAT
for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p holds
( ( p +* (i,0) in dom (primrec (f1,f2,i)) implies Del (p,i) in dom f1 ) & ( Del (p,i) in dom f1 implies p +* (i,0) in dom (primrec (f1,f2,i)) ) & ( p +* (i,0) in dom (primrec (f1,f2,i)) implies (primrec (f1,f2,i)) . (p +* (i,0)) = f1 . (Del (p,i)) ) & ( p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) implies ( p +* (i,m) in dom (primrec (f1,f2,i)) & (p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*> in dom f2 ) ) & ( p +* (i,m) in dom (primrec (f1,f2,i)) & (p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*> in dom f2 implies p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) ) & ( p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) implies (primrec (f1,f2,i)) . (p +* (i,(m + 1))) = f2 . ((p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*>) ) )
theorem
theorem
theorem Th64:
theorem
for
i,
m being
Element of
NAT for
f1,
f2 being non
empty NAT * -defined to-naturals homogeneous Function for
p being
Element of
((arity f1) + 1) -tuples_on NAT st
i in dom p holds
(
p +* (
i,
(m + 1))
in dom (primrec (f1,f2,i)) iff (
p +* (
i,
m)
in dom (primrec (f1,f2,i)) &
(p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*> in dom f2 ) )
by Lm6;
theorem
for
i,
m being
Element of
NAT for
f1,
f2 being non
empty NAT * -defined to-naturals homogeneous Function for
p being
Element of
((arity f1) + 1) -tuples_on NAT st
i in dom p &
p +* (
i,
(m + 1))
in dom (primrec (f1,f2,i)) holds
(primrec (f1,f2,i)) . (p +* (i,(m + 1))) = f2 . ((p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*>) by Lm6;
theorem Th67:
theorem Th68:
theorem
begin
:: deftheorem Def15 defines composition_closed COMPUT_1:def 15 :
for X being set holds
( X is composition_closed iff for f being Element of HFuncs NAT
for F being with_the_same_arity FinSequence of HFuncs NAT st f in X & arity f = len F & rng F c= X holds
f * <:F:> in X );
:: deftheorem Def16 defines primitive-recursion_closed COMPUT_1:def 16 :
for X being set holds
( X is primitive-recursion_closed iff for g, f1, f2 being Element of HFuncs NAT
for i being Element of NAT st g is_primitive-recursively_expressed_by f1,f2,i & f1 in X & f2 in X holds
g in X );
:: deftheorem Def17 defines primitive-recursively_closed COMPUT_1:def 17 :
for X being set holds
( X is primitive-recursively_closed iff ( 0 const 0 in X & 1 succ 1 in X & ( for n, i being Element of NAT st 1 <= i & i <= n holds
n proj i in X ) & X is composition_closed & X is primitive-recursion_closed ) );
theorem Th70:
Lm7:
for X being non empty set
for n, i being Element of NAT st 1 <= i & i <= n holds
for x being Element of X
for p being Element of n -tuples_on X holds p +* (i,x) in n -tuples_on X
;
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
:: deftheorem defines PrimRec COMPUT_1:def 18 :
PrimRec = meet { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ;
theorem Th78:
:: deftheorem Def19 defines primitive-recursive COMPUT_1:def 19 :
for x being set holds
( x is primitive-recursive iff x in PrimRec );
definition
func initial-funcs -> Subset of
(HFuncs NAT) equals
{(0 const 0),(1 succ 1)} \/ { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ;
coherence
{(0 const 0),(1 succ 1)} \/ { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } is Subset of (HFuncs NAT)
let Q be
Subset of
(HFuncs NAT);
func PR-closure Q -> Subset of
(HFuncs NAT) equals
Q \/ { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i ) } ;
coherence
Q \/ { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i ) } is Subset of (HFuncs NAT)
func composition-closure Q -> Subset of
(HFuncs NAT) equals
Q \/ { (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of (HFuncs NAT) * : ( f in Q & arity f = len F & rng F c= Q ) } ;
coherence
Q \/ { (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of (HFuncs NAT) * : ( f in Q & arity f = len F & rng F c= Q ) } is Subset of (HFuncs NAT)
end;
:: deftheorem defines initial-funcs COMPUT_1:def 20 :
initial-funcs = {(0 const 0),(1 succ 1)} \/ { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ;
:: deftheorem defines PR-closure COMPUT_1:def 21 :
for Q being Subset of (HFuncs NAT) holds PR-closure Q = Q \/ { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i ) } ;
:: deftheorem defines composition-closure COMPUT_1:def 22 :
for Q being Subset of (HFuncs NAT) holds composition-closure Q = Q \/ { (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of (HFuncs NAT) * : ( f in Q & arity f = len F & rng F c= Q ) } ;
:: deftheorem Def23 defines PrimRec-Approximation COMPUT_1:def 23 :
for b1 being Function of NAT,(bool (HFuncs NAT)) holds
( b1 = PrimRec-Approximation iff ( b1 . 0 = initial-funcs & ( for m being Nat holds b1 . (m + 1) = (PR-closure (b1 . m)) \/ (composition-closure (b1 . m)) ) ) );
theorem Th79:
theorem Th80:
theorem Th81:
theorem Th82:
begin
:: deftheorem Def24 defines nullary COMPUT_1:def 24 :
for f being homogeneous Relation holds
( f is nullary iff arity f = 0 );
:: deftheorem Def25 defines unary COMPUT_1:def 25 :
for f being homogeneous Relation holds
( f is unary iff arity f = 1 );
:: deftheorem Def26 defines binary COMPUT_1:def 26 :
for f being homogeneous Relation holds
( f is binary iff arity f = 2 );
:: deftheorem Def27 defines ternary COMPUT_1:def 27 :
for f being homogeneous Relation holds
( f is ternary iff arity f = 3 );
registration
let f be
primitive-recursive unary Function;
let g be
primitive-recursive ternary Function;
cluster primrec (
f,
g,1)
-> primitive-recursive binary ;
coherence
( primrec (f,g,1) is primitive-recursive & primrec (f,g,1) is binary )
cluster primrec (
f,
g,2)
-> primitive-recursive binary ;
coherence
( primrec (f,g,2) is primitive-recursive & primrec (f,g,2) is binary )
end;
theorem Th83:
theorem Th84:
theorem Th85:
theorem Th86:
Lm8:
now
reconsider z3 =
<*0,0,0*> as
FinSequence of
NAT ;
let g be non
empty homogeneous quasi_total PartFunc of
(NAT *),
NAT;
( arity g = 2 implies ( dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) & dom <:<*(3 proj 1),(3 proj 3)*>:> = 3 -tuples_on NAT & dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of (NAT *),NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) ) )set G =
g * <:<*(3 proj 1),(3 proj 3)*>:>;
A1:
rng (g * <:<*(3 proj 1),(3 proj 3)*>:>) c= NAT
by RELAT_1:def 19;
assume A2:
arity g = 2
;
( dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) & dom <:<*(3 proj 1),(3 proj 3)*>:> = 3 -tuples_on NAT & dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of (NAT *),NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) )then A3:
dom g = 2
-tuples_on NAT
by Th25;
thus A4:
dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3))
by FUNCT_6:62;
( dom <:<*(3 proj 1),(3 proj 3)*>:> = 3 -tuples_on NAT & dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of (NAT *),NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) )hence A5:
dom <:<*(3 proj 1),(3 proj 3)*>:> =
(3 -tuples_on NAT) /\ (dom (3 proj 3))
by Th40
.=
(3 -tuples_on NAT) /\ (3 -tuples_on NAT)
by Th40
.=
3
-tuples_on NAT
;
( dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3 -tuples_on NAT & ex G being homogeneous PartFunc of (NAT *),NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty ) )
now
set f =
<*(3 proj 1),(3 proj 3)*>;
let x be
set ;
( ( x in rng <:<*(3 proj 1),(3 proj 3)*>:> implies x in dom g ) & ( x in dom g implies x in rng <:<*(3 proj 1),(3 proj 3)*>:> ) )set F =
<:<*(3 proj 1),(3 proj 3)*>:>;
A6:
product (rngs <*(3 proj 1),(3 proj 3)*>) =
product <*(rng (3 proj 1)),(rng (3 proj 3))*>
by FUNCT_6:34
.=
product <*NAT,(rng (3 proj 3))*>
by Th40
.=
product <*NAT,NAT*>
by Th40
.=
2
-tuples_on NAT
by FUNCT_6:6
;
assume
x in dom g
;
x in rng <:<*(3 proj 1),(3 proj 3)*>:>then
x is
Element of 2
-tuples_on NAT
by A2, Th25;
then consider d1,
d2 being
Element of
NAT such that A8:
x = <*d1,d2*>
by FINSEQ_2:120;
reconsider x9 =
<*d1,0,d2*> as
Element of 3
-tuples_on NAT by FINSEQ_2:124;
<:<*(3 proj 1),(3 proj 3)*>:> . x9 =
<*((3 proj 1) . x9),((3 proj 3) . x9)*>
by A4, A5, FUNCT_6:62
.=
<*(x9 . 1),((3 proj 3) . x9)*>
by Th42
.=
<*(x9 . 1),(x9 . 3)*>
by Th42
.=
<*d1,(x9 . 3)*>
by FINSEQ_1:62
.=
x
by A8, FINSEQ_1:62
;
hence
x in rng <:<*(3 proj 1),(3 proj 3)*>:>
by A5, FUNCT_1:def 5;
verum
end;
then
rng <:<*(3 proj 1),(3 proj 3)*>:> = dom g
by TARSKI:2;
hence A9:
dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3
-tuples_on NAT
by A5, RELAT_1:46;
ex G being homogeneous PartFunc of (NAT *),NAT st
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty )then reconsider G =
g * <:<*(3 proj 1),(3 proj 3)*>:> as
PartFunc of
(NAT *),
NAT by A1, FINSEQ_2:162, RELSET_1:11;
reconsider G =
G as
homogeneous PartFunc of
(NAT *),
NAT by A9, MARGREL1:def 22;
take G =
G;
( G = g * <:<*(3 proj 1),(3 proj 3)*>:> & G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty )thus
G = g * <:<*(3 proj 1),(3 proj 3)*>:>
;
( G is Element of HFuncs NAT & arity G = 3 & G is quasi_total & not G is empty )
G is
Element of
PFuncs (
(NAT *),
NAT)
by PARTFUN1:119;
then
G in HFuncs NAT
;
hence
G is
Element of
HFuncs NAT
;
( arity G = 3 & G is quasi_total & not G is empty )
len z3 = 3
by FINSEQ_1:62;
then A10:
z3 is
Element of 3
-tuples_on NAT
by FINSEQ_2:110;
for
x being
FinSequence st
x in dom G holds
3
= len x
by A9, CARD_1:def 13;
hence
arity G = 3
by A10, A9, MARGREL1:def 26;
( G is quasi_total & not G is empty )hence
(
G is
quasi_total & not
G is
empty )
by A9, Th25;
verum
end;
:: deftheorem defines (1,2)->(1,?,2) COMPUT_1:def 28 :
for g being Function holds (1,2)->(1,?,2) g = g * <:<*(3 proj 1),(3 proj 3)*>:>;
registration
let g be
NAT * -defined to-naturals homogeneous len-total binary Function;
cluster (1,2)->(1,?,2) g -> non
empty len-total ternary ;
coherence
( not (1,2)->(1,?,2) g is empty & (1,2)->(1,?,2) g is ternary & (1,2)->(1,?,2) g is len-total )
end;
theorem Th87:
theorem Th88:
:: deftheorem defines [+] COMPUT_1:def 29 :
[+] = primrec ((1 proj 1),(3 succ 3),2);
theorem Th89:
definition
func [*] -> primitive-recursive binary Function equals
primrec (
(1 const 0),
((1,2)->(1,?,2) [+]),2);
coherence
primrec ((1 const 0),((1,2)->(1,?,2) [+]),2) is primitive-recursive binary Function
;
end;
:: deftheorem defines [*] COMPUT_1:def 30 :
[*] = primrec ((1 const 0),((1,2)->(1,?,2) [+]),2);
theorem Th90:
:: deftheorem defines [!] COMPUT_1:def 31 :
[!] = primrec ((0 const 1),([*] * <:<*((1 succ 1) * <:<*(2 proj 1)*>:>),(2 proj 2)*>:>),1);
theorem
definition
func [^] -> primitive-recursive binary Function equals
primrec (
(1 const 1),
((1,2)->(1,?,2) [*]),2);
coherence
primrec ((1 const 1),((1,2)->(1,?,2) [*]),2) is primitive-recursive binary Function
;
end;
:: deftheorem defines [^] COMPUT_1:def 32 :
[^] = primrec ((1 const 1),((1,2)->(1,?,2) [*]),2);
theorem
:: deftheorem defines [pred] COMPUT_1:def 33 :
[pred] = primrec ((0 const 0),(2 proj 1),1);
theorem Th93:
definition
func [-] -> primitive-recursive binary Function equals
primrec (
(1 proj 1),
((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)),2);
coherence
primrec ((1 proj 1),((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)),2) is primitive-recursive binary Function
;
end;
:: deftheorem defines [-] COMPUT_1:def 34 :
[-] = primrec ((1 proj 1),((1,2)->(1,?,2) ([pred] * <:<*(2 proj 2)*>:>)),2);
theorem