let i be Element of NAT ; :: thesis: for f1, f2 being non empty to-naturals homogeneous from-natural-fseqs 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 to-naturals homogeneous from-natural-fseqs 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 A1:
( i >= 1 & 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
set n = (arity f1) + 1;
set h = 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 )
given n' being Element of NAT such that A2:
( dom g c= n' -tuples_on NAT & i >= 1 & i <= n' )
and
A3:
( (arity f1) + 1 = n' & n' + 1 = arity f2 )
and
A4:
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 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))*>) ) ) ) )
; :: according to COMPUT_1:def 12 :: thesis: g = primrec f1,f2,i
A5:
dom (primrec f1,f2,i) c= ((arity f1) + 1) -tuples_on NAT
by Th60;
A6:
now 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[
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) ) );
A7:
len p = (arity f1) + 1
by FINSEQ_2:109;
then A8:
i in dom p
by A1, FINSEQ_3:27;
then A9:
( (
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 (primrec f1,f2,i) implies
Del p,
i in dom f1 ) & (
Del p,
i in dom f1 implies
p +* i,
0 in dom (primrec f1,f2,i) ) )
by A3, A4, A7, 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 A3, A4, A7, A8, Lm6;
then A10:
S2[
0 ]
by A9;
set k =
p /. i;
A11:
p = p +* i,
(p /. i)
by FUNCT_7:40;
A12:
for
m being
Element of
NAT st
S2[
m] holds
S2[
m + 1]
proof
let m be
Element of
NAT ;
:: thesis: ( S2[m] implies S2[m + 1] )
assume that A13:
(
p +* i,
m in dom g iff
p +* i,
m in dom (primrec f1,f2,i) )
and A14:
(
p +* i,
m in dom g implies
g . (p +* i,m) = (primrec f1,f2,i) . (p +* i,m) )
;
:: thesis: S2[m + 1]
A15:
(
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 A3, A4, A7;
A16:
(
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 A8, Lm6;
thus
(
p +* i,
(m + 1) in dom g iff
p +* i,
(m + 1) in dom (primrec f1,f2,i) )
by A8, A13, A14, A15, Lm6;
:: thesis: ( p +* i,(m + 1) in dom g implies g . (p +* i,(m + 1)) = (primrec f1,f2,i) . (p +* i,(m + 1)) )
assume A17:
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))*>) &
g . (p +* i,m) = (primrec f1,f2,i) . (p +* i,m) )
by A3, A4, A7, A14;
hence
g . (p +* i,(m + 1)) = (primrec f1,f2,i) . (p +* i,(m + 1))
by A3, A4, A7, A8, A13, A16, A17, Lm6;
:: thesis: verum
end;
for
m being
Element of
NAT holds
S2[
m]
from NAT_1:sch 1(A10, A12);
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 A11;
:: thesis: verum end;
then A18:
dom g = dom (primrec f1,f2,i)
by A2, A3, A5, 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 A5, A6;
hence
g = primrec f1,f2,i
by A18, FUNCT_1:9; :: thesis: verum