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: 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
A7: S2[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)))} by FUNCOP_1:13;
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: S2[ 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, FUNCOP_1:13;
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 Element of NAT holds S2[n] from NAT_1:sch 1(A10, A6);
 hence ex k being Element of NAT st q = p +* (i,k) by A1, A2; :: thesis: verum