let i be Element of NAT ; :: thesis: for e1, e2 being NAT * -defined to-naturals homogeneous Function
for p being FinSequence of NAT st not i in dom p holds
primrec e1,e2,i,p = {}
let e1, e2 be NAT * -defined to-naturals homogeneous Function; :: thesis: for p being FinSequence of NAT st not i in dom p holds
primrec e1,e2,i,p = {}
set f1 = e1;
set f2 = e2;
let p be FinSequence of NAT ; :: thesis: ( not i in dom p implies primrec e1,e2,i,p = {} )
assume A1:
not i in dom p
; :: thesis: primrec e1,e2,i,p = {}
consider F being Function of NAT ,(HFuncs NAT ) such that
A2:
primrec e1,e2,i,p = F . (p /. i)
and
( i in dom p & Del p,i in dom e1 implies F . 0 = (p +* i,0 ) .--> (e1 . (Del p,i)) )
and
A3:
( ( not i in dom p or not Del p,i in dom e1 ) implies F . 0 = {} )
and
A4:
for m being Element of NAT holds S1[m,F . m,F . (m + 1),p,i,e2]
by Def13;
defpred S2[ Element of NAT ] means F . $1 = {} ;
A5:
S2[ 0 ]
by A1, A3;
A6:
for m being Element of NAT st S2[m] holds
S2[m + 1]
by A1, A4;
for m being Element of NAT holds S2[m]
from NAT_1:sch 1(A5, A6);
hence
primrec e1,e2,i,p = {}
by A2; :: thesis: verum