proposition: Lemma eval_annot_augment_with_clause : forall cl st (WS: wf_state st) (HC: has_conflict_clause (hconsmap st) cl) (ES: eval_annot_state st) (EL: eval_literal_list cl), eval_annot_result_state (augment_with_clause cl st).
proof: Proof. unfold augment_with_clause. intros. assert (ES' := eval_annot_get_fresh_clause st ES). assert (WFS' := wf_get_fresh_clause_id st WS). assert (MS' := get_fresh_clause_id_mono st). assert (units st = units (snd (get_fresh_clause_id st))). { destruct st ; simpl; reflexivity. } destruct (get_fresh_clause_id st) as (i,st') ; simpl; intros. apply eval_annot_insert_normalised_clause; auto. - simpl in *. rewrite <- MS' in *. apply wf_make_clause; auto. destruct WFS';auto. auto with wf. - simpl in *. rewrite <- H. rewrite MS'. eapply eval_annot_make_clause with (m:= hconsmap st) ; eauto. destruct ES;auto. destruct WS ; auto. apply wf_pset_empty. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause