proposition: Lemma is_tauto_is_complete : forall be : bool_expr, is_valid be -> is_tauto be = true.
proof: Proof. unfold is_tauto, is_valid in |- *. intros. elim (BDDof_bool_expr_correct be initBDDconfig initBDDneg_memo initBDDor_memo initBDDconfig_OK initBDDneg_memo_OK_2 initBDDor_memo_OK). intros. elim H1. intros. elim H3. intros. elim H5. intros. elim H7. intros. rewrite <- (BDDunique (fst (BDDof_bool_expr initBDDconfig initBDDneg_memo initBDDor_memo be)) H0 BDDone (fst (snd (BDDof_bool_expr initBDDconfig initBDDneg_memo initBDDor_memo be)))) . reflexivity. unfold config_node_OK in |- *. unfold node_OK in |- *. right. left. reflexivity. exact H2. apply bool_fun_eq_symm. apply bool_fun_eq_trans with (bf2 := bool_fun_of_bool_expr be). exact H9. apply bool_fun_eq_trans with (bf2 := bool_fun_one). exact H. apply bool_fun_eq_symm. exact (bool_fun_of_BDDone _ H0). Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1 bdd5_2 bdd6 bdd7 BDDdummy_lemma_2 BDDdummy_lemma_3 BDDdummy_lemma_4 bdd8 bdd9 bdd10 bdd11