proposition: Lemma build_pexpr_atom_correct : forall a vm vm' pe, check_atom a Typ.TZ -> build_pexpr_atom_aux build_pexpr vm a = (vm',pe) -> wf_vmap vm -> wf_vmap vm' /\ (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ (forall p, (nat_of_P p < nat_of_P (fst vm))%nat -> nth_error (snd vm) (nat_of_P (fst vm - p) - 1) = nth_error (snd vm')(nat_of_P (fst vm' - p) - 1)) /\ bounded_pexpr (fst vm') pe /\ interp_atom a = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe).
proof: Proof. apply build_pexpr_atom_aux_correct';apply build_pexpr_correct. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz