fact: Fixpoint aeval (a: aexp) (s: store) : Z := match a with | CONST n => n | VAR x => s x | PLUS a1 a2 => aeval a1 s + aeval a2 s | MINUS a1 a2 => aeval a1 s - aeval a2 s | TIMES a1 a2 => aeval a1 s * aeval a2 s end.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)