fact: Fixpoint fv_aexp (a: aexp) : IdentSet.t := match a with | CONST n => IdentSet.empty | VAR v => IdentSet.singleton v | PLUS a1 a2 => IdentSet.union (fv_aexp a1) (fv_aexp a2) | MINUS a1 a2 => IdentSet.union (fv_aexp a1) (fv_aexp a2) end.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)