begin
theorem Th2:
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)
begin
begin
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 )
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 :
Def9:
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 Def9 defines
is_primitive-recursively_expressed_by COMPUT_1:def 9 :
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 :
Def10:
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 Def10 defines
primrec COMPUT_1:def 10 :
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 ) ) ) ) );
definition
let f1,
f2 be
NAT * -defined to-naturals homogeneous Function;
let i be
Element of
NAT ;
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;
Lm2:
now for f1, f2 being 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 = F
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:30;
A8:
(p +* (i,m)) +* (
i,
0) =
p +* (
i,
0)
by FUNCT_7:34
.=
(p +* (i,(m + 1))) +* (
i,
0)
by FUNCT_7:34
;
A9:
dom p = dom (p +* (i,(m + 1)))
by FUNCT_7:30;
A10:
Del (
(p +* (i,m)),
i) =
Del (
p,
i)
by Th3
.=
Del (
(p +* (i,(m + 1))),
i)
by Th3
;
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:34
.=
(p +* (i,(m + 1))) +* (
i,
(k + 1))
by FUNCT_7:34
;
A14:
(p +* (i,m)) +* (
i,
k) =
p +* (
i,
k)
by FUNCT_7:34
.=
(p +* (i,(m + 1))) +* (
i,
k)
by FUNCT_7:34
;
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:30;
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:12;
verum
end;
Lm3:
now for f1, f2 being 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 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:34;
A7:
(p +* (i,(m + 1))) . i = m + 1
by A1, FUNCT_7:31;
(p +* (i,m)) . i = m
by A1, FUNCT_7:31;
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:11;
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:13;
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:13;
then A20:
p +* (
i,
k) =
(p +* (i,(m + 1))) +* (
i,
0)
by A19, TARSKI:def 1
.=
p +* (
i,
0)
by FUNCT_7:34
;
k =
(p +* (i,k)) . i
by A1, FUNCT_7:31
.=
0
by A1, A20, FUNCT_7:31
;
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 for f1, f2 being 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 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 for n being Element of NAT st S2[n] holds
S2[n + 1]
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 Def10;
dom p = dom (p +* (i,((k + n) + 1)))
by FUNCT_7:30;
then A9:
(p +* (i,((k + n) + 1))) /. i =
(p +* (i,((k + n) + 1))) . i
by A1, PARTFUN1:def 6
.=
(k + n) + 1
by A1, FUNCT_7:31
;
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 Def10;
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:30;
then (p +* (i,(k + n))) /. i =
(p +* (i,(k + n))) . i
by A1, PARTFUN1:def 6
.=
k + n
by A1, FUNCT_7:31
;
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 for f1, f2 being 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 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 Def10;
A10:
dom p = dom (p +* (i,(k + n)))
by FUNCT_7:30;
then (p +* (i,(k + n))) /. i =
(p +* (i,(k + n))) . i
by A1, PARTFUN1:def 6
.=
k + n
by A1, FUNCT_7:31
;
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 Def10;
dom p = dom (p +* (i,((k + n) + 1)))
by FUNCT_7:30;
then A16:
(p +* (i,((k + n) + 1))) /. i =
(p +* (i,((k + n) + 1))) . i
by A1, PARTFUN1:def 6
.=
(k + n) + 1
by A1, FUNCT_7:31
;
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:13;
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:31;
((p +* (i,(k + n))) +* (i,((k + n) + 1))) . i = (k + n) + 1
by A1, A10, FUNCT_7:31;
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
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;
begin
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
;
begin
Lm8:
now for g being non empty homogeneous quasi_total PartFunc of (NAT *),NAT st arity g = 2 holds
( 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 ) )
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 Th22;
thus A4:
dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3))
by FINSEQ_3:142;
( 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 Th36
.=
(3 -tuples_on NAT) /\ (3 -tuples_on NAT)
by Th36
.=
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 for x being set holds
( ( 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)*>;
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 FINSEQ_3:133
.=
product <*NAT,(rng (3 proj 3))*>
by Th36
.=
product <*NAT,NAT*>
by Th36
.=
2
-tuples_on NAT
by FINSEQ_3:128
;
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, Th22;
then consider d1,
d2 being
Element of
NAT such that A8:
x = <*d1,d2*>
by FINSEQ_2:100;
reconsider x9 =
<*d1,0,d2*> as
Element of 3
-tuples_on NAT by FINSEQ_2:104;
<:<*(3 proj 1),(3 proj 3)*>:> . x9 =
<*((3 proj 1) . x9),((3 proj 3) . x9)*>
by A4, A5, FINSEQ_3:142
.=
<*(x9 . 1),((3 proj 3) . x9)*>
by Th38
.=
<*(x9 . 1),(x9 . 3)*>
by Th38
.=
<*d1,(x9 . 3)*>
by FINSEQ_1:45
.=
x
by A8, FINSEQ_1:45
;
hence
x in rng <:<*(3 proj 1),(3 proj 3)*>:>
by A5, FUNCT_1:def 3;
verum
end;
then
rng <:<*(3 proj 1),(3 proj 3)*>:> = dom g
by TARSKI:1;
hence A9:
dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) = 3
-tuples_on NAT
by A5, RELAT_1:27;
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:142, RELSET_1:4;
reconsider G =
G as
homogeneous PartFunc of
(NAT *),
NAT by A9, MARGREL1:def 21;
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:45;
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:45;
then A10:
z3 is
Element of 3
-tuples_on NAT
by FINSEQ_2:92;
for
x being
FinSequence st
x in dom G holds
3
= len x
by A9, CARD_1:def 7;
hence
arity G = 3
by A10, A9, MARGREL1:def 25;
( G is quasi_total & not G is empty )hence
(
G is
quasi_total & not
G is
empty )
by A9, Th22;
verum
end;