fact: Fixpoint live (c: com) (L: IdentSet.t) : IdentSet.t := match c with | SKIP => L | ASSIGN x a => if IdentSet.mem x L then IdentSet.union (IdentSet.remove x L) (fv_aexp a) else L | SEQ c1 c2 => live c1 (live c2 L) | IFTHENELSE b c1 c2 => IdentSet.union (fv_bexp b) (IdentSet.union (live c1 L) (live c2 L)) | WHILE b c => let L' := IdentSet.union (fv_bexp b) L in let default := IdentSet.union (fv_com (WHILE b c)) L in postfixpoint (fun x => IdentSet.union L' (live c x)) default end.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)