fact: Fixpoint ceval_step3 (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 => match (ceval_step3 st c1 i') with | Some st' => ceval_step3 st' c2 i' | None => None end | IFB b THEN c1 ELSE c2 FI => if (beval st b) then ceval_step3 st c1 i' else ceval_step3 st c2 i' | WHILE b1 DO c1 END => if (beval st b1) then match (ceval_step3 st c1 i') with | Some st' => ceval_step3 st' c i' | None => None end else Some st end end.
imports: Coq.omega.Omega Coq.Arith.Arith Imp Maps