proposition: Lemma eval_cnf_hyps : forall o l st (HL: Forall (has_literal (hconsmap st)) l) (WF: wf_state st) , (eval_result_state (cnf_hyps (is_classic o) l st) -> eval_ohformula o) -> (eval_state st -> Forall eval_literal l -> eval_ohformula o).
proof: Proof. unfold cnf_hyps. induction l ; simpl. - auto. - intros. inv H1. inv HL. specialize (eval_augment_hyp o a st H3 WF). assert (WFA: wf_result_state (augment_hyp (is_classic o) a st)). { apply wf_augment_hyp ; auto. } generalize (hconsmap_augment_hyp (is_classic o) a st). unfold hconsmap_progress. destruct (augment_hyp (is_classic o) a st). + simpl in *. tauto. + simpl. tauto. + simpl in *. intros. assert (HL : Forall (has_literal (hconsmap st0)) l). { revert H6. apply Forall_Forall. apply has_literal_mono; auto. intuition congruence. } specialize (IHl st0 HL). tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause