diff --git a/coq/AffineValidation.v b/coq/AffineValidation.v
index 7ce165b20643f3b43faf4f05e9bc29e7e510360f..63bf355afb99777cdbcf6925acce5f5293acbfc1 100644
--- a/coq/AffineValidation.v
+++ b/coq/AffineValidation.v
@@ -3,7 +3,7 @@ Require Import Recdef.
 Require Import Flover.AffineForm Flover.AffineArithQ Flover.AffineArith.
 Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
 Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.Typing Flover.ssaPrgs.
-Require Import Flover.IntervalValidation.
+Require Import Flover.IntervalValidation Flover.RealRangeArith.
 
 Lemma usedVars_eq_compat e1 e2:
   Q_orderedExps.eq e1 e2 ->
@@ -113,7 +113,7 @@ Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) (P: precond) (validVa
       olet valid := validAffineBounds e' A P validVars exprsAf currentMaxNoise in
       let (exprsAf', n') := valid in
       olet af := FloverMap.find e' exprsAf' in
-      match o with 
+      match o with
       | Neg =>
         updateExpMap e (AffineArithQ.negate_aff af) n' exprsAf' intv
       | Inv =>
@@ -155,7 +155,7 @@ Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) (P: precond) (validVa
       let (exprsAf3, n3) := valid3 in
       olet af3 := FloverMap.find e3 exprsAf3 in
         updateExpMapSucc e (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 n3)) n3 exprsAf3 intv
-    | Downcast _ e' => 
+    | Downcast _ e' =>
       olet valid' := validAffineBounds e' A P validVars exprsAf currentMaxNoise in
       let (exprsAf', n') := valid' in
       olet asubres := FloverMap.find e' A in
@@ -485,7 +485,7 @@ Qed.
 Lemma afQ2R_fresh n a:
   fresh n a <-> fresh n (afQ2R a).
 Proof.
-  split; induction a; intros *. 
+  split; induction a; intros *.
   all: try (unfold fresh, get_max_index; rewrite get_max_index_aux_equation; now simpl).
   all: intros A.
   all: remember A as A' eqn:tmp; clear tmp.
@@ -562,7 +562,7 @@ Definition affine_fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
     NatSet.In v fVars ->
     exists vR, E v = Some vR /\
           (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R.
-          
+
 Definition affine_vars_typed (S: NatSet.t) (Gamma: nat -> option mType) :=
   forall v, NatSet.In v S ->
        exists m: mType, Gamma v = Some m.
@@ -619,7 +619,7 @@ Proof.
 Qed.
 
 Lemma validAffineBounds_sound (e: expr Q) (A: analysisResult) (P: precond)
-      fVars dVars (E: env) Gamma exprAfs noise iexpmap inoise map1: 
+      fVars dVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
   (forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
         checked_expressions A E Gamma fVars dVars e iexpmap inoise map1) ->
   (inoise > 0)%nat ->
@@ -1851,7 +1851,7 @@ Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (valid
   end.
 
 Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
-      fVars dVars outVars (E: env) Gamma exprAfs noise iexpmap inoise map1: 
+      fVars dVars outVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
   (forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
         checked_expressions A E Gamma fVars dVars e iexpmap inoise map1) ->
   (inoise > 0)%nat ->
@@ -2104,7 +2104,7 @@ Proof.
     exists ihmap, ihaf, ihvR, ihaiv, ihaerr.
     repeat split; try auto.
     + econstructor; try eauto.
-      eapply IntervalValidation.swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n REAL Gamma)) ; try eauto.
+      eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n REAL Gamma)) ; try eauto.
       intros n1; erewrite Rmap_updVars_comm; eauto.
     + intros e' Hnone Hsome.
       specialize (ihchecked e').
diff --git a/coq/CertificateChecker.v b/coq/CertificateChecker.v
index cd75d0adf8fb78637da1652408243a386e4fe6c9..e2dcbfb04a14456b3731fb4732600fdf301572e1 100644
--- a/coq/CertificateChecker.v
+++ b/coq/CertificateChecker.v
@@ -4,12 +4,12 @@
    Running this function on the encoded analysis result gives the desired theorem
    as shown in the soundness theorem.
 **)
-Require Import Coq.Reals.Reals Coq.QArith.Qreals.
-Require Import Flover.Infra.RealSimps Flover.Infra.RationalSimps Flover.Infra.RealRationalProps Flover.Infra.Ltacs.
-Require Import Flover.RealRangeValidator Flover.RoundoffErrorValidator Flover.Environments Flover.Typing Flover.FPRangeValidator.
+From Flover
+     Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
+     Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
+     Environments Typing FPRangeValidator ExpressionAbbrevs Commands.
 
-Require Export Coq.QArith.QArith.
-Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
+Require Export Infra.ExpressionAbbrevs Flover.Commands.
 
 (** Certificate checking function **)
 Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
@@ -68,10 +68,13 @@ Proof.
   { unfold vars_typed. intros; apply types_defined. set_tac. destruct H1; set_tac.
     split; try auto. hnf; intros; set_tac. }
   rename R into validFPRanges.
-  edestruct (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=defVars) (E:=E1))
-    as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]]; eauto.
+  assert (validRanges e absenv E1 defVars) as valid_e.
+  { eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=defVars) (E:=E1));
+      auto. }
+  pose proof (validRanges_single _ _ _ _ valid_e) as valid_single;
+    destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
   destruct iv_e as [elo ehi].
-  edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType)) L approxE1E2 H0 eval_real R0 L1 H P_valid H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
+  edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType)) L approxE1E2 H0 eval_real R0 valid_e H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
   exists (elo, ehi), err_e, vR, vF, mF; split; auto.
 Qed.
 
@@ -81,7 +84,7 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) d
   then
     if (RangeValidatorCmd f absenv P NatSet.empty) &&
        FPRangeValidatorCmd f absenv tMap NatSet.empty
-    then (validErrorboundCmd f tMap absenv NatSet.empty)
+    then (RoundoffErrorValidatorCmd f tMap absenv NatSet.empty)
     else false
   else false.
 
@@ -126,12 +129,13 @@ Proof.
     destruct H0; set_tac. }
   assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
     as freeVars_contained by set_tac.
-  edestruct (validIntervalboundsCmd_sound)
-    as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]]; eauto.
+  assert (validRangesCmd f absenv E1 defVars) as valid_f.
+  { eapply RangeValidatorCmd_sound; eauto.
+    unfold affine_dVars_range_valid; intros.
+    set_tac. }
+  pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
+  destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
   destruct iv as [f_lo f_hi].
-  edestruct validErrorboundCmd_gives_eval as [vF [mF eval_float]]; eauto.
+  edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto.
   exists (f_lo, f_hi), err, vR, vF, mF; split; try auto.
-  split; try auto; split; try auto.
-  intros.
-  eapply validErrorboundCmd_sound; eauto.
 Qed.
diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v
index 58292325a82507d2c10936507fcb02321b02112b..d86cf33b849a1bac1964be4c2025164e115173ff 100644
--- a/coq/ErrorValidation.v
+++ b/coq/ErrorValidation.v
@@ -2181,7 +2181,7 @@ Theorem validErrorboundCmd_gives_eval (f:cmd Q) :
     NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
     bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
     validErrorboundCmd f Gamma A dVars = true ->
-    validRangesCmd f A E1 (toRMap defVars) ->
+    validRangesCmd f A E1 defVars ->
     vars_typed (NatSet.union fVars dVars) defVars ->
     FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
     (exists vF m,
@@ -2241,32 +2241,12 @@ Proof.
         split; try auto. }
       { eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRMap defVars));
           eauto using Rmap_updVars_comm. }
-      { eapply valid_cont.
-      { intros v1 v1_mem.
-        unfold updEnv.
-        case_eq (v1 =? n); intros v1_eq.
-        - apply Nat.eqb_eq in v1_eq; subst.
-          exists v, (q1, q2), e1; split; try auto; split; try auto; simpl.
-          destruct (validIntervalbounds_sound e (E:=E1) (Gamma:=defVars) L (fVars:=fVars))
-            as [iv_e' [ err_e' [vR_e [map_e [eval_real_e bounded_real_e]]]]];
-            eauto.
-          rewrite map_e in *; inversion Heqo; subst.
-          pose proof (meps_0_deterministic _ eval_real_e H7); subst.
-          simpl in *. inversion Heqo0; subst; lra.
-        - rewrite Nat.eqb_neq in v1_eq; set_tac.
-          destruct v1_mem; subst; try congruence.
-          apply fVars_sound ; try auto.
-          destruct H0; auto. }
-        { intros v1 mem_fVars.
-          specialize (P_valid v1 mem_fVars).
-          unfold updEnv.
-          case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try auto.
-          rewrite Nat.eqb_eq in case_v1; subst.
-          assert (NatSet.In n (NatSet.union fVars dVars))
-            as in_union
-              by (rewrite NatSet.union_spec; auto).
-          rewrite <- NatSet.mem_spec in in_union.
-          rewrite in_union in *; congruence. }
+      { apply validRangesCmd_swap with (Gamma1 := updDefVars n REAL defVars).
+        - intros x.
+          unfold toRMap, updDefVars.
+          destruct (x =? n) eqn:?; auto.
+        - apply valid_cont.
+          apply swap_Gamma_eval_expr with (Gamma1 := toRMap defVars); try auto. }
         { intros v1 v1_mem; set_tac.
           unfold updDefVars.
           case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try eauto.
@@ -2277,16 +2257,17 @@ Proof.
           rewrite Nat.eqb_neq in case_v1; congruence. }
         { exists vF_res; exists m_res; try auto.
           econstructor; eauto. }
+    + destruct valid_intv as [[? ?] ?]; auto.
   - inversion eval_real; subst.
     unfold updEnv; simpl.
     unfold validErrorboundCmd in valid_bounds.
-    simpl in *.
+    destruct valid_intv.
     edestruct validErrorbound_sound as [[vF [mF eval_e]] bounded_e]; eauto.
     exists vF; exists mF; econstructor; eauto.
 Qed.
 
 Theorem validErrorboundCmd_sound (f:cmd Q):
-  forall A E1 E2 outVars fVars dVars vR vF mF elo ehi err P Gamma defVars,
+  forall A E1 E2 outVars fVars dVars vR vF mF elo ehi err Gamma defVars,
     typeCheckCmd f defVars Gamma = true ->
     approxEnv E1 defVars A fVars dVars E2 ->
     ssa f (NatSet.union fVars dVars) outVars ->
@@ -2294,16 +2275,14 @@ Theorem validErrorboundCmd_sound (f:cmd Q):
     bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
     bstep (toRCmd f) E2 defVars vF mF ->
     validErrorboundCmd f Gamma A dVars = true ->
-    validIntervalboundsCmd f A P dVars = true ->
-    dVars_range_valid dVars E1 A ->
-    fVars_P_sound fVars E1 P ->
+    validRangesCmd f A E1 defVars ->
     vars_typed (NatSet.union fVars dVars) defVars ->
     FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
     (Rabs (vR - vF) <= (Q2R err))%R.
 Proof.
   induction f;
     intros * type_f approxc1c2 ssa_f freeVars_subset eval_real eval_float
-                    valid_bounds valid_intv fVars_sound P_valid types_defined A_res;
+                    valid_bounds valid_intv types_defined A_res;
     cbn in *; Flover_compute; try congruence; type_conv; subst.
   - inversion eval_real;
       inversion eval_float;
@@ -2317,25 +2296,20 @@ Proof.
     match goal with
       | [H : validErrorbound _ _ _ _ = true |- _] =>
         eapply validErrorbound_sound
-          with (err := e2) (elo := fst(i)) (ehi:= snd(i)) in H; edestruct i; eauto;
+          with (err := e0) (elo := fst(i)) (ehi:= snd(i)) in H; edestruct i; eauto;
           destruct H as [[vFe [mFe eval_float_e]] bounded_e]
     end.
     canonize_hyps.
     rename R into valid_rec.
-    rewrite (typingSoundnessExp _ _  L0 eval_float_e) in *;
+    rewrite (typingSoundnessExp _ _  L eval_float_e) in *;
       simpl in *.
-    (* destruct (Gamma (Var Q n)); try congruence. *)
-    (* match goal with *)
-    (* | [ H: _ && _ = true |- _] => andb_to_prop H *)
-    (* end. *)
-    (* type_conv. *)
     apply (IHf A (updEnv n v E1) (updEnv n v0 E2) outVars fVars
-               (NatSet.add n dVars) vR vF mF elo ehi err P Gamma
+               (NatSet.add n dVars) vR vF mF elo ehi err Gamma
                (updDefVars n m1 defVars));
       eauto.
     + eapply approxUpdBound; try eauto.
       simpl in *.
-      apply Rle_trans with (r2:= Q2R e2); try lra.
+      apply Rle_trans with (r2:= Q2R e0); try lra.
       eapply bounded_e; eauto.
     + eapply ssa_equal_set; eauto.
       hnf. intros a; split; intros in_set.
@@ -2354,34 +2328,13 @@ Proof.
       split; try auto.
     + eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRMap defVars));
         eauto using Rmap_updVars_comm.
-    + intros v1 v1_mem.
-      unfold updEnv.
-      case_eq (v1 =? n); intros v1_eq.
-      * apply Nat.eqb_eq in v1_eq; subst.
-        exists v, (q1,q2), e1; split; try auto; split; try auto.
-        simpl. rewrite <- R1, <- R0.
-        destruct (validIntervalbounds_sound e L (E:=E1) (Gamma:=defVars) (fVars:=fVars))
-          as [iv_e [ err_e [ vR_e [ map_e [eval_real_e bounded_real_e]]]]];
-          eauto.
-        repeat destr_factorize.
-        pose proof (meps_0_deterministic _ eval_real_e H7); subst.
-        inversion Heqo0; subst.
-        simpl in *; auto.
-      * rewrite Nat.eqb_neq in v1_eq.
-        set_tac.
-        destruct v1_mem as [? | [? ?]].
-        { exfalso; apply v1_eq; auto. }
-        { apply fVars_sound ; auto. }
-    + intros v1 mem_fVars.
-      specialize (P_valid v1 mem_fVars).
-      unfold updEnv.
-      case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try auto.
-      rewrite Nat.eqb_eq in case_v1; subst.
-      assert (NatSet.In n (NatSet.union fVars dVars))
-        as in_union
-          by (rewrite NatSet.union_spec; auto).
-      rewrite <- NatSet.mem_spec in in_union.
-      rewrite in_union in *; congruence.
+    + apply validRangesCmd_swap with (Gamma1 := updDefVars n REAL defVars).
+      * intros x.
+        unfold toRMap, updDefVars.
+        destruct (x =? n) eqn:?; auto.
+      * destruct valid_intv as [[? valid_cont] ?].
+        apply valid_cont.
+        apply swap_Gamma_eval_expr with (Gamma1 := toRMap defVars); try auto.
     + intros v1 v1_mem; set_tac.
       unfold updDefVars.
       case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try eauto.
@@ -2390,10 +2343,11 @@ Proof.
       destruct v1_mem as [v_fVar | v_dVar]; try auto.
       rewrite NatSet.add_spec in v_dVar. destruct v_dVar; try auto.
       subst; rewrite Nat.eqb_refl in case_v1; congruence.
+    + destruct valid_intv as [[? ?] ?]; auto.
   - inversion eval_real; subst.
     inversion eval_float; subst.
     unfold updEnv; simpl.
     unfold validErrorboundCmd in valid_bounds.
-    simpl in *.
+    destruct valid_intv as [? ?].
     edestruct validErrorbound_sound as [[* [* eval_e]] bounded_e]; eauto.
 Qed.
diff --git a/coq/FPRangeValidator.v b/coq/FPRangeValidator.v
index 1fa73b0dece414525cb90fac168050cbf4089f1c..9db3a1e9ba5131e3d859328f12c72c38c32df00f 100644
--- a/coq/FPRangeValidator.v
+++ b/coq/FPRangeValidator.v
@@ -55,7 +55,7 @@ Fixpoint FPRangeValidatorCmd (f:cmd Q) (A:analysisResult) typeMap dVars :=
 Ltac prove_fprangeval m v L1 R:=
   destruct m eqn:?; try auto;
   unfold normal, Normal, validValue, Denormal in *; canonize_hyps;
-  rewrite orb_true_iff in *;
+  try rewrite orb_true_iff in *;
   destruct L1; destruct R; canonize_hyps;
   rewrite <- Rabs_eq_Qabs in *;
   Q2R_to_head;
@@ -69,16 +69,14 @@ Ltac prove_fprangeval m v L1 R:=
   destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R; lra.
 
 Theorem FPRangeValidator_sound:
-  forall (e:expr Q) E1 E2 Gamma v m A tMap P fVars dVars,
+  forall (e:expr Q) E1 E2 Gamma v m A tMap fVars dVars,
   approxEnv E1 Gamma A fVars dVars E2 ->
   eval_expr E2 Gamma (toRExp e) v m ->
   typeCheck e Gamma tMap = true ->
-  validIntervalbounds e A P dVars = true ->
+  validRanges e A E1 Gamma ->
   validErrorbound e tMap A dVars = true ->
   FPRangeValidator e A tMap dVars = true ->
   NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars ->
-  dVars_range_valid dVars E1 A ->
-  fVars_P_sound fVars E1 P ->
   vars_typed (NatSet.union fVars dVars) Gamma ->
  (forall v, NatSet.In v dVars ->
         exists vF m, E2 v = Some vF /\ FloverMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) ->
@@ -91,8 +89,8 @@ Proof.
     as type_e
       by (eapply typingSoundnessExp; eauto).
   unfold validFloatValue.
-  edestruct (validIntervalbounds_sound e (A:=A) (P:=P))
-    as [iv_e [err_e [vR[ map_e[eval_real vR_bounded]]]]]; eauto.
+  pose proof (validRanges_single _ _ _ _ H2) as valid_e.
+  destruct valid_e as [iv_e [err_e [vR[ map_e[eval_real vR_bounded]]]]].
   destruct iv_e as  [e_lo e_hi].
   assert (Rabs (vR - v) <= Q2R (err_e))%R.
   { eapply validErrorbound_sound; eauto. }
@@ -107,17 +105,18 @@ Proof.
   destruct e;
     unfold validFloatValue in *; cbn in *;
       rewrite type_e in *; cbn in *.
-  - destruct (n mem dVars) eqn:?; simpl in *.
-    + destruct (H9 n); try set_tac.
-      destruct H12 as [m2 [env_eq [map_eq validVal]]].
-      inversion H0; subst.
-      rewrite env_eq in H14; inversion H14; subst.
-      rewrite map_eq in type_e; inversion type_e; subst; auto.
-    + Flover_compute.
-      prove_fprangeval m v L1 R.
   - Flover_compute.
-    prove_fprangeval m v L1 R.
+    destruct (n mem dVars) eqn:?.
+    + set_tac. edestruct H7 as [? [? [? [? ?]]]]; eauto.
+      rewrite H10 in type_e; inversion type_e; subst.
+      inversion H0; subst.
+      rewrite H14 in H3; inversion H3; subst.
+      auto.
+    + Flover_compute. prove_fprangeval m v L2 R.
   - Flover_compute; try congruence.
+    type_conv; subst.
+    prove_fprangeval m v L1 R.
+  - Flover_compute; destruct u; Flover_compute; try congruence.
     type_conv; subst.
     prove_fprangeval m0 v L1 R.
   - Flover_compute; try congruence.
@@ -132,18 +131,16 @@ Proof.
 Qed.
 
 Lemma FPRangeValidatorCmd_sound (f:cmd Q):
-  forall E1 E2 Gamma v vR m A tMap P fVars dVars outVars,
+  forall E1 E2 Gamma v vR m A tMap fVars dVars outVars,
   approxEnv E1 Gamma A fVars dVars E2 ->
   ssa f (NatSet.union fVars dVars) outVars ->
   bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) vR m ->
   bstep (toRCmd f) E2 Gamma v m ->
   typeCheckCmd f Gamma tMap = true ->
-  validIntervalboundsCmd f A P dVars = true ->
+  validRangesCmd f A E1 Gamma ->
   validErrorboundCmd f tMap A dVars = true ->
   FPRangeValidatorCmd f A tMap dVars = true ->
   NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
-  dVars_range_valid dVars E1 A ->
-  fVars_P_sound fVars E1 P ->
   vars_typed (NatSet.union fVars dVars) Gamma ->
  (forall v, NatSet.In v dVars ->
         exists vF m, E2 v = Some vF /\ FloverMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) ->
@@ -160,85 +157,71 @@ Proof.
           by(eapply typingSoundnessExp; eauto).
         match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in *).
         Flover_compute.
-        edestruct (validIntervalbounds_sound e L1 (Gamma := Gamma)(P:= P) (A:=A)
-                                             (fVars:=fVars) (dVars:=dVars)
-                                             (E:=E1))
-        as [iv_e [err_e [vR_e [map_e [eval_e_real bounded_vR_e]]]]]; eauto.
+        destruct H4 as [[valid_e valid_rec] valid_single].
+        pose proof (validRanges_single _ _ _ _ valid_e) as valid_e_single.
+        destruct valid_e_single
+          as [iv_e [err_e [vR_e [map_e [eval_e_real bounded_vR_e]]]]].
+        destr_factorize.
+        edestruct (validErrorbound_sound e (E1:=E1) (E2:=E2) (fVars:=fVars)
+                                         (dVars := dVars) (A:=A) tMap
+                                         (nR:=v0) (err:=err_e) (elo:=fst iv_e) (ehi:=snd iv_e))
+          as [[vF_e [m_e eval_float_e]] err_bounded_e]; eauto.
         + set_tac. split; try auto.
           split; try auto.
           hnf; intros; subst; set_tac.
-        + destr_factorize.
-          edestruct (validErrorbound_sound e (E1:=E1) (E2:=E2) (fVars:=fVars)
-                                           (dVars := dVars) (A:=A) (P:=P) tMap
-                                           (nR:=v0) (err:=err_e) (elo:=q) (ehi:=q0))
-          as [[vF_e [m_e eval_float_e]] err_bounded_e]; eauto.
-          * set_tac. split; try auto.
-            split; try auto.
-            hnf; intros; subst; set_tac.
-          * rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H20) in *; try auto.
-            apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2)
-                          (updDefVars n m Gamma) v vR m0 A tMap P fVars
-                          (NatSet.add n dVars) (outVars)); eauto.
-            { eapply approxUpdBound; eauto.
-              simpl in *.
-              apply Rle_trans with (r2:= Q2R err_e); try lra.
-              eapply err_bounded_e. eauto.
-              apply Qle_Rle.
-              rewrite Qeq_bool_iff in *.
-              destruct i; inversion Heqo0; subst.
-              rewrite R2.
-              lra. }
-            { eapply ssa_equal_set; eauto.
-              hnf. intros a; split; intros in_set.
-              - rewrite NatSet.add_spec, NatSet.union_spec;
-                  rewrite NatSet.union_spec, NatSet.add_spec in in_set.
-                destruct in_set as [P1 | [ P2 | P3]]; auto.
-              - rewrite NatSet.add_spec, NatSet.union_spec in in_set;
+        + destruct iv_e; auto.
+        + rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H18) in *; try auto.
+          apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2)
+                     (updDefVars n m Gamma) v vR m0 A tMap fVars
+                     (NatSet.add n dVars) (outVars)); eauto.
+          * eapply approxUpdBound; eauto.
+            simpl in *.
+            apply Rle_trans with (r2:= Q2R err_e); try lra.
+            eapply err_bounded_e. eauto.
+            apply Qle_Rle.
+            rewrite Qeq_bool_iff in *.
+            destruct i0; inversion Heqo0; subst.
+            rewrite R2.
+            lra.
+          * eapply ssa_equal_set; eauto.
+            hnf. intros a; split; intros in_set.
+            { rewrite NatSet.add_spec, NatSet.union_spec;
+                rewrite NatSet.union_spec, NatSet.add_spec in in_set.
+              destruct in_set as [P1 | [ P2 | P3]]; auto. }
+            { rewrite NatSet.add_spec, NatSet.union_spec in in_set;
                   rewrite NatSet.union_spec, NatSet.add_spec.
-                destruct in_set as [P1 | [ P2 | P3]]; auto. }
-            { eapply (swap_Gamma_bstep (Gamma1 := updDefVars n REAL (toRMap Gamma))); eauto.
-              eauto using Rmap_updVars_comm. }
-            { set_tac; split.
-              - split; try auto.
-                hnf; intros; subst.
-                apply H5; rewrite NatSet.add_spec; auto.
-              - hnf; intros.
+              destruct in_set as [P1 | [ P2 | P3]]; auto. }
+          * eapply (swap_Gamma_bstep (Gamma1 := updDefVars n REAL (toRMap Gamma))); eauto.
+            eauto using Rmap_updVars_comm.
+          * apply validRangesCmd_swap with (Gamma1:=updDefVars n REAL Gamma).
+            { intros x; unfold toRMap, updDefVars.
+              destruct (x =? n) eqn:?; auto. }
+            { eapply valid_rec. auto. }
+          * set_tac; split.
+            { split; try auto.
+              hnf; intros; subst.
+              apply H5; rewrite NatSet.add_spec; auto. }
+            { hnf; intros.
                 apply H5; rewrite NatSet.add_spec; auto. }
-            { intros v2 v2_fVar.
-              unfold updEnv.
-              case_eq (v2 =? n); intros v2_eq.
-              - apply Nat.eqb_eq in v2_eq; subst.
-                set_tac.
-                destruct v2_fVar as [? |[? ?]]; try congruence.
-                exists vR_e, (q1,q2), e1; split; try auto. split; try auto.
-                simpl; canonize_hyps. rewrite <- R4, <- R5. auto.
-              - apply H8; try auto.
-                set_tac. destruct v2_fVar as [v2_n | [? ?]]; try auto.
-                rewrite Nat.eqb_neq in v2_eq; congruence. }
-            { unfold fVars_P_sound. intros. unfold updEnv.
-              destruct (v2 =? n) eqn:?; eauto.
-              rewrite Nat.eqb_eq in *; subst.
-              set_tac.
-              exfalso; apply H18; set_tac. }
-            { unfold vars_typed. intros.
-              unfold updDefVars.
-              destruct (v2 =? n) eqn:?; eauto.
-              apply H10. rewrite NatSet.union_spec in *.
-              destruct H4; try auto.
-              rewrite NatSet.add_spec in H4.
-              rewrite Nat.eqb_neq in *.
-              destruct H4; subst; try congruence; auto. }
-            { intros. unfold updEnv.
-              type_conv; subst.
-              destruct (v2 =? n) eqn:?; try rewrite Nat.eqb_eq in *;
-                try rewrite Nat.eqb_neq in *.
-              - exists v1; subst. exists m1; repeat split; try auto.
-                eapply FPRangeValidator_sound; eauto.
-                set_tac. split; try auto.
-                split; try auto.
-                hnf; intros; subst; set_tac.
-              - apply H11.
-                rewrite NatSet.add_spec in H4; destruct H4;
-                  auto; subst; congruence. }
-  - eapply FPRangeValidator_sound; eauto.
+          * unfold vars_typed. intros.
+            unfold updDefVars.
+            destruct (v2 =? n) eqn:?; eauto.
+            apply H8. rewrite NatSet.union_spec in *.
+            destruct H4; try auto.
+            rewrite NatSet.add_spec in H4.
+            rewrite Nat.eqb_neq in *.
+            destruct H4; subst; try congruence; auto.
+          * intros. unfold updEnv.
+            type_conv; subst.
+            destruct (v2 =? n) eqn:?; try rewrite Nat.eqb_eq in *;
+              try rewrite Nat.eqb_neq in *.
+            { exists v1; subst. exists m1; repeat split; try auto.
+              eapply FPRangeValidator_sound; eauto.
+              set_tac. split; try auto.
+              split; try auto.
+              hnf; intros; subst; set_tac. }
+            { apply H9.
+              rewrite NatSet.add_spec in H4; destruct H4;
+                auto; subst; congruence. }
+  - destruct H4. eapply FPRangeValidator_sound; eauto.
 Qed.
diff --git a/coq/IEEE_connection.v b/coq/IEEE_connection.v
index c57c2c51ea1adb0b97f596cc913d3dff555efb0f..0034115931532afa5b87b444aa9835d09f259af5 100644
--- a/coq/IEEE_connection.v
+++ b/coq/IEEE_connection.v
@@ -474,11 +474,11 @@ Qed.
 (* (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53) *)
 (*                                     (-1022)%Z 53%Z) *)
 Lemma eval_expr_gives_IEEE (e:expr fl64) :
-  forall E1 E2 E2_real Gamma tMap vR A P fVars dVars,
+  forall E1 E2 E2_real Gamma tMap vR A fVars dVars,
     (forall x, (toREnv E2) x = E2_real x) ->
     typeCheck (B2Qexpr e) Gamma tMap = true ->
     approxEnv E1 Gamma A fVars dVars E2_real ->
-    validIntervalbounds (B2Qexpr e) A P dVars = true ->
+    validRanges (B2Qexpr e) A E1 Gamma ->
     validErrorbound (B2Qexpr e) tMap A dVars = true ->
     FPRangeValidator (B2Qexpr e) A tMap dVars = true ->
     eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) vR M64 ->
@@ -486,8 +486,6 @@ Lemma eval_expr_gives_IEEE (e:expr fl64) :
     is64BitEval (B2Qexpr e) ->
     noDowncast (B2Qexpr e) ->
     eval_expr_valid e E2 ->
-    dVars_range_valid dVars E1 A ->
-    fVars_P_sound fVars E1 P ->
     vars_typed (NatSet.union fVars dVars) Gamma ->
       (forall v,
         NatSet.In v dVars ->
@@ -503,90 +501,89 @@ Proof.
     intros * envs_eq typecheck_e approxEnv_E1_E2_real valid_rangebounds
                      valid_roundoffs valid_float_ranges eval_e_float
                      usedVars_sound is64BitEval_e noDowncast_e eval_IEEE_valid_e
-                     fVars_defined vars_typed dVars_sound dVars_valid
-                     usedVars_64bit;
+                     vars_typed dVars_sound usedVars_64bit;
     (match_pat (eval_expr _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
      revert eval_IEEE_valid_e;
      Flover_compute_asm; try congruence; type_conv; subst;
      unfold optionBind;
      intros eval_IEEE_valid_e.
      - unfold toREnv in *.
-    destruct (E2 n) eqn:HE2; try congruence.
-    exists f; split; try eauto.
-    eapply Var_load; try auto. rewrite HE2; auto.
+       destruct (E2 n) eqn:HE2; try congruence.
+       exists f; split; try eauto.
+       eapply Var_load; try auto. rewrite HE2; auto.
      - eexists; split; try eauto.
-    eapply (Const_dist') with (delta:=0%R); eauto.
-    + rewrite Rabs_R0; apply mTypeToR_pos_R.
-    + unfold perturb. lra.
-     - edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto.
-    assert (is_finite 53 1024 v_e = true).
-    { apply validValue_is_finite.
-      eapply FPRangeValidator_sound; eauto.
-      eapply eval_eq_env; eauto. }
-    rewrite eval_float_e.
-    exists (b64_opp v_e); split; try auto.
-    unfold b64_opp. rewrite <- (is_finite_Bopp _ _ pair) in H.
-    rewrite B2Q_B2R_eq; auto. rewrite B2R_Bopp.
-    eapply Unop_neg'; eauto.
-    unfold evalUnop. rewrite is_finite_Bopp in H. rewrite B2Q_B2R_eq; auto.
+       eapply (Const_dist') with (delta:=0%R); eauto.
+       + rewrite Rabs_R0; apply mTypeToR_pos_R.
+       + unfold perturb. lra.
+     - destruct valid_rangebounds as [valid_e valid_intv].
+       edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto.
+       assert (is_finite 53 1024 v_e = true).
+       { apply validValue_is_finite.
+         eapply FPRangeValidator_sound; eauto.
+         eapply eval_eq_env; eauto. }
+       rewrite eval_float_e.
+       exists (b64_opp v_e); split; try auto.
+       unfold b64_opp. rewrite <- (is_finite_Bopp _ _ pair) in H.
+       rewrite B2Q_B2R_eq; auto. rewrite B2R_Bopp.
+       eapply Unop_neg'; eauto.
+       unfold evalUnop. rewrite is_finite_Bopp in H. rewrite B2Q_B2R_eq; auto.
      - repeat (match goal with
-            |H: _ /\ _ |- _ => destruct H
+               |H: _ /\ _ |- _ => destruct H
             end).
        assert (FloverMap.find (B2Qexpr e1) tMap = Some M64 /\
-            FloverMap.find (B2Qexpr e2) tMap = Some M64 /\
-            FloverMap.find (Binop b (B2Qexpr e1) (B2Qexpr e2)) tMap = Some M64)
-           as [tMap_e1 [tMap_e2 tMap_b]].
-    { repeat split; apply (typing_expr_64_bit _ Gamma); simpl; auto.
-      - intros; apply usedVars_64bit; set_tac.
-      - intros; apply usedVars_64bit; set_tac.
-      - rewrite Heqo, Heqo4, Heqo6.
-        apply Is_true_eq_true; apply andb_prop_intro; split.
-        + apply andb_prop_intro; split; apply Is_true_eq_left; auto.
-          apply mTypeEq_refl.
-        + apply Is_true_eq_left; auto. }
-    repeat destr_factorize.
-    assert (m1 = M64).
-    { eapply (typing_agrees_expr (B2Qexpr e1)); eauto. }
-    assert (m2 = M64).
-    { eapply typing_agrees_expr; eauto. }
-    subst.
-    destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A P fVars dVars)
-      as [v_e1 [eval_float_e1 eval_rel_e1]];
-      try auto; try set_tac;
-        [ intros; apply usedVars_64bit ; set_tac | ].
-    destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A P fVars dVars)
-      as [v_e2 [eval_float_e2 eval_rel_e2]];
-      try auto; try set_tac;
-        [ intros; apply usedVars_64bit ; set_tac | ].
-    edestruct (validIntervalbounds_sound (B2Qexpr e2))
-      as [iv_2 [err_2 [nR2 [map_e2 [eval_real_e2 e2_bounded_real]]]]];
-      eauto; set_tac.
-    rewrite eval_float_e1, eval_float_e2.
-    inversion Heqo1; subst.
-    destr_factorize.
-    destruct iv_2 as [ivlo_2 ivhi_2].
-    assert (forall vF2 m2,
+               FloverMap.find (B2Qexpr e2) tMap = Some M64 /\
+               FloverMap.find (Binop b (B2Qexpr e1) (B2Qexpr e2)) tMap = Some M64)
+         as [tMap_e1 [tMap_e2 tMap_b]].
+       { repeat split; apply (typing_expr_64_bit _ Gamma); simpl; auto.
+         - intros; apply usedVars_64bit; set_tac.
+         - intros; apply usedVars_64bit; set_tac.
+         -  rewrite Heqo, Heqo3, Heqo5.
+            apply Is_true_eq_true; apply andb_prop_intro; split.
+            + apply andb_prop_intro; split; apply Is_true_eq_left; auto.
+              apply mTypeEq_refl.
+            + apply Is_true_eq_left; auto. }
+       repeat destr_factorize.
+       assert (m1 = M64).
+       { eapply (typing_agrees_expr (B2Qexpr e1)); eauto. }
+       assert (m2 = M64).
+       { eapply typing_agrees_expr; eauto. }
+       subst.
+       destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A fVars dVars)
+         as [v_e1 [eval_float_e1 eval_rel_e1]];
+         try auto; try set_tac;
+           [ intros; apply usedVars_64bit ; set_tac | ].
+       destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A fVars dVars)
+         as [v_e2 [eval_float_e2 eval_rel_e2]];
+         try auto; try set_tac;
+           [ intros; apply usedVars_64bit ; set_tac | ].
+       pose proof (validRanges_single _ _ _ _ H14) as valid_e.
+       destruct valid_e as [iv_2 [err_2 [nR2 [map_e2 [eval_real_e2 e2_bounded_real]]]]].
+       rewrite eval_float_e1, eval_float_e2.
+       inversion Heqo1; subst.
+       destr_factorize.
+       destruct iv_2 as [ivlo_2 ivhi_2].
+       assert (forall vF2 m2,
                eval_expr E2_real Gamma (toRExp (B2Qexpr e2)) vF2 m2 ->
                (Rabs (nR2 - vF2) <= Q2R err_2))%R.
-    { eapply validErrorbound_sound; try eauto; try set_tac. }
+    { eapply validErrorbound_sound; try eauto; set_tac. }
     assert (contained (Q2R (B2Q v_e2))
                       (widenInterval
                          (Q2R ivlo_2, Q2R ivhi_2) (Q2R err_2))).
     { eapply distance_gives_iv.
       - simpl. eapply e2_bounded_real.
-      - eapply H11. instantiate(1:=M64).
+      - eapply H15. instantiate(1:=M64).
         eapply eval_eq_env; eauto. }
     assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R).
     { intros; subst; simpl in *.
       andb_to_prop R3.
       apply le_neq_bool_to_lt_prop in L3.
       destruct L3; hnf; intros.
-      - rewrite H15 in *.
-        apply Qlt_Rlt in H14.
-        rewrite Q2R0_is_0, Q2R_plus in H14. lra.
-      - rewrite H15 in *.
-        apply Qlt_Rlt in H14.
-        rewrite Q2R0_is_0, Q2R_minus in H14; lra. }
+      - rewrite H19 in *.
+        apply Qlt_Rlt in H18.
+        rewrite Q2R0_is_0, Q2R_plus in H18. lra.
+      - rewrite H19 in *.
+        apply Qlt_Rlt in H18.
+        rewrite Q2R0_is_0, Q2R_minus in H18; lra. }
     assert (validFloatValue
               (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2))) M64).
     { eapply (FPRangeValidator_sound (Binop b (B2Qexpr e1) (B2Qexpr e2)));
@@ -598,17 +595,19 @@ Proof.
       - Flover_compute.
         apply Is_true_eq_true.
         repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
+      - repeat split; try auto.
+        + intros ? iv2 err2 find. subst.
+          destruct iv2; rewrite find in *;
+            eapply H11; eauto.
+        + rewrite Heqo0. auto.
       - Flover_compute.
         apply Is_true_eq_true.
         repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
-        apply andb_prop_intro; split; auto using Is_true_eq_left.
+        apply andb_prop_intro; split; try auto using Is_true_eq_left.
+        apply Is_true_eq_left.
+        rewrite L4, R1. auto.
       - Flover_compute.
         apply Is_true_eq_true.
-        repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left.
-        apply Is_true_eq_left. inversion Heqo2; subst. auto.
-      - rewrite Heqo, Heqo0.
-        apply Is_true_eq_true.
-        inversion Heqo1; inversion Heqo2; subst.
         repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. }
     assert (validFloatValue (Q2R (B2Q v_e1)) M64).
     { eapply (FPRangeValidator_sound (B2Qexpr e1)); try eauto; try set_tac.
@@ -635,13 +634,14 @@ Proof.
       - cbn. Flover_compute.
         apply Is_true_eq_true.
         repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
+      - cbn; repeat split; try auto.
+        + intros ? iv2 err2 find. subst.
+          destruct iv2; rewrite find in *;
+            eapply H11; eauto.
+        + rewrite Heqo0. auto.
       - cbn. Flover_compute.
         apply Is_true_eq_true.
         repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
-      - cbn. Flover_compute.
-        inversion Heqo1; inversion Heqo2; subst.
-        apply Is_true_eq_true.
-        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
       - cbn. Flover_compute.
         inversion Heqo1; inversion Heqo2; subst.
         apply Is_true_eq_true.
@@ -651,14 +651,14 @@ Proof.
       andb_to_prop R3.
       apply le_neq_bool_to_lt_prop in L3.
       destruct L3 as [case_low | case_high]; hnf; intros.
-      - rewrite H19 in *.
+      - rewrite H23 in *.
         apply Qlt_Rlt in case_low.
         rewrite Q2R0_is_0, Q2R_plus in case_low. lra.
-      - rewrite H19 in *.
+      - rewrite H23 in *.
         apply Qlt_Rlt in case_high.
         rewrite Q2R0_is_0, Q2R_minus in case_high; lra. }
-    clear H2 H12 dVars_sound dVars_valid usedVars_64bit vars_typed fVars_defined
-    usedVars_sound R2 R1 L1 L R6 L0 R3 R4 L2 R5 R7 L5 Heqo Heqo0 Heqo1 IHe1
+    clear H2 H12 dVars_sound usedVars_64bit vars_typed usedVars_sound R2 R1 L1 L
+    L0 R3 R4 L2 R5 Heqo Heqo0 Heqo1 IHe1
     IHe2.
     pose proof (fexp_correct 53 1024 eq_refl) as fexpr_corr.
     assert (forall k : Z, (-1022 < k)%Z ->
@@ -677,7 +677,7 @@ Proof.
     { revert H1; intros case_val.
       destruct case_val as [eval_is_zero | eval_normal]; try auto.
       left; unfold Normal, Denormal in H15; unfold Normal;
-        destruct H15 as [normal_b | [denormal_b |zero_b]].
+        destruct H19 as [normal_b | [denormal_b |zero_b]].
       - repeat rewrite <- B2Q_B2R_eq; try auto.
       - destruct denormal_b.
         assert ((Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))) < (Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))))%R.
@@ -697,7 +697,7 @@ Proof.
         unfold IZR in eval_normal.
         simpl in eval_normal. rewrite <- INR_IPR in eval_normal.
         simpl in eval_normal. lra. }
-    pose proof (validValue_bounded b v_e1 v_e2 H2 H18) as cond_valid.
+    pose proof (validValue_bounded b v_e1 v_e2 H2 H22) as cond_valid.
     destruct b; revert H1; intros case_eval.
     (* Addition *)
     + unfold evalBinop in *. unfold b64_plus.
@@ -865,7 +865,7 @@ Proof.
       - intros; apply usedVars_64bit; set_tac.
       - intros; apply usedVars_64bit; set_tac.
       - intros; apply usedVars_64bit; set_tac.
-      - rewrite Heqo, Heqo4, Heqo6, Heqo8.
+      - rewrite Heqo, Heqo3, Heqo5, Heqo7.
         apply Is_true_eq_true; apply andb_prop_intro; split.
         + apply andb_prop_intro; split.
           * apply andb_prop_intro; split.
@@ -883,15 +883,15 @@ Proof.
     assert (m3 = M64).
     { eapply (typing_agrees_expr (B2Qexpr e3)); eauto. }
     subst.
-    destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A P fVars dVars)
+    destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A fVars dVars)
       as [v_e1 [eval_float_e1 eval_rel_e1]];
       try auto; try set_tac;
         [ intros; apply usedVars_64bit ; set_tac | ].
-    destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A P fVars dVars)
+    destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A fVars dVars)
       as [v_e2 [eval_float_e2 eval_rel_e2]];
       try auto; try set_tac;
         [ intros; apply usedVars_64bit ; set_tac | ].
-    destruct (IHe3 E1 E2 E2_real Gamma tMap v3 A P fVars dVars)
+    destruct (IHe3 E1 E2 E2_real Gamma tMap v3 A fVars dVars)
       as [v_e3 [eval_float_e3 eval_rel_e3]];
       try auto; try set_tac;
         [ intros; apply usedVars_64bit ; set_tac | ].
@@ -902,12 +902,12 @@ Proof.
 Qed.
 
 Lemma bstep_gives_IEEE (f:cmd fl64) :
-  forall E1 E2 E2_real Gamma tMap vR vF A P fVars dVars outVars,
+  forall E1 E2 E2_real Gamma tMap vR vF A fVars dVars outVars,
     (forall x, (toREnv E2) x = E2_real x) ->
     approxEnv E1 Gamma A fVars dVars E2_real ->
     ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars ->
     typeCheckCmd (B2Qcmd f) Gamma tMap = true ->
-    validIntervalboundsCmd (B2Qcmd f) A P dVars = true ->
+    validRangesCmd (B2Qcmd f) A E1 Gamma ->
     validErrorboundCmd (B2Qcmd f) tMap A dVars = true ->
     FPRangeValidatorCmd (B2Qcmd f) A tMap dVars = true ->
     bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap Gamma) vR REAL ->
@@ -916,8 +916,6 @@ Lemma bstep_gives_IEEE (f:cmd fl64) :
     is64BitBstep (B2Qcmd f) ->
     noDowncastFun (B2Qcmd f) ->
     bstep_valid f E2 ->
-    dVars_range_valid dVars E1 A ->
-    fVars_P_sound fVars E1 P ->
     vars_typed (NatSet.union fVars dVars) Gamma ->
       (forall v,
         NatSet.In v dVars ->
@@ -933,8 +931,7 @@ Proof.
     intros * envs_eq approxEnv_E1_E2_real ssa_f typeCheck_f valid_ranges_f
                      valid_roundoffs_f valid_float_ranges bstep_real bstep_float
                      freeVars_sound is64_eval nodowncast_f bstep_sound
-                     dVars_sound fVars_defined vars_typed dVars_valid
-                     freeVars_typed;
+                     vars_typed dVars_valid freeVars_typed;
     cbn in *;
     revert bstep_sound;
     Flover_compute_asm; try congruence; type_conv; subst;
@@ -962,6 +959,7 @@ Proof.
                    eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) (Q2R (B2Q v_e)) M64)
            as eval_float_e.
     { eapply eval_expr_gives_IEEE; try eauto.
+      - destruct valid_ranges_f as [[? ?] ?]; auto.
       - hnf; intros. rewrite NatSet.diff_spec in H0.
         destruct H0.
         specialize (H25 a H0). rewrite NatSet.union_spec in H25.
@@ -977,24 +975,21 @@ Proof.
         set_tac.  apply H26; set_tac. }
     destruct eval_float_e as [v_e [eval_float_e eval_rel_e]].
     assert (forall v m, eval_expr E2_real Gamma (toRExp (B2Qexpr e)) v m ->
-                   Rabs (v0 - v) <= Q2R e2)%R
+                   Rabs (v0 - v) <= Q2R e0)%R
       as err_e_valid.
     { eapply validErrorbound_sound; try eauto.
       - hnf; intros. rewrite NatSet.diff_spec in H0.
         destruct H0. specialize (H25 a H0). rewrite NatSet.union_spec in H25.
-        destruct H25; try auto; congruence. }
-    assert (Rabs (v0 - (Q2R (B2Q v_e))) <= Q2R e2)%R.
+        destruct H25; try auto; congruence.
+      - destruct valid_ranges_f as [[? ?] ?]; auto.
+      - instantiate (1:= snd i). instantiate (1:=fst i).
+        destruct i; simpl in *; auto. }
+    assert (Rabs (v0 - (Q2R (B2Q v_e))) <= Q2R e0)%R.
     { eapply err_e_valid. eapply eval_eq_env; eauto. }
     (* Now construct a new evaluation according to our big-step semantics
        using lemma validErrorboundCmd_gives_eval *)
-    (* destruct (A (getRetExp (B2Qcmd f))) as [iv_f err_f] eqn:A_f. *)
-    (* destruct iv_f as [ivlo_f ivhi_f]. *)
-    edestruct (validIntervalboundsCmd_sound) as [iv_ret [err_ret [v_ret
-                                                                    [map_ret
-                                                                       [eval_ret bound_ret]]]]];
-      eauto.
-    { cbn. Flover_compute.
-      rewrite L0, R4, R3, R2. auto. }
+    destruct valid_ranges_f as [[valid_e valid_cont] valid_single].
+    destruct valid_single as [iv_ret [err_ret [v_ret [map_ret [eval_ret bound_ret]]]]].
     assert (exists vF m, bstep (toRCmd (B2Qcmd f)) (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) vF m).
     { eapply validErrorboundCmd_gives_eval with (E1 := updEnv n v0 E1)
                                                   (elo:=fst(iv_ret))
@@ -1023,28 +1018,11 @@ Proof.
           eauto.
         intros; unfold updDefVars, toRMap.
         destruct (n0 =? n); auto.
-      - unfold dVars_range_valid in *. intros. unfold updEnv. set_tac.
-        destruct H1; subst.
-        + exists v0, (q1, q2), e1; split; try eauto.
-          * rewrite Nat.eqb_refl; auto.
-          * split; try auto.
-            edestruct validIntervalbounds_sound
-              as [iv_e [err_e [v_e' [map_e [? ?]]]]]; eauto.
-            { set_tac; split; try auto. split; try auto.
-              hnf; intros. eapply H26. subst; set_tac. }
-            simpl. destr_factorize; simpl in *.
-            canonize_hyps. rewrite <- R4, <- R3.
-            rewrite <- (meps_0_deterministic _ H17 H1) in H2; auto.
-        + destruct H1.
-          rewrite <- Nat.eqb_neq in H1.
-          rewrite H1.
-          apply dVars_sound; auto.
-      - unfold fVars_P_sound; intros; unfold updEnv.
-        destruct (v1 =? n) eqn:?.
-        + rewrite Nat.eqb_eq in Heqb; subst; exfalso.
-          set_tac. apply H26; rewrite NatSet.union_spec; auto.
-        + apply fVars_defined; auto.
-      - unfold IntervalValidation.vars_typed. intros.
+      - eapply validRangesCmd_swap with (Gamma1 :=updDefVars n REAL Gamma);
+          try auto.
+        intros x; unfold toRMap, updDefVars.
+        destruct (x =? n); auto.
+      - unfold RealRangeArith.vars_typed. intros.
         unfold updDefVars. destruct (v1 =? n) eqn:?.
         + exists M64; auto.
         + apply vars_typed.
@@ -1063,7 +1041,7 @@ Proof.
     subst.
     destruct (IHf (updEnv n v0 E1) (updFlEnv n v_e E2)
                   (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) tMap
-                  vR vF_new A P fVars (NatSet.add n dVars) outVars); try eauto.
+                  vR vF_new A fVars (NatSet.add n dVars) outVars); try eauto.
     + intros. unfold toREnv, updFlEnv, updEnv.
       destruct (x =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
     + eapply approxUpdBound; eauto.
@@ -1079,6 +1057,10 @@ Proof.
       * rewrite NatSet.add_spec in H1;
           rewrite NatSet.union_spec, NatSet.add_spec in *;
           destruct H1; auto. destruct H1; auto.
+    + eapply validRangesCmd_swap with (Gamma1 := updDefVars n REAL Gamma);
+        try auto.
+      intros x; unfold toRMap, updDefVars.
+      destruct (x =? n); auto.
     + eapply (swap_Gamma_bstep (Gamma1:= updDefVars n REAL (toRMap Gamma)));
         eauto.
       intros; unfold updDefVars, toRMap.
@@ -1098,29 +1080,7 @@ Proof.
     + destruct bstep_sound as [eval_sound bstep_sound].
       rewrite eval_float_e in bstep_sound; unfold optionBind in bstep_sound.
       auto.
-    + unfold dVars_range_valid in *; intros; unfold updEnv.
-      destruct (v1 =? n) eqn:?.
-      * set_tac. rewrite Nat.eqb_eq in Heqb; subst.
-        destruct H1 as [? | [? ?]]; try congruence.
-        exists v0. edestruct validIntervalbounds_sound as [iv_e [err_e [? [? [? ?]]]]]; eauto.
-        { set_tac; split; auto. split; auto.
-          hnf; intros; subst; set_tac. }
-        canonize_hyps.
-        destr_factorize; simpl in *.
-        exists (q1,q2), e1.
-        split; try auto.
-        split; try auto.
-        simpl in *. rewrite R4, R3 in *.
-        rewrite <- (meps_0_deterministic _ H4 H17). auto.
-      * eapply dVars_sound; set_tac.
-        destruct H1; rewrite Nat.eqb_neq in Heqb; try congruence.
-        destruct H1; auto.
-    + unfold fVars_P_sound. intros; unfold updEnv.
-      destruct (v1 =? n) eqn:?.
-      * rewrite Nat.eqb_eq in Heqb; subst; exfalso.
-        set_tac. apply H26; rewrite NatSet.union_spec; auto.
-      * apply fVars_defined. auto.
-    + unfold IntervalValidation.vars_typed.
+    + unfold RealRangeArith.vars_typed.
       intros. unfold updDefVars. destruct (v1 =? n) eqn:?.
       * exists M64; auto.
       * apply vars_typed.
@@ -1158,9 +1118,10 @@ Proof.
       eapply bstep_eq_env with (E1:= toREnv (updFlEnv n v_e E2)); eauto.
       intros; unfold toREnv, updFlEnv, updEnv.
       destruct (x0 =? n); auto.
-  - edestruct (eval_expr_gives_IEEE); eauto.
-    exists x; destruct H.
-    split; try auto. apply ret_b; auto.
+  - destruct valid_ranges_f as [? ?].
+    edestruct (eval_expr_gives_IEEE) as [v_res [eval_float eval_e]]; eauto.
+    exists v_res; split; try auto.
+    apply ret_b; auto.
 Qed.
 
 Theorem IEEE_connection_expr e A P E1 E2 defVars:
@@ -1198,17 +1159,18 @@ Proof.
     { eapply typing_agrees_expr; eauto. }
     subst.
     edestruct eval_expr_gives_IEEE; eauto.
-    + set_tac.
-    + unfold dVars_range_valid. intros. inversion H7.
-    + unfold vars_typed. intros.
-      apply H5.
-      set_tac. destruct H7; try auto.
-      inversion H7.
-    + intros. inversion H7.
-    + destruct H7 as [eval_float_f eval_rel].
-      exists x, err, vR, x0.
-      repeat split; try auto.
-      eapply roundoff_sound; eauto.
+  - eapply RealRangeValidator.RangeValidator_sound; eauto.
+    + unfold dVars_range_valid; intros; set_tac.
+    + hnf. intros; set_tac.
+    + hnf; intros. apply H5. set_tac. destruct H7; set_tac.
+  - set_tac.
+  - hnf; intros.
+    apply H5. set_tac. destruct H7; set_tac.
+  - intros. set_tac.
+  - destruct H7 as [eval_float_f eval_rel].
+    exists x, err, vR, x0.
+    repeat split; try auto.
+    eapply roundoff_sound; eauto.
 Qed.
 
 Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
@@ -1234,10 +1196,6 @@ Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
     (forall vF m,
         bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars vF m ->
         (Rabs (vR - vF) <= Q2R err)%R).
-(**
-   The proofs is a simple composition of the soundness proofs for the range
-   validator and the error bound validator.
-**)
 Proof.
   intros.
   unfold CertificateCheckerCmd in *.
@@ -1256,20 +1214,27 @@ Proof.
     assert (m = M64).
     { eapply typing_agrees_cmd; eauto. }
     subst.
-    edestruct bstep_gives_IEEE; eauto.
-    + eapply ssa_equal_set; eauto.
+    assert (ssa (B2Qcmd f) (NatSet.union (freeVars (B2Qcmd f)) (NatSet.empty)) outVars).
+    { eapply ssa_equal_set; eauto.
       hnf; intros; split; intros; set_tac.
       destruct H7; try auto.
-      inversion H7.
+      inversion H7. }
+    edestruct bstep_gives_IEEE; eauto.
+    + eapply RealRangeValidator.RangeValidatorCmd_sound; eauto.
+      * hnf; intros; set_tac.
+      * hnf; intros; set_tac.
+      * hnf; intros.
+        apply H4; set_tac.
+      * hnf; intros.
+        apply H5; set_tac.
+        destruct H8; set_tac.
+      * set_tac.
     + set_tac.
-    + unfold dVars_range_valid. intros.
-      inversion H7.
-    + unfold fVars_P_sound; intros.
-      apply H4; rewrite NatSet.mem_spec; auto.
-    + unfold vars_typed. intros. apply H5. set_tac. destruct H7; try auto.
-      inversion H7.
-    + intros. inversion H7.
-    + destruct H7.
+    + hnf; intros.
+      apply H5.
+      set_tac; destruct H8; set_tac.
+    + intros; set_tac.
+    + destruct H8.
       exists x, err, vR, x0, M64.
       repeat split; auto.
 Qed.
diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v
index 0edb43488c423957f9aec259468412bebeeebb10..e7d7451636ac773c92c5a9cf61b809ba327c4773 100644
--- a/coq/IntervalValidation.v
+++ b/coq/IntervalValidation.v
@@ -138,7 +138,7 @@ Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P:precond)
     NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
     fVars_P_sound fVars E P ->
     vars_typed (NatSet.union fVars dVars) Gamma ->
-    validRanges f A E.
+    validRanges f A E Gamma.
     (* exists iv err vR, *)
     (*   FloverMap.find f A = Some (iv, err) /\ *)
     (*   eval_expr E (toRMap Gamma) (toREval (toRExp f)) vR REAL /\ *)
diff --git a/coq/RealRangeArith.v b/coq/RealRangeArith.v
index 35211730b839d59e5d6756e912d3e2d4738e245e..81488c0c3c3a62a97af38242b0381add3364f48e 100644
--- a/coq/RealRangeArith.v
+++ b/coq/RealRangeArith.v
@@ -91,7 +91,6 @@ Proof.
     eapply swap_Gamma_eval_expr; eauto.
 Qed.
 
-
 Lemma validRanges_swap Gamma1 Gamma2:
   forall e A E,
     (forall n, (toRMap Gamma1) n =  toRMap (Gamma2) n) ->
@@ -107,9 +106,9 @@ Proof.
          lra]).
   - destruct valid1; auto.
   - destruct valid1 as [[? [? ?]] ?]; auto.
-  - admit.
+  - destruct valid1 as [[? [? ?]] ?]; auto.
   - destruct valid1; auto.
-Admitted.
+Qed.
 
 Fixpoint validRangesCmd (f:cmd Q) A E Gamma {struct f} : Prop :=
   match f with
@@ -133,3 +132,26 @@ Corollary validRangesCmd_single f A E Gamma:
 Proof.
   destruct f; simpl in *; intros [ _ valid_f]; auto.
 Qed.
+
+Lemma validRangesCmd_swap:
+  forall f A E Gamma1 Gamma2,
+    (forall n, (toRMap Gamma1) n =  toRMap (Gamma2) n) ->
+    validRangesCmd f A E Gamma1 ->
+    validRangesCmd f A E Gamma2.
+Proof.
+  induction f; intros * Gamma_swap valid1; simpl in *; try (split; auto);
+    try (
+        destruct valid1 as [_ [? [? [? [? [? ?]]]]]];
+        repeat eexists; eauto;
+        [eapply swap_Gamma_bstep with (Gamma1 := (toRMap Gamma1)); eauto |
+         lra |
+         lra]).
+  - destruct valid1 as [[? valid_all_exec] ?]; split.
+    + eapply validRanges_swap; eauto.
+    + intros. eapply IHf; [ | eapply valid_all_exec].
+      * intros x. unfold updDefVars.
+        destruct (x =? n) eqn:?; auto.
+      * eapply swap_Gamma_eval_expr with (Gamma1 := toRMap Gamma2); eauto.
+  - destruct valid1.
+    eapply validRanges_swap; eauto.
+Qed.
\ No newline at end of file
diff --git a/coq/RoundoffErrorValidator.v b/coq/RoundoffErrorValidator.v
index 4336676a240fa8b8419828fffe8940e9d3eb1508..556eeb045a310261f95f3b78c7054224b772a88f 100644
--- a/coq/RoundoffErrorValidator.v
+++ b/coq/RoundoffErrorValidator.v
@@ -2,7 +2,8 @@ From Coq
      Require Import Reals.Reals QArith.Qreals.
 
 From Flover
-     Require Export Infra.ExpressionAbbrevs ErrorValidation RealRangeValidator.
+     Require Export Infra.ExpressionAbbrevs ErrorValidation RealRangeValidator
+     Typing Environments.
 
 Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType) (A:analysisResult) (dVars:NatSet.t) :=
   (* if *)
@@ -12,17 +13,15 @@ Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType) (A:analysi
 
 Theorem RoundoffErrorValidator_sound:
 forall (e : expr Q) (E1 E2 : env) (fVars dVars : NatSet.t) (A : analysisResult)
-         (nR : R) (err : error) (P : precond) (elo ehi : Q) (Gamma : FloverMap.t mType)
+         (nR : R) (err : error) (elo ehi : Q) (Gamma : FloverMap.t mType)
          (defVars : nat -> option mType),
-       Typing.typeCheck e defVars Gamma = true ->
-       Environments.approxEnv E1 defVars A fVars dVars E2 ->
+       typeCheck e defVars Gamma = true ->
+       approxEnv E1 defVars A fVars dVars E2 ->
        NatSet.Subset (usedVars e -- dVars) fVars ->
        eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
        RoundoffErrorValidator e Gamma A dVars = true ->
-       RangeValidator e A P dVars = true ->
-       IntervalValidation.dVars_range_valid dVars E1 A ->
-       IntervalValidation.fVars_P_sound fVars E1 P ->
-       IntervalValidation.vars_typed (fVars ∪ dVars) defVars ->
+       validRanges e A E1 defVars ->
+       vars_typed (fVars ∪ dVars) defVars ->
        FloverMap.find (elt:=intv * error) e A = Some (elo, ehi, err) ->
        (exists (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m) /\
        (forall (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m -> (Rabs (nR - nF) <= Q2R err)%R).
@@ -30,3 +29,33 @@ Proof.
   intros. cbn in *.
   eapply validErrorbound_sound; eauto.
 Qed.
+
+Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType) (A:analysisResult) (dVars:NatSet.t) :=
+  (* if *)
+  validErrorboundCmd f tMap A dVars.
+  (*then true *)
+  (* else validAffineErrorboundsCmd e A tMap dVars ... *)
+
+Theorem RoundoffErrorValidatorCmd_sound f:
+  forall A E1 E2 outVars fVars dVars vR elo ehi err Gamma defVars,
+    typeCheckCmd f defVars Gamma = true ->
+    approxEnv E1 defVars A fVars dVars E2 ->
+    ssa f (NatSet.union fVars dVars) outVars ->
+    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
+    bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
+    validErrorboundCmd f Gamma A dVars = true ->
+    validRangesCmd f A E1 defVars ->
+    vars_typed (NatSet.union fVars dVars) defVars ->
+    FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
+    (exists vF m,
+        bstep (toRCmd f) E2 defVars vF m) /\
+    (forall vF mF,
+    bstep (toRCmd f) E2 defVars vF mF ->
+    (Rabs (vR - vF) <= (Q2R err))%R).
+Proof.
+  intros.
+  cbn in *.
+  split.
+  - eapply validErrorboundCmd_gives_eval; eauto.
+  - intros. eapply validErrorboundCmd_sound; eauto.
+Qed.
\ No newline at end of file
diff --git a/coq/floverParser.v b/coq/floverParser.v
index aee0429ae9f24b1134406319e61fcaa90414259b..3d35b288bcd824e9b24af5005b997fb327a3c678 100644
--- a/coq/floverParser.v
+++ b/coq/floverParser.v
@@ -1,4 +1,5 @@
-Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List Coq.Reals.Reals.
+Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List
+        Coq.Reals.Reals Coq.Bool.Bool Coq.QArith.QArith.
 
 Require Import CertificateChecker Infra.MachineType.