proposition: Lemma wf_augment_clauses : forall st prf (WC : Forall (has_conflict_clause (hconsmap st)) prf) (WF : wf_state st) , wf_result_state (augment_clauses prf st).
proof: Proof. unfold augment_clauses. intros. revert WF. revert WC. change (has_conflict_clause (hconsmap st)) with ((fun st x => has_conflict_clause (hconsmap st) x) st). apply fold_update_correct. - unfold augment_with_clause. intros. assert (HO :hconsmap_result (Progress st') = hconsmap st0). { rewrite <- H. generalize (hconsmap_get_fresh_clause_id st0). destruct (get_fresh_clause_id st0) as (fr,st2). simpl. intros. rewrite <- H1. apply hconsmap_insert_normalised_clause. apply not_fail_insert_normalised_clause. } { revert H0. apply has_conflict_clause_mono; auto. simpl in HO. congruence. } - intros. apply wf_augment_with_clause; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause