begin
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem
canceled;
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
begin
:: deftheorem Def1 defines compatible COMPUT_1:def 1 :
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 :
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 , 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 :
:: deftheorem Def7 defines arity COMPUT_1:def 7 :
theorem
:: deftheorem defines HFuncs COMPUT_1:def 8 :
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
:: deftheorem defines const COMPUT_1:def 9 :
theorem Th34:
theorem Th35:
:: deftheorem Def10 defines succ COMPUT_1:def 10 :
theorem
canceled;
theorem Th37:
theorem Th38:
:: deftheorem defines proj COMPUT_1:def 11 :
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 :
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 :
:: deftheorem Def16 defines primitive-recursion_closed COMPUT_1:def 16 :
:: deftheorem Def17 defines primitive-recursively_closed COMPUT_1:def 17 :
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 :
theorem Th78:
:: deftheorem Def19 defines primitive-recursive COMPUT_1:def 19 :
definition
func initial-funcs -> Subset of
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
let Q be
Subset of ;
func PR-closure Q -> Subset of
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
func composition-closure Q -> Subset of
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
end;
:: deftheorem defines initial-funcs COMPUT_1:def 20 :
:: deftheorem defines PR-closure COMPUT_1:def 21 :
:: deftheorem defines composition-closure COMPUT_1:def 22 :
:: deftheorem Def23 defines PrimRec-Approximation COMPUT_1:def 23 :
theorem Th79:
theorem Th80:
theorem Th81:
theorem Th82:
begin
:: deftheorem Def24 defines nullary COMPUT_1:def 24 :
:: deftheorem Def25 defines unary COMPUT_1:def 25 :
:: deftheorem Def26 defines binary COMPUT_1:def 26 :
:: deftheorem Def27 defines ternary COMPUT_1:def 27 :
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 ,;
( 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 , 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 B2:
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 , 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 A2:
dom g = 2
-tuples_on NAT
by Th25;
thus A3:
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 , 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 A4:
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 , 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)*>:>;
A5:
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 B2, Th25;
then consider d1,
d2 being
Element of
NAT such that A7:
x = <*d1,d2*>
by FINSEQ_2:120;
reconsider x' =
<*d1,0 ,d2*> as
Element of 3
-tuples_on NAT by FINSEQ_2:124;
<:<*(3 proj 1),(3 proj 3)*>:> . x' =
<*((3 proj 1) . x'),((3 proj 3) . x')*>
by A3, A4, FUNCT_6:62
.=
<*(x' . 1),((3 proj 3) . x')*>
by Th42
.=
<*(x' . 1),(x' . 3)*>
by Th42
.=
<*d1,(x' . 3)*>
by FINSEQ_1:62
.=
x
by A7, FINSEQ_1:62
;
hence
x in rng <:<*(3 proj 1),(3 proj 3)*>:>
by A4, FUNCT_1:def 5;
verum
end;
then
rng <:<*(3 proj 1),(3 proj 3)*>:> = dom g
by TARSKI:2;
hence A8:
dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3
-tuples_on NAT
by A4, RELAT_1:46;
ex G being homogeneous PartFunc of , 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 ,
by A1, FINSEQ_2:162, RELSET_1:11;
reconsider G =
G as
homogeneous PartFunc of ,
by A8, UNIALG_1:def 1;
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 A11:
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 A8, FINSEQ_1:def 18;
hence
arity G = 3
by A11, A8, UNIALG_1:def 10;
( G is quasi_total & not G is empty )hence
(
G is
quasi_total & not
G is
empty )
by A8, Th25;
verum
end;
:: deftheorem defines (1,2)->(1,?,2) COMPUT_1:def 28 :
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 :
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 :
theorem Th90:
:: deftheorem defines [!] COMPUT_1:def 31 :
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 :
theorem
:: deftheorem defines [pred] COMPUT_1:def 33 :
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 :
theorem