let g be Element of HFuncs NAT ; for f1, f2 being quasi_total Element of HFuncs NAT
for i being Element of NAT st g is_primitive-recursively_expressed_by f1,f2,i holds
( g is quasi_total & ( not f1 is empty implies not g is empty ) )
let f1, f2 be quasi_total Element of HFuncs NAT ; for i being Element of NAT st g is_primitive-recursively_expressed_by f1,f2,i holds
( g is quasi_total & ( not f1 is empty implies not g is empty ) )
let i be Element of NAT ; ( g is_primitive-recursively_expressed_by f1,f2,i implies ( g is quasi_total & ( not f1 is empty implies not g is empty ) ) )
assume A1:
g is_primitive-recursively_expressed_by f1,f2,i
; ( g is quasi_total & ( not f1 is empty implies not g is empty ) )
then consider n being Element of NAT such that
A2:
dom g c= n -tuples_on NAT
and
A3:
i >= 1
and
A4:
i <= n
and
A5:
(arity f1) + 1 = n
and
A6:
n + 1 = arity f2
and
A7:
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))*>) ) ) ) )
by Def12;
reconsider f29 = f2 as non empty quasi_total Element of HFuncs NAT by A6, Th21;
per cases
( f1 is empty or not f1 is empty )
;
suppose
not
f1 is
empty
;
( g is quasi_total & ( not f1 is empty implies not g is empty ) )then A8:
dom f1 = (arity f1) -tuples_on NAT
by Th25;
A9:
g is
quasi_total
proof
let x,
y be
FinSequence of
NAT ;
UNIALG_1:def 2 ( not len x = len y or not x in proj1 g or y in proj1 g )
assume that A10:
len x = len y
and A11:
x in dom g
;
y in proj1 g
defpred S2[
Element of
NAT ]
means y +* i,$1
in dom g;
A12:
len x = n
by A2, A11, FINSEQ_1:def 18;
A13:
now let k be
Element of
NAT ;
( S2[k] implies S2[k + 1] )assume A14:
S2[
k]
;
S2[k + 1]reconsider gyk =
g . (y +* i,k) as
Element of
NAT ;
reconsider gyik =
<*gyk*> as
FinSequence of
NAT ;
A15:
dom f29 = (arity f2) -tuples_on NAT
by Th25;
len ((y +* i,k) ^ <*(g . (y +* i,k))*>) =
(len (y +* i,k)) + (len <*(g . (y +* i,k))*>)
by FINSEQ_1:35
.=
n + (len <*(g . (y +* i,k))*>)
by A10, A12, FUNCT_7:99
.=
n + 1
by FINSEQ_1:56
;
then
(y +* i,k) ^ <*(g . (y +* i,k))*> is
Element of
dom f2
by A6, A15, FINSEQ_2:110;
then
(y +* i,k) ^ <*(g . (y +* i,k))*> in dom f29
;
hence
S2[
k + 1]
by A7, A10, A12, A14;
verum end;
y is
Element of
(len y) -tuples_on NAT
by FINSEQ_2:110;
then
Del y,
i in (arity f1) -tuples_on NAT
by A3, A4, A5, A10, A12, Th12;
then A16:
S2[
0 ]
by A7, A8, A10, A12;
for
k being
Element of
NAT holds
S2[
k]
from NAT_1:sch 1(A16, A13);
then A17:
y +* i,
(y /. i) in dom g
;
i in dom y
by A3, A4, A10, A12, FINSEQ_3:27;
then
y . i = y /. i
by PARTFUN1:def 8;
hence
y in dom g
by A17, FUNCT_7:37;
verum
end; consider pp being
set such that A18:
pp in n -tuples_on NAT
by XBOOLE_0:def 1;
pp is
Element of
n -tuples_on NAT
by A18;
then reconsider p =
pp as
FinSequence of
NAT ;
A19:
len p = n
by A18, FINSEQ_1:def 18;
Del p,
i in (arity f1) -tuples_on NAT
by A3, A4, A5, A18, Th12;
hence
(
g is
quasi_total & ( not
f1 is
empty implies not
g is
empty ) )
by A7, A19, A8, A9;
verum end;