proposition: Lemma set_hmap_correct : forall m st (LE: hmap_order (hconsmap st) m) (WF: wf_state st), (eval_state st -> eval_state (set_hmap m st)) /\ (eval_annot_state st -> eval_annot_state (set_hmap m st)) /\ wf_state (set_hmap m st) /\ (hconsmap (set_hmap m st) = m).
proof: Proof. intros. split_and; simpl; auto. - intro ES; destruct ES; constructor; simpl; auto. destruct WF. eapply eval_units_mono ; eauto. - intro ES; destruct ES; constructor; simpl; auto. + revert ev_an_stack0. apply ForallMono; auto. apply eval_annot_mono; auto. + apply forall_units_mono with (m':= m) in ev_an_units0; auto. unfold eval_annot_units. eapply forall_units_monoP; eauto. apply eval_annot_mono; auto. destruct WF;auto. + unfold eval_annot_clauses in *. revert ev_an_clauses0. apply WMap.Forall_mono; auto. apply eval_annot_mono. - destruct WF. constructor ; simpl; auto. + eapply wf_order; eauto. + revert wf_arrows0. apply Forall_Forall. intro. apply has_literal_mono; auto. + eapply wf_units_def_mono; eauto. + eapply wf_units_lit_mono; eauto. + revert wf_stack0. apply ForallMono; auto. apply check_annot_mono; auto. apply isMono_lift;auto. apply has_literal_mono. + revert wf_clauses0. apply has_clauses_mono; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause