Commit 8220b270 authored by Heiko Becker's avatar Heiko Becker

Slight changes to environment approximation relation, fixes #10

parent d9796e96
......@@ -17,7 +17,7 @@ Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Pr
approxEnv emptyEnv A NatSet.empty NatSet.empty emptyEnv
|approxUpdFree E1 E2 A v1 v2 x fVars dVars:
approxEnv E1 A fVars dVars E2 ->
(Rabs (v1 - v2) <= v1 * Q2R machineEpsilon)%R ->
(Rabs (v1 - v2) <= Rabs v1 * Q2R machineEpsilon)%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
|approxUpdBound E1 E2 A v1 v2 x fVars dVars:
......@@ -141,7 +141,7 @@ Proof.
apply Rmult_le_compat_r.
{ apply mEps_geq_zero. }
{ rewrite <- maxAbs_impl_RmaxAbs.
apply contained_leq_maxAbs_val.
apply contained_leq_maxAbs.
unfold contained; simpl.
pose proof (validIntervalbounds_sound (Var Q x) A P (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) bounds_valid (fVars := (NatSet.add x fVars))) as valid_bounds_prf.
rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment