proposition: Lemma BDDor_1_1_eq_1 : forall (bound : nat) (cfg : BDDconfig) (memo : BDDor_memo) (node1 node2 : ad), BDDor_1_1 cfg memo node1 node2 bound = BDDor_1 cfg memo node1 node2 bound.
proof: Proof. simple induction bound. simpl in |- *. reflexivity. intros n H cfg memo node1 node2. simpl in |- *. elim (BDDcompare (var cfg node1) (var cfg node2)). cut (BDDor_1_1 cfg memo (low cfg node1) (low cfg node2) n = BDDor_1 cfg memo (low cfg node1) (low cfg node2) n). intro H0. rewrite H0. elim (BDDor_1 cfg memo (low cfg node1) (low cfg node2) n). intros y y0. elim y0; intros y1 y2. simpl in |- *. cut (BDDor_1_1 y y2 (high cfg node1) (high cfg node2) n = BDDor_1 y y2 (high cfg node1) (high cfg node2) n). intro H1. rewrite H1. elim (BDDor_1 y y2 (high cfg node1) (high cfg node2) n). intros y3 y4. elim y4; intros y5 y6. simpl in |- *. elim (BDDmake y3 (var cfg node1) y1 y5). simpl in |- *. reflexivity. apply H. apply H. cut (BDDor_1_1 cfg memo node1 (low cfg node2) n = BDDor_1 cfg memo node1 (low cfg node2) n). intro H0. rewrite H0. elim (BDDor_1 cfg memo node1 (low cfg node2) n). intros y y0. elim y0; intros y1 y2. simpl in |- *. cut (BDDor_1_1 y y2 node1 (high cfg node2) n = BDDor_1 y y2 node1 (high cfg node2) n). intro H1. rewrite H1. elim (BDDor_1 y y2 node1 (high cfg node2) n). intros y3 y4. elim y4; intros y5 y6. simpl in |- *. elim (BDDmake y3 (var cfg node2) y1 y5). simpl in |- *. reflexivity. apply H. apply H. cut (BDDor_1_1 cfg memo (low cfg node1) node2 n = BDDor_1 cfg memo (low cfg node1) node2 n). intro H0. rewrite H0. elim (BDDor_1 cfg memo (low cfg node1) node2 n). intros y y0. elim y0; intros y1 y2. simpl in |- *. cut (BDDor_1_1 y y2 (high cfg node1) node2 n = BDDor_1 y y2 (high cfg node1) node2 n). intro H1. rewrite H1. elim (BDDor_1 y y2 (high cfg node1) node2 n). intros y3 y4. elim y4; intros y5 y6. simpl in |- *. simpl in |- *. elim (BDDmake y3 (var cfg node1) y1 y5). simpl in |- *. reflexivity. apply H. apply H. 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