let i be Element of NAT ; 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; ( 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
; 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 ; ( 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 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))*>) ) ) ) )
; COMPUT_1:def 12 g = primrec f1,f2,i
A6:
now let p be
Element of
((arity f1) + 1) -tuples_on NAT ;
( ( 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[
Element of
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:40;
A8:
len p = (arity f1) + 1
by FINSEQ_1:def 18;
then A9:
i in dom p
by A1, A2, FINSEQ_3:27;
A10:
for
m being
Element of
NAT st
S2[
m] holds
S2[
m + 1]
proof
let m be
Element of
NAT ;
( 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) )
;
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;
( 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
;
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;
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
Element of
NAT holds
S2[
m]
from NAT_1:sch 1(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;
verum end;
A17:
dom (primrec f1,f2,i) c= ((arity f1) + 1) -tuples_on NAT
by Th60;
then A18:
dom g = dom (primrec f1,f2,i)
by A3, A4, A6, SUBSET_1:8;
then
for x being set 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, FUNCT_1:9; verum