fact: Fixpoint ceval_fun_no_while (st : state) (c : com) : state := match c with | SKIP => st | x ::= a1 => t_update st x (aeval st a1) | c1 ;; c2 => let st' := ceval_fun_no_while st c1 in ceval_fun_no_while st' c2 | IFB b THEN c1 ELSE c2 FI => if (beval st b) then ceval_fun_no_while st c1 else ceval_fun_no_while st c2 | WHILE b DO c END => st end.
imports: Coq.Bool.Bool Coq.Arith.Arith Coq.Arith.EqNat Coq.omega.Omega Coq.Lists.List Coq.omega.Omega Maps