proposition: Lemma BDDor_1_lemma_one_1 : forall (cfg : BDDconfig) (memo : BDDor_memo) (node1 : ad) (bound : nat), BDDor_memo_lookup memo node1 BDDone = None -> BDDor_1 cfg memo node1 BDDone bound = (cfg, (BDDone, BDDor_memo_put memo node1 BDDone BDDone)).
proof: Proof. intros cfg memo node1 bound H. elim bound. simpl in |- *. rewrite H. elim (sumbool_of_bool (N.eqb node1 BDDzero)). intro y. rewrite y. cut (node1 = BDDzero). intro H0. rewrite H0; reflexivity. apply Neqb_complete. assumption. intro y. rewrite y. elim (sumbool_of_bool (N.eqb node1 BDDone)); intro y0. rewrite y0. cut (node1 = BDDone). intro H0. rewrite H0; reflexivity. apply Neqb_complete. assumption. rewrite y0. reflexivity. intros n H0. simpl in |- *. rewrite H. elim (sumbool_of_bool (N.eqb node1 BDDzero)). intro y. rewrite y. cut (node1 = BDDzero). intro H1. rewrite H1. reflexivity. apply Neqb_complete; assumption. intro y. rewrite y. elim (sumbool_of_bool (N.eqb node1 BDDone)). intro y0. rewrite y0. cut (node1 = BDDone). intro H1. rewrite H1. reflexivity. apply Neqb_complete. assumption. intro y0. rewrite y0. 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