fact: Fixpoint dce (c: com) (L: IdentSet.t): com := match c with | SKIP => SKIP | ASSIGN x a => if IdentSet.mem x L then ASSIGN x a else SKIP | SEQ c1 c2 => SEQ (dce c1 (live c2 L)) (dce c2 L) | IFTHENELSE b c1 c2 => IFTHENELSE b (dce c1 L) (dce c2 L) | WHILE b c => WHILE b (dce c (live (WHILE b c) L)) end.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)