proposition: Lemma checker_correct : Form.check_form t_form -> Atom.check_atom t_atom -> forall t_i t_func, let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form in Atom.wt t_i t_func t_atom -> forall s t confl, checker C.is_false s t confl -> ~ (S.valid rho s).
proof: Proof. unfold checker; intros H1 H2 t_i t_func rho H10; apply _checker__correct. intros c H; apply C.is_false_correct; auto with smtcoq_core. apply step_checker_correct; auto with smtcoq_core. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker