let e1, e2 be NAT * -defined to-naturals homogeneous Function; :: thesis: for i being Nat
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 i be Nat; :: 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 sequence of (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 Nat holds S₁[m,F . m,F . (m + 1),p,i,e2] by Def10;
defpred S₂[ Nat] means ( q in dom (F . $1) implies ex k being Element of NAT st q = p +* (i,k) );
A6: for m being Nat st S₂[m] holds
S₂[m + 1]

proof

let m be Nat; :: thesis: ( S₂[m] implies S₂[m + 1] )
assume that
A7: S₂[m] and
A8: 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 A9: dom (F . (m + 1)) = (dom (F . m)) \/ {(p +* (i,(m + 1)))} ;
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 A8, A9, 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 A7; :: 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, A7, A8; :: thesis: verum

end;

end;

end;

A10: S₂[ 0 ]

proof

assume A11: 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;
then p +* (i,0) = q by A11, 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, A11; :: thesis: verum

end;

end;

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A10, A6);
hence ex k being Element of NAT st q = p +* (i,k) by A1, A2; :: thesis: verum