proposition: Lemma case_split_ann_correct : forall st g a cl m prf d (UPWF : wf_state st) (PRF : case_split_ann a cl st g = Success (m, prf, d)) (EVST : eval_state st -> (eval_or cl -> eval_ohformula g) -> eval_ohformula g) (EVA : eval_annot_state st -> (eval_pset (hconsmap st) a) -> (( eval_or cl -> eval_ohformula g) -> eval_ohformula g)) (AN : wf_pset (hconsmap st) a) (WFD : (has_conflict_clause (hconsmap st)) cl) (HF : has_oform (hconsmap st) g) , (eval_state st -> eval_annot_state st -> eval_ohformula g) /\ (eval_annot_state st -> eval_pset m d -> eval_ohformula g) /\ Forall eval_literal_list prf /\ hmap_order (hconsmap st) m /\ Forall (has_conflict_clause m) prf /\ wf_pset m d.
proof: Proof. unfold case_split_ann. intros. destruct (case_split cl st g) eqn:EQ; try congruence. inv PRF. unfold eval_annot in EVA. simpl in EVA. apply case_split_correct with (a:= a) in EQ; auto. destruct EQ as (PRF1 & PRF2 & PRF3 & PRF4 & PRF5 & PRF6). split_and; try tauto. - destruct b; auto. - intros EPA EPS. destruct b. tauto. assert (EA : eval_pset m a). { apply eval_pset_union in EPS. destruct EPS; auto. destruct AN;auto. destruct PRF6;auto. } assert (EA' : eval_pset (hconsmap st) a). { revert EA. apply eval_pset_mono; auto. } apply PRF2 ; auto. - destruct b ; auto. apply wf_pset_union. revert AN. apply wf_pset_mono; auto. revert PRF6. apply wf_pset_mono; auto with wf. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause