fact: Fixpoint correct_allocation (c: com) (L: IdentSet.t) : bool := match c with | SKIP => true | ASSIGN x a => if IdentSet.mem x L then match expr_is_var a with | None => IdentSet.for_all (fun z => String.eqb z x || negb (String.eqb (f z) (f x))) L | Some y => IdentSet.for_all (fun z => String.eqb z x || String.eqb z y || negb (String.eqb (f z) (f x))) L end else true | SEQ c1 c2 => correct_allocation c1 (live c2 L) && correct_allocation c2 L | IFTHENELSE b c1 c2 => correct_allocation c1 L && correct_allocation c2 L | WHILE b c => correct_allocation c (live (WHILE b c) L) end.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)