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 )
assume A1: e1 is empty ; :: thesis: primrec e1,e2,i,p is empty
consider F being Function of NAT ,(HFuncs NAT ) such that
A2: primrec e1,e2,i,p = F . (p /. i) and
A3: ( ( i in dom p & Del p,i in dom e1 implies F . 0 = (p +* i,0 ) .--> (e1 . (Del p,i)) ) & ( ( 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
( ( 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 = {} ;
A5: S₂[ 0 ] by A1, A3;
A6: for k being Element of NAT st S₂[k] holds
S₂[k + 1] by A4, RELAT_1:60;
for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A5, A6);
hence primrec e1,e2,i,p is empty by A2; :: thesis: verum