fact: Fixpoint ceval_step1 (st : state) (c : com) : state := match c with | <{ skip }> => st | <{ l := a1 }> => (l !-> aeval st a1 ; st) | <{ c1 ; c2 }> => let st' := ceval_step1 st c1 in ceval_step1 st' c2 | <{ if b then c1 else c2 end }> => if (beval st b) then ceval_step1 st c1 else ceval_step1 st c2 | <{ while b1 do c1 end }> => st end.
imports: Coq(Lia) Coq(Arith.Arith) Coq(Arith.PeanoNat) Coq(Arith.EqNat) LF(Imp Maps)