proposition: Lemma BDDor_1_lemma_zero_2 : forall (cfg : BDDconfig) (memo : BDDor_memo) (node2 : ad) (bound : nat), BDDor_memo_lookup memo BDDzero node2 = None -> BDDor_1 cfg memo BDDzero node2 bound = (cfg, (node2, BDDor_memo_put memo BDDzero node2 node2)).
proof: Proof. intros cfg memo node2 bound H. elim bound. simpl in |- *. rewrite H. reflexivity. intros n H0. simpl in |- *. rewrite H. 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