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 sequence of (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 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 Def10;
defpred S₂[ Nat] means F . $1 = {} ;
A4: for k being Nat st S₂[k] holds
S₂[k + 1] by A3, RELAT_1:38;
assume e1 is empty ; :: thesis: primrec (e1,e2,i,p) is empty
then A5: S₂[ 0 ] by A2;
for k being Nat holds S₂[k] from NAT_1:sch 2(A5, A4);
hence primrec (e1,e2,i,p) is empty by A1; :: thesis: verum