proposition: Lemma hcons_tauto_prover_correct : forall am mdec mbool n f (DEC: eqb_map is_dec_atomT mdec am = true ) (BOOL: eqb_map has_bool_atomT mbool am = true) (PROVER: hcons_tauto_prover (bool_of_ptrie_bool mdec) (bool_of_ptrie_bool mbool) n f = true), BForm.eval_hbformula (eval_prop am) f.
proof: Proof. intros am mdec mbool n f. intros. apply eqb_map_correct in DEC. apply eqb_map_correct in BOOL. apply BForm.to_hformula_correct with (has_bool := bool_of_ptrie_bool mbool). - intros. apply has_bool_correct. rewrite <- H. rewrite BOOL. change (has_bool am i = bool_of_ptrie_bool (map_bool_of_ptrie has_bool_atomT am) i). apply map_bool_of_ptrie_correct. - unfold hcons_tauto_prover in PROVER. apply hcons_prover_correct with (eval_atom := eval_prop am IsProp) in PROVER. rewrite eval_hformula_hlform in PROVER. auto. + intros. apply is_dec_correct. rewrite <- H. rewrite DEC. change (eval_is_dec am a = bool_of_ptrie_bool (map_bool_of_ptrie is_dec_atomT am) a). apply map_bool_of_ptrie_correct. + apply empty_thy. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause