fact: Fixpoint modified_by (c: com) (x: ident) : Prop := match c with | SKIP => False | ASSIGN y a => x = y | SEQ c1 c2 => modified_by c1 x \/ modified_by c2 x | IFTHENELSE b c1 c2 => modified_by c1 x \/ modified_by c2 x | WHILE b c1 => modified_by c1 x end.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)