let e1, e2 be NAT * -defined to-naturals homogeneous Function; :: thesis: for i being Nat
for p being FinSequence of NAT holds dom (primrec (e1,e2,i,p)) c= (1 + (arity e1)) -tuples_on NAT
let i be Nat; :: thesis: for p being FinSequence of NAT holds dom (primrec (e1,e2,i,p)) c= (1 + (arity e1)) -tuples_on NAT
set f1 = e1;
set f2 = e2;
let p be FinSequence of NAT ; :: thesis: dom (primrec (e1,e2,i,p)) c= (1 + (arity e1)) -tuples_on NAT
per cases ( i in dom p or not i in dom p ) ;
suppose A1: i in dom p ; :: thesis: dom (primrec (e1,e2,i,p)) c= (1 + (arity e1)) -tuples_on NAT
consider F being sequence of (HFuncs NAT) such that
A2: primrec (e1,e2,i,p) = F . (p /. i) and
A3: ( i in dom p & Del (p,i) in dom e1 implies F . 0 = (p +* (i,0)) .--> (e1 . (Del (p,i))) ) and
A4: ( ( not i in dom p or not Del (p,i) in dom e1 ) implies F . 0 = {} ) and
A5: for m being Nat holds S1[m,F . m,F . (m + 1),p,i,e2] by Def10;
defpred S2[ Nat] means dom (F . $1) c= (1 + (arity e1)) -tuples_on NAT;
A6: now :: thesis: for m being Nat st S2[m] holds
S2[m + 1]
let m be Nat; :: thesis: ( S2[m] implies S2[b1 + 1] )
assume A7: S2[m] ; :: thesis: S2[b1 + 1]
set pc = (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>;
per cases ( ( p +* (i,m) in dom (F . m) & (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom e2 ) or not p +* (i,m) in dom (F . m) or not (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom e2 ) ;
suppose A8: ( p +* (i,m) in dom (F . m) & (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom e2 ) ; :: thesis: S2[b1 + 1]
dom (p +* (i,m)) = dom p by FUNCT_7:30
.= dom (p +* (i,(m + 1))) by FUNCT_7:30 ;
then A9: len (p +* (i,m)) = len (p +* (i,(m + 1))) by FINSEQ_3:29;
len (p +* (i,m)) = 1 + (arity e1) by A7, A8, CARD_1:def 7;
then p +* (i,(m + 1)) is Element of (1 + (arity e1)) -tuples_on NAT by A9, FINSEQ_2:92;
then A10: {(p +* (i,(m + 1)))} c= (1 + (arity e1)) -tuples_on NAT by ZFMISC_1:31;
F . (m + 1) = (F . m) +* ((p +* (i,(m + 1))) .--> (e2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>))) by A1, A5, A8;
then dom (F . (m + 1)) = (dom (F . m)) \/ (dom ((p +* (i,(m + 1))) .--> (e2 . ((p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*>)))) by FUNCT_4:def 1;
then dom (F . (m + 1)) = (dom (F . m)) \/ {(p +* (i,(m + 1)))} ;
hence S2[m + 1] by A7, A10, XBOOLE_1:8; :: thesis: verum
end;
suppose ( not p +* (i,m) in dom (F . m) or not (p +* (i,m)) ^ <*((F . m) . (p +* (i,m)))*> in dom e2 ) ; :: thesis: S2[b1 + 1]
hence S2[m + 1] by A5, A7; :: thesis: verum
end;
end;
end;
A11: S2[ 0 ]
proof
per cases ( Del (p,i) in dom e1 or not Del (p,i) in dom e1 ) ;
suppose A12: Del (p,i) in dom e1 ; :: thesis: S2[ 0 ]
dom e1 c= (arity e1) -tuples_on NAT by Th20;
then A13: len (Del (p,i)) = arity e1 by A12, CARD_1:def 7;
A14: dom p = dom (p +* (i,0)) by FUNCT_7:30;
p <> <*> NAT by A1;
then consider n being Nat such that
A15: len p = n + 1 by NAT_1:6;
len (Del (p,i)) = n by A1, A15, FINSEQ_3:109;
then len (p +* (i,0)) = 1 + (arity e1) by A13, A15, A14, FINSEQ_3:29;
then A16: p +* (i,0) is Element of (1 + (arity e1)) -tuples_on NAT by FINSEQ_2:92;
dom (F . 0) = {(p +* (i,0))} by A1, A3, A12;
hence S2[ 0 ] by A16, ZFMISC_1:31; :: thesis: verum
end;
suppose not Del (p,i) in dom e1 ; :: thesis: S2[ 0 ]
hence S2[ 0 ] by A4, XBOOLE_1:2; :: thesis: verum
end;
end;
end;
for m being Nat holds S2[m] from NAT_1:sch 2(A11, A6);
hence dom (primrec (e1,e2,i,p)) c= (1 + (arity e1)) -tuples_on NAT by A2; :: thesis: verum
end;
suppose not i in dom p ; :: thesis: dom (primrec (e1,e2,i,p)) c= (1 + (arity e1)) -tuples_on NAT
then primrec (e1,e2,i,p) = {} by Th49;
hence dom (primrec (e1,e2,i,p)) c= (1 + (arity e1)) -tuples_on NAT ; :: thesis: verum
end;
end;