proposition: Lemma cnf_checker_correct : forall rho rhobv t_form, Form.check_form t_form -> forall s t confl, cnf_checker t_form C.is_false s t confl -> ~ (S.valid (Form.interp_state_var rho rhobv t_form) s).
proof: Proof. unfold cnf_checker; intros rho rhobv t_form Ht; apply _checker__correct. intros c H; apply C.is_false_correct; auto. apply step_checker_correct; auto. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker