proposition: Lemma fp_invariant : forall e b i i2 l', fp e b i (abstract_i i) = (i2, Some l') -> fp l' b i (abstract_i i) = (i2, Some l').
proof: Proof. intros e b i i2 l'; unfold fp. case_eq (fp2 e e b i (abstract_i i)); [intros i1 l1 | intros l1]; intros Hfp2. intros Heq; injection Heq; do 2 intro; subst i1 l1; clear Heq. rewrite fp2_invariant with (3:=Hfp2); auto. apply abstract_i_compatible. apply compatible_refl. assert (Hac :=abstract_i_compatible i). case_eq (fp2 e l1 b i (abstract_i i)). intros i' l2 Hfp2_2 Heq;injection Heq; do 2 intro; subst i' l2; clear Heq. rewrite fp2_invariant with (e:= e)(e':=l1)(f:=abstract_i i)(i':=i2); auto. apply fp2_compatible2 with (2:=Hfp2); auto. apply compatible_refl. intros l2 Hfp2_2. case_eq (fp1 (widen2 e)(widen2 e) b i (abstract_i i)); intros i' [l3 | ] Hfp1 Heq; try (intros; discriminate). injection Heq; do 2 intro; subst l' i2; clear Heq. rewrite fp1_widen2_invariant with (1:=Hfp1) in Hfp1. rewrite fp2_widen2_eq_fp1 with (1:=Hfp1); auto. Qed.
imports: syntax little denot Bool List String ZArith axiom