let i be Element of NAT ; :: thesis: for e1, e2 being NAT * -defined to-naturals homogeneous Function
for p being FinSequence of NAT st e1 is empty holds
primrec e1,e2,i,p is empty
let e1, e2 be NAT * -defined to-naturals homogeneous Function; :: thesis: for p being FinSequence of NAT st e1 is empty holds
primrec e1,e2,i,p is empty
set f1 = e1;
set f2 = e2;
let p be FinSequence of NAT ; :: thesis: ( e1 is empty implies primrec e1,e2,i,p is empty )
consider F being Function of NAT ,(HFuncs NAT ) such that
A1: 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
A2: ( ( not i in dom p or not Del p,i in dom e1 ) implies F . 0 = {} ) and
A3: for m being Element of NAT holds
( ( i in dom p & p +* i,m in dom (F . m) & (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom e2 implies F . (m + 1) = (F . m) +* ((p +* i,(m + 1)) .--> (e2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))) ) & ( ( not i in dom p or not p +* i,m in dom (F . m) or not (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom e2 ) implies F . (m + 1) = F . m ) ) by Def13;
defpred S₂[ Element of NAT ] means F . $1 = {} ;
A4: for k being Element of NAT st S₂[k] holds
S₂[k + 1] by A3, RELAT_1:60;
assume e1 is empty ; :: thesis: primrec e1,e2,i,p is empty
then A5: S₂[ 0 ] by A2;
for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A5, A4);
hence primrec e1,e2,i,p is empty by A1; :: thesis: verum