let i be Element of NAT ; :: thesis: for f1, f2 being non empty to-naturals homogeneous from-natural-fseqs Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) holds
p in dom (primrec f1,f2,i,p)
let f1, f2 be non empty to-naturals homogeneous from-natural-fseqs Function; :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT st f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) holds
p in dom (primrec f1,f2,i,p)
let p be Element of ((arity f1) + 1) -tuples_on NAT ; :: thesis: ( f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) implies p in dom (primrec f1,f2,i,p) )
assume that
A1:
f1 is len-total
and
A2:
f2 is len-total
and
A3:
(arity f1) + 2 = arity f2
and
A4:
( 1 <= i & i <= 1 + (arity f1) )
; :: thesis: p in dom (primrec f1,f2,i,p)
A5:
len p = 1 + (arity f1)
by FINSEQ_2:109;
then A6:
i in dom p
by A4, FINSEQ_3:27;
then A7:
p /. i = p . i
by PARTFUN1:def 8;
consider F being Function of NAT , HFuncs NAT such that
A8:
primrec f1,f2,i,p = F . (p /. i)
and
A9:
( i in dom p & Del p,i in dom f1 implies F . 0 = (p +* i,0 ) .--> (f1 . (Del p,i)) )
and
( ( not i in dom p or not Del p,i in dom f1 ) implies F . 0 = {} )
and
A10:
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 ) )
by Def13;
defpred S2[ Element of NAT ] means p +* i,$1 in dom (F . $1);
A11:
now A12:
len (Del p,i) = arity f1
by A5, A6, FINSEQ_3:118;
reconsider Dpi =
Del p,
i as
FinSequence of
NAT by FINSEQ_3:114;
reconsider Dpi' =
Dpi as
Element of
(len Dpi) -tuples_on NAT by FINSEQ_2:110;
dom f1 = (arity f1) -tuples_on NAT
by A1, Th26;
then
Dpi' in dom f1
by A12;
then
dom (F . 0 ) = {(p +* i,0 )}
by A4, A5, A9, FINSEQ_3:27, FUNCOP_1:19;
hence
S2[
0 ]
by TARSKI:def 1;
:: thesis: verum end;
A13:
now let m be
Element of
NAT ;
:: thesis: ( S2[m] implies S2[m + 1] )assume A14:
S2[
m]
;
:: thesis: S2[m + 1]set pc =
(p +* i,m) ^ <*((F . m) . (p +* i,m))*>;
A15:
dom f2 = (arity f2) -tuples_on NAT
by A2, Th26;
F . m is
Element of
HFuncs NAT
;
then A16:
rng (F . m) c= NAT
by RELSET_1:12;
(F . m) . (p +* i,m) in rng (F . m)
by A14, FUNCT_1:12;
then reconsider aa =
(F . m) . (p +* i,m) as
Element of
NAT by A16;
reconsider p2 =
<*aa*> as
FinSequence of
NAT ;
reconsider p1 =
(p +* i,m) ^ p2 as
FinSequence of
NAT ;
(
len (p +* i,m) = 1
+ (arity f1) &
len p2 = 1 )
by FINSEQ_2:109;
then len p1 =
((arity f1) + 1) + 1
by FINSEQ_1:35
.=
arity f2
by A3
;
then
p1 is
Element of
(arity f2) -tuples_on NAT
by FINSEQ_2:110;
then
F . (m + 1) = (F . m) +* ((p +* i,(m + 1)) .--> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>)))
by A6, A10, A14, A15;
then A17:
dom (F . (m + 1)) = (dom (F . m)) \/ (dom ({(p +* i,(m + 1))} --> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))))
by FUNCT_4:def 1;
p +* i,
(m + 1) in {(p +* i,(m + 1))}
by TARSKI:def 1;
then
p +* i,
(m + 1) in dom ({(p +* i,(m + 1))} --> (f2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>)))
by FUNCOP_1:19;
hence
S2[
m + 1]
by A17, XBOOLE_0:def 3;
:: thesis: verum end;
A18:
for m being Element of NAT holds S2[m]
from NAT_1:sch 1(A11, A13);
p +* i,(p . i) = p
by FUNCT_7:37;
hence
p in dom (primrec f1,f2,i,p)
by A7, A8, A18; :: thesis: verum