proposition: Theorem Fma_FTS: (exists ga_e:float, exists al2_e:float, (FtoRradix ga_e=ga)%R /\ (FtoRradix al2_e=al2)%R /\ (Fbounded bo ga_e) /\ (Fbounded bo al2_e) /\ (Fexp al2_e <= Fexp ga_e)%Z).
proof: Proof. elim errorBoundedMult with bo radix p (Closest bo radix) a x u1; auto with zarith. 2:apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; intros u2' T; elim T; intros E1 T'; elim T'; intros E2 E3; clear T T'. elim errorBoundedPlus with bo radix p y u2' al1; auto with zarith. 2: fold FtoRradix; rewrite E1; rewrite <- u2Def; auto. rewrite E3; intros al2' T; elim T; intros F1 T'; elim T'; intros F2 F3; clear T T'. elim LeExpRound2 with (Z.min (Fexp y) (Fexp a+Fexp x)) (Fplus radix y u2') al1; auto. 2: unfold FtoRradix; rewrite Fplus_correct; auto; fold FtoRradix; rewrite E1; rewrite <- u2Def; auto. 2:simpl; rewrite E3; auto with zarith. intros al1' T; elim T; intros U1 T'; elim T'; intros U2 U3; clear T T'. elim LeExpRound2 with (Z.min (Fexp y) (Fexp a+Fexp x)) (Fmult a x) u1; auto with zarith. 2: unfold FtoRradix; rewrite Fmult_correct; auto. intros u1' T; elim T; intros U4 T'; elim T'; intros U5 U6; clear T T'. elim LeExpRound2 with (Z.min (Fexp y) (Fexp a+Fexp x)) (Fplus radix (Fmult a x) y) r1; auto with zarith. 2: unfold FtoRradix; rewrite Fplus_correct; auto; rewrite Fmult_correct; auto. 2: simpl; rewrite Z.min_comm; auto with zarith. intros r1' T; elim T; intros U7 T'; elim T'; intros U8 U9; clear T T'. elim LeExpRound2 with (Z.min (Fexp y) (Fexp a+Fexp x)) (Fplus radix u1' al1') be1; auto with zarith. 2: unfold FtoRradix; rewrite Fplus_correct; auto; fold FtoRradix; rewrite U5; rewrite U2; auto. 2: simpl; apply Zmin_Zle; auto with zarith. intros be1' T; elim T; intros V1 T'; elim T'; intros V2 V3; clear T T'. elim errorBoundedPlus with bo radix p u1' al1' be1; auto with zarith. 2: fold FtoRradix; rewrite U5; rewrite U2; auto. fold FtoRradix; intros be2' T; elim T; intros V4 T'; elim T'; intros V5 V6; clear T T'. elim LeExpRound2 with (Z.min (Fexp y) (Fexp a+Fexp x)) (Fminus radix be1' r1') gat; auto with zarith. 2: unfold FtoRradix; rewrite Fminus_correct; auto; fold FtoRradix; rewrite V2; rewrite U8; auto. 2: simpl; apply Zmin_Zle; auto with zarith. intros gat' T; elim T; intros V7 T'; elim T'; intros V8 V9; clear T T'. elim LeExpRound2 with (Z.min (Fexp y) (Fexp a+Fexp x)) (Fplus radix gat' be2') ga; auto with zarith. 2: unfold FtoRradix; rewrite Fplus_correct; auto; fold FtoRradix; rewrite V8; rewrite V4; rewrite U5; rewrite U2; rewrite <- be2Def; auto. 2: simpl; apply Zmin_Zle; lia. intros ga' T; elim T; intros W1 T'; elim T'; intros W2 W3; clear T T'. exists ga'; exists al2'; split; auto; split. unfold FtoRradix; rewrite F1; fold FtoRradix. rewrite E1; rewrite al2Def; rewrite u2Def; ring. split; auto; split; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz