fact: Fixpoint ceval_step (st : state) (c : com) (i : nat) : option state := match i with | O => None | S i' => match c with | SKIP => Some st | l ::= a1 => Some (t_update st l (aeval st a1)) | c1 ;; c2 => LETOPT st' <== ceval_step st c1 i' IN ceval_step st' c2 i' | IFB b THEN c1 ELSE c2 FI => if (beval st b) then ceval_step st c1 i' else ceval_step st c2 i' | WHILE b1 DO c1 END => if (beval st b1) then LETOPT st' <== ceval_step st c1 i' IN ceval_step st' c i' else Some st end end.
imports: Coq.omega.Omega Coq.Arith.Arith Imp Maps