proposition: Lemma fp1_widen2_invariant : forall e b i i' l, fp1 (widen2 e)(widen2 e) b i (abstract_i i) = (i', Some l) -> l = widen2 e.
proof: Proof. intros e b i i' l; unfold fp1. case_eq (intersect_env true (widen2 e) b); [intros a Hinter| intros Hinter] ; simpl. case_eq (abstract_i i a); intros i'0 [l'' | ] Ha; try (intros; discriminate). intros Heq; injection Heq; do 2 intro; subst l i'; clear Heq. rewrite join_widen2; auto. assert (compatible a l'') by (apply (abstract_i_compatible i a l''); rewrite Ha; auto). apply compatible_trans with a. apply compatible_trans with (widen2 e). apply compatible_widen2. apply compatible_intersect_env with (1:=Hinter). apply compatible_join_env_left; auto. intros Heq; injection Heq; do 2 intro; subst l; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom