let i be Element of NAT ; :: thesis: for e1, e2 being NAT * -defined to-naturals homogeneous Function
for p, q being FinSequence of NAT st q in dom (primrec e1,e2,i,p) holds
ex k being Element of NAT st q = p +* i,k
let e1, e2 be NAT * -defined to-naturals homogeneous Function; :: thesis: for p, q being FinSequence of NAT st q in dom (primrec e1,e2,i,p) holds
ex k being Element of NAT st q = p +* i,k
set f1 = e1;
set f2 = e2;
let p, q be FinSequence of NAT ; :: thesis: ( q in dom (primrec e1,e2,i,p) implies ex k being Element of NAT st q = p +* i,k )
assume A1: q in dom (primrec e1,e2,i,p) ; :: thesis: ex k being Element of NAT st q = p +* i,k
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)) ) and
A4: ( ( not i in dom p or not Del p,i in dom e1 ) implies F . 0 = {} ) and
A5: 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 ( q in dom (F . $1) implies ex k being Element of NAT st q = p +* i,k );
A6: S2[ 0 ]
proof
assume A7: q in dom (F . 0 ) ; :: thesis: ex k being Element of NAT st q = p +* i,k
per cases ( ( i in dom p & Del p,i in dom e1 ) or not i in dom p or not Del p,i in dom e1 ) ;
suppose ( i in dom p & Del p,i in dom e1 ) ; :: thesis: ex k being Element of NAT st q = p +* i,k
then dom (F . 0 ) = {(p +* i,0 )} by A3, FUNCOP_1:19;
then p +* i,0 = q by A7, TARSKI:def 1;
hence ex k being Element of NAT st q = p +* i,k ; :: thesis: verum
end;
suppose ( not i in dom p or not Del p,i in dom e1 ) ; :: thesis: ex k being Element of NAT st q = p +* i,k
hence ex k being Element of NAT st q = p +* i,k by A4, A7; :: thesis: verum
end;
end;
end;
A8: 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
A9: S2[m] and
A10: q in dom (F . (m + 1)) ; :: thesis: ex k being Element of NAT st q = p +* i,k
per cases ( ( i in dom p & p +* i,m in dom (F . m) & (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom e2 ) or 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 ) ;
suppose ( i in dom p & p +* i,m in dom (F . m) & (p +* i,m) ^ <*((F . m) . (p +* i,m))*> in dom e2 ) ; :: thesis: ex k being Element of NAT st q = p +* i,k
then F . (m + 1) = (F . m) +* ((p +* i,(m + 1)) .--> (e2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>))) by A5;
then dom (F . (m + 1)) = (dom (F . m)) \/ (dom ((p +* i,(m + 1)) .--> (e2 . ((p +* i,m) ^ <*((F . m) . (p +* i,m))*>)))) by FUNCT_4:def 1;
then A11: dom (F . (m + 1)) = (dom (F . m)) \/ {(p +* i,(m + 1))} by FUNCOP_1:19;
thus ex k being Element of NAT st q = p +* i,k :: thesis: verum
proof
per cases ( q in dom (F . m) or q in {(p +* i,(m + 1))} ) by A10, A11, XBOOLE_0:def 3;
suppose q in dom (F . m) ; :: thesis: ex k being Element of NAT st q = p +* i,k
hence ex k being Element of NAT st q = p +* i,k by A9; :: thesis: verum
end;
suppose q in {(p +* i,(m + 1))} ; :: thesis: ex k being Element of NAT st q = p +* i,k
then q = p +* i,(m + 1) by TARSKI:def 1;
hence ex k being Element of NAT st q = p +* i,k ; :: thesis: verum
end;
end;
end;
end;
suppose ( 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 ) ; :: thesis: ex k being Element of NAT st q = p +* i,k
hence ex k being Element of NAT st q = p +* i,k by A5, A9, A10; :: thesis: verum
end;
end;
end;
for n being Element of NAT holds S2[n] from NAT_1:sch 1(A6, A8);
 hence ex k being Element of NAT st q = p +* i,k by A1, A2; :: thesis: verum