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 (l !-> aeval st a1 ; st) | <{ c1 ; c2 }> => match (ceval_step3 st c1 i') with | Some st' => ceval_step3 st' c2 i' | None => None end | <{ if b then c1 else c2 end }> => 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(Lia) Coq(Arith.Arith) Coq(Arith.PeanoNat) Coq(Arith.EqNat) LF(Imp Maps)