proposition: Lemma live_while_charact: forall b c L, let L' := live (WHILE b c) L in IdentSet.Subset (fv_bexp b) L' /\ IdentSet.Subset L L' /\ IdentSet.Subset (live c L') L'.
proof: Proof. intros. generalize (postfixpoint_charact (fun x : IdentSet.t => IdentSet.union (IdentSet.union (fv_bexp b) L) (live c x)) (IdentSet.union (IdentSet.union (fv_bexp b) (fv_com c)) L)). simpl in L'. fold L'. intros [A|A]. - split. fsetdec. split; fsetdec. - rewrite A. split. fsetdec. split. fsetdec. eapply ISProp.subset_trans. apply live_upper_bound. fsetdec. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)