proposition: Lemma fp_precondition : forall e b i1 i2 i3 l', fp e b i1 (abstract_i i2) =(i3, Some l') -> forall g, i_a Ab.m g (a_conj (a_b b) (to_a l')) -> i_a Ab.m g (pc i3 (to_a l')).
proof: Proof. intros e b i1 i2 i3 l'. unfold fp. case_eq (fp2 e e b i1 (abstract_i i2)); [intros i' [l1 | ] Hfp2 Heq| intros l Hfp2] . injection Heq; do 2 intro; subst i3 l1. assert (Hcee: compatible e e) by apply compatible_refl. exact (fp2_precondition1 _ _ _ _ _ _ _ Hcee Hfp2). discriminate. case_eq (fp2 e l b i1 (abstract_i i2)); [intros i' [l1 | ] Hfp2' Heq| intros l1 Hfp2'] . injection Heq; do 2 intro; subst i3 l1. assert (Hcel : compatible e l). apply fp2_compatible2 with (2:= Hfp2); auto. exact (abstract_i_compatible i2). apply compatible_refl. exact (fp2_precondition1 _ _ _ _ _ _ _ Hcel Hfp2'). discriminate. case_eq (fp1 (widen2 e)(widen2 e) b i1 (abstract_i i2)); intros a_i [l2 | ] Hfp1 Heq g Ha. injection Heq; do 2 intro; subst a_i l'. apply precondition_shift with (a := to_a l2). intros; apply widen2_top. apply fp1_precondition with (2:=Hfp1); auto. apply compatible_refl. discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom