proposition: Theorem VeltkampU: forall x p q hx tx:float, (Fcanonic radix b x) -> (Closest b radix (x*((powerRZ radix s)+1))%R p) -> (Closest b radix (x-p)%R q) -> (Closest b radix (q+p)%R hx) -> (Closest b radix (x-hx)%R tx) -> (Rabs (x-hx) <= (powerRZ radix (s+Fexp x)) /2)%R /\ (FtoRradix x=hx+tx)%R /\ (exists hx':float, (FtoRradix hx'=hx)%R /\ (Fbounded b' hx') /\ ((Fnormal radix b x) -> (s+Fexp x <= Fexp hx')%Z)) /\ (exists tx':float, (FtoRradix tx'=tx)%R /\ (Fbounded bt tx') /\ (Fexp x <= Fexp tx')%Z).
proof: Proof. intros. generalize Veltkamp; intros T. elim T with radix b s t x p q hx; auto. 2: apply FcanonicBound with radix; auto. clear T; intros H4 T; elim T; intros hx' T'; elim T'; intros H5 T''; clear T T'. elim T''; intros H6 H7; clear T''. generalize Veltkamp_tail; intros T. elim T with radix b s t x p q hx tx; auto. 2: apply FcanonicBound with radix; auto. clear T; intros tx' T'; elim T'; intros H8 T''; clear T'. elim T''; intros H9 T; elim T; intros H10 H11; clear T T''. split; auto. split; auto with real. unfold FtoRradix; rewrite <- H9; rewrite H8; auto with real. split. exists hx'; split; auto. split; auto. elim H6; auto with zarith. exists tx'. split; auto. split; auto. rewrite <- FcanonicFnormalizeEq with radix b t x; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz