let g be Element of HFuncs NAT; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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 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)))*>) ) ) ) ) ;
reconsider f29 = f2 as non empty quasi_total Element of HFuncs NAT by A6, Th17;
per cases ( f1 is empty or not f1 is empty ) ;
suppose f1 is empty ; :: thesis: ( g is quasi_total & ( not f1 is empty implies not g is empty ) )
hence ( g is quasi_total & ( not f1 is empty implies not g is empty ) ) by A1, Th66; :: thesis: verum
end;
suppose not f1 is empty ; :: thesis: ( g is quasi_total & ( not f1 is empty implies not g is empty ) )
then A8: dom f1 = (arity f1) -tuples_on NAT by Th21;
A9: g is quasi_total
proof
let x, y be FinSequence of NAT ; :: according to MARGREL1:def 22 :: thesis: ( not len x = len y or not x in dom g or y in dom g )
assume that
A10: len x = len y and
A11: x in dom g ; :: thesis: y in dom g
defpred S2[ Nat] means y +* (i,$1) in dom g;
A12: len x = n by A2, A11, CARD_1:def 7;
A13: now :: thesis: for k being Nat st S2[k] holds
S2[k + 1]
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A14: S2[k] ; :: thesis: S2[k + 1]
A15: dom f29 = (arity f2) -tuples_on NAT by Th21;
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
len ((y +* (i,k)) ^ <*(g . (y +* (i,k)))*>) = (len (y +* (i,k))) + (len <*(g . (y +* (i,k)))*>) by FINSEQ_1:22
.= n + (len <*(g . (y +* (i,k)))*>) by A10, A12, FUNCT_7:97
.= n + 1 by FINSEQ_1:39 ;
then (y +* (i,kk)) ^ <*(g . (y +* (i,kk)))*> is Element of dom f2 by A6, A15, FINSEQ_2:92;
then (y +* (i,k)) ^ <*(g . (y +* (i,k)))*> in dom f29 ;
hence S2[k + 1] by A7, A10, A12, A14; :: thesis: verum
end;
y is Element of (len y) -tuples_on NAT by FINSEQ_2:92;
then Del (y,i) in (arity f1) -tuples_on NAT by A3, A4, A5, A10, A12, Th9;
then A16: S2[ 0 ] by A7, A8, A10, A12;
for k being Nat holds S2[k] from NAT_1:sch 2(A16, A13);
 then A17: y +* (i,(y /. i)) in dom g ;
i in dom y by A3, A4, A10, A12, FINSEQ_3:25;
then y . i = y /. i by PARTFUN1:def 6;
hence y in dom g by A17, FUNCT_7:35; :: thesis: verum
end;
consider pp being object 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, CARD_1:def 7;
Del (p,i) in (arity f1) -tuples_on NAT by A3, A4, A5, A18, Th9;
hence ( g is quasi_total & ( not f1 is empty implies not g is empty ) ) by A7, A19, A8, A9; :: thesis: verum
end;
end;