let i be Nat; :: thesis: for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function st 1 <= i & i <= (arity f1) + 1 holds
for g being Element of HFuncs NAT st g is_primitive-recursively_expressed_by f1,f2,i holds
g = primrec (f1,f2,i)
let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; :: thesis: ( 1 <= i & i <= (arity f1) + 1 implies for g being Element of HFuncs NAT st g is_primitive-recursively_expressed_by f1,f2,i holds
g = primrec (f1,f2,i) )
assume that
A1: i >= 1 and
A2: i <= (arity f1) + 1 ; :: thesis: for g being Element of HFuncs NAT st g is_primitive-recursively_expressed_by f1,f2,i holds
g = primrec (f1,f2,i)
let g be Element of HFuncs NAT; :: thesis: ( g is_primitive-recursively_expressed_by f1,f2,i implies g = primrec (f1,f2,i) )
set n = (arity f1) + 1;
set h = primrec (f1,f2,i);
given n9 being Element of NAT such that A3: dom g c= n9 -tuples_on NAT and
i >= 1 and
i <= n9 and
A4: (arity f1) + 1 = n9 and
n9 + 1 = arity f2 and
A5: for p being FinSequence of NAT st len p = n9 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)))*>) ) ) ) ) ; :: according to COMPUT_1:def 9 :: thesis: g = primrec (f1,f2,i)
A6: now :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT holds
( ( p in dom g implies p in dom (primrec (f1,f2,i)) ) & ( p in dom (primrec (f1,f2,i)) implies p in dom g ) & ( p in dom g implies g . p = (primrec (f1,f2,i)) . p ) )
let p be Element of ((arity f1) + 1) -tuples_on NAT; :: thesis: ( ( p in dom g implies p in dom (primrec (f1,f2,i)) ) & ( p in dom (primrec (f1,f2,i)) implies p in dom g ) & ( p in dom g implies g . p = (primrec (f1,f2,i)) . p ) )
defpred S2[ Nat] means ( ( p +* (i,$1) in dom g implies p +* (i,$1) in dom (primrec (f1,f2,i)) ) & ( p +* (i,$1) in dom (primrec (f1,f2,i)) implies p +* (i,$1) in dom g ) & ( p +* (i,$1) in dom g implies g . (p +* (i,$1)) = (primrec (f1,f2,i)) . (p +* (i,$1)) ) );
set k = p /. i;
A7: p = p +* (i,(p /. i)) by FUNCT_7:38;
A8: len p = (arity f1) + 1 by CARD_1:def 7;
then A9: i in dom p by A1, A2, FINSEQ_3:25;
A10: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume that
A11: ( p +* (i,m) in dom g iff p +* (i,m) in dom (primrec (f1,f2,i)) ) and
A12: ( p +* (i,m) in dom g implies g . (p +* (i,m)) = (primrec (f1,f2,i)) . (p +* (i,m)) ) ; :: thesis: S2[m + 1]
( p +* (i,(m + 1)) in dom g iff ( p +* (i,m) in dom g & (p +* (i,m)) ^ <*(g . (p +* (i,m)))*> in dom f2 ) ) by A4, A5, A8;
hence ( p +* (i,(m + 1)) in dom g iff p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) ) by A9, A11, A12, Lm6; :: thesis: ( p +* (i,(m + 1)) in dom g implies g . (p +* (i,(m + 1))) = (primrec (f1,f2,i)) . (p +* (i,(m + 1))) )
A13: ( 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 A9, Lm6;
assume A14: p +* (i,(m + 1)) in dom g ; :: thesis: g . (p +* (i,(m + 1))) = (primrec (f1,f2,i)) . (p +* (i,(m + 1)))
then g . (p +* (i,(m + 1))) = f2 . ((p +* (i,m)) ^ <*(g . (p +* (i,m)))*>) by A4, A5, A8;
hence g . (p +* (i,(m + 1))) = (primrec (f1,f2,i)) . (p +* (i,(m + 1))) by A4, A5, A8, A9, A11, A12, A13, A14, Lm6; :: thesis: verum
end;
A15: ( p +* (i,0) in dom (primrec (f1,f2,i)) iff Del (p,i) in dom f1 ) by A9, Lm6;
then ( p +* (i,0) in dom g implies ( g . (p +* (i,0)) = f1 . (Del (p,i)) & (primrec (f1,f2,i)) . (p +* (i,0)) = f1 . (Del (p,i)) ) ) by A4, A5, A8, A9, Lm6;
then A16: S2[ 0 ] by A4, A5, A8, A15;
for m being Nat holds S2[m] from NAT_1:sch 2(A16, A10);
hence ( ( p in dom g implies p in dom (primrec (f1,f2,i)) ) & ( p in dom (primrec (f1,f2,i)) implies p in dom g ) & ( p in dom g implies g . p = (primrec (f1,f2,i)) . p ) ) by A7; :: thesis: verum
end;
A17: dom (primrec (f1,f2,i)) c= ((arity f1) + 1) -tuples_on NAT by Th55;
then A18: dom g = dom (primrec (f1,f2,i)) by A3, A4, A6;
for x being object st x in dom (primrec (f1,f2,i)) holds
g . x = (primrec (f1,f2,i)) . x by A17, A6;
hence g = primrec (f1,f2,i) by A18; :: thesis: verum