proposition: Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_bf (Zeval_formula env) f.
proof: Proof. intros f w. unfold ZTautoChecker. apply (tauto_checker_sound _ _ _ _ eval_nformula). - apply Zeval_nformula_dec. - intros t ? env. unfold eval_nformula. unfold RingMicromega.eval_nformula. destruct t. apply (check_inconsistent_sound Zsor ZSORaddon) ; auto. - unfold Zdeduce. intros ? ? ? H **. revert H. apply (nformula_plus_nformula_correct Zsor ZSORaddon); auto. - intros ? ? ? ? H. rewrite normalise_correct in H. rewrite Zeval_formula_compat; auto. - intros ? ? ? ? H. rewrite negate_correct in H ; auto. rewrite Tauto.hold_eNOT. rewrite Zeval_formula_compat; auto. - intros t w0. unfold eval_tt. intros H env. rewrite (make_impl_map (eval_nformula env)). + eapply ZChecker_sound; eauto. + tauto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat