fact: Fixpoint beval (b: bexp) (s: store) : bool := match b with | TRUE => true | FALSE => false | EQUAL a1 a2 => aeval a1 s =? aeval a2 s | LESSEQUAL a1 a2 => aeval a1 s <=? aeval a2 s | NOT b1 => negb (beval b1 s) | AND b1 b2 => beval b1 s && beval b2 s end.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)