proposition: Lemma BDDvar_make_is_var : forall (cfg : BDDconfig) (x : BDDvar), BDDconfig_OK cfg -> bool_fun_eq (bool_fun_of_BDD (fst (BDDvar_make cfg x)) (snd (BDDvar_make cfg x))) (bool_fun_var x).
proof: Proof. intros. apply bool_fun_eq_trans with (bf2 := bool_fun_if x bool_fun_one bool_fun_zero). unfold BDDvar_make in |- *. apply bool_fun_eq_trans with (bool_fun_if x (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg BDDzero)). apply BDDmake_bool_fun. assumption. left; reflexivity. right; left; reflexivity. intro. inversion H0. inversion H1. inversion H2. rewrite (config_OK_zero cfg H) in H3; discriminate. intro. inversion H0. inversion H1. inversion H2. rewrite (config_OK_one cfg H) in H3; discriminate. apply bool_fun_if_preserves_eq. apply bool_fun_of_BDDone. assumption. apply bool_fun_of_BDDzero. assumption. unfold bool_fun_eq, bool_fun_one, bool_fun_zero, bool_fun_var, bool_fun_if in |- *. unfold bool_fun_eval in |- *. intro. elim (vb x). reflexivity. reflexivity. 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