proposition: Lemma BDDor_1_internal : forall (cfg : BDDconfig) (memo : BDDor_memo) (node1 node2 : ad) (bound : nat), BDDconfig_OK cfg -> config_node_OK cfg node1 -> config_node_OK cfg node2 -> BDDor_memo_OK cfg memo -> is_internal_node (fst (BDDor_1 cfg memo node1 node2 bound)) (fst (snd (BDDor_1 cfg memo node1 node2 bound))) -> is_internal_node cfg node1 \/ is_internal_node cfg node2.
proof: Proof. intros cfg memo node1 node2 bound H H0 H1 H2 H3. elim H0; intro. elim H1; intro. rewrite H4 in H3. rewrite H5 in H3. elim (option_sum _ (BDDor_memo_lookup memo BDDzero BDDzero)). intro y. inversion y. rewrite (BDDor_1_lemma_1 cfg memo BDDzero BDDzero x bound H6) in H3. simpl in H3. unfold BDDor_memo_OK in H2. cut (bool_fun_eq (bool_fun_of_BDD cfg x) (bool_fun_or (bool_fun_of_BDD cfg BDDzero) (bool_fun_of_BDD cfg BDDzero))). intro H7. rewrite (proj1 (bool_fun_of_BDD_semantics cfg H)) in H7. cut (x = BDDzero). intro H8. inversion H3. inversion H9. inversion H10. rewrite H8 in H11. rewrite (config_OK_zero cfg H) in H11. discriminate. apply BDDunique with (cfg := cfg). assumption. right. right. unfold in_dom in |- *. inversion H3. inversion H8. inversion H9. rewrite H10. reflexivity. left; reflexivity. apply bool_fun_eq_trans with (bf2 := bool_fun_or bool_fun_zero bool_fun_zero). assumption. rewrite (proj1 (bool_fun_of_BDD_semantics cfg H)). unfold bool_fun_eq in |- *. reflexivity. exact (proj2 (proj2 (proj2 (proj2 (H2 BDDzero BDDzero x H6))))). intro y. rewrite (BDDor_1_lemma_zero_1 cfg memo BDDzero bound y) in H3. simpl in H3. inversion H3. inversion H6. inversion H7. rewrite (config_OK_zero cfg H) in H8. discriminate. elim H5; clear H5; intro. rewrite H4 in H3. rewrite H5 in H3. elim (option_sum _ (BDDor_memo_lookup memo BDDzero BDDone)). intro y. inversion y. rewrite (BDDor_1_lemma_1 cfg memo BDDzero BDDone x bound H6) in H3. simpl in H3. unfold BDDor_memo_OK in H2. cut (bool_fun_eq (bool_fun_of_BDD cfg x) (bool_fun_or (bool_fun_of_BDD cfg BDDzero) (bool_fun_of_BDD cfg BDDone))). intro H7. rewrite (proj1 (bool_fun_of_BDD_semantics cfg H)) in H7. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics cfg H))) in H7. cut (x = BDDone). intro H8. inversion H3. inversion H9. inversion H10. rewrite H8 in H11. rewrite (config_OK_one cfg H) in H11. discriminate. apply BDDunique with (cfg := cfg). assumption. right. right. unfold in_dom in |- *. inversion H3. inversion H8. inversion H9. rewrite H10. reflexivity. right; left; reflexivity. apply bool_fun_eq_trans with (bf2 := bool_fun_or bool_fun_zero bool_fun_one). assumption. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics cfg H))). unfold bool_fun_eq in |- *. reflexivity. exact (proj2 (proj2 (proj2 (proj2 (H2 BDDzero BDDone x H6))))). intro y. rewrite (BDDor_1_lemma_one_1 cfg memo BDDzero bound y) in H3. simpl in H3. inversion H3. inversion H6. inversion H7. rewrite (config_OK_one cfg H) in H8. discriminate. right. apply in_dom_is_internal. assumption. elim H4; clear H4; intro. rewrite H4 in H3. elim (option_sum _ (BDDor_memo_lookup memo BDDone node2)). intro y. inversion y. rewrite (BDDor_1_lemma_1 cfg memo BDDone node2 x bound H5) in H3. simpl in H3. unfold BDDor_memo_OK in H2. cut (x = BDDone). intro H6. rewrite H6 in H3. inversion H3. inversion H7. inversion H8. rewrite (config_OK_one cfg H) in H9. discriminate. apply BDDunique with (cfg := cfg). assumption. exact (proj1 (proj2 (proj2 (H2 BDDone node2 x H5)))). right; left; reflexivity. apply bool_fun_eq_trans with (bf2 := bool_fun_or (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg node2)). exact (proj2 (proj2 (proj2 (proj2 (H2 BDDone node2 x H5))))). rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics cfg H))). apply bool_fun_eq_trans with (bf2 := bool_fun_or (bool_fun_of_BDD cfg node2) bool_fun_one). apply bool_fun_or_commute. apply bool_fun_or_one. intro y. rewrite (BDDor_1_lemma_one_2 cfg memo node2 bound y) in H3. simpl in H3. inversion H3. inversion H5. inversion H6. rewrite (config_OK_one cfg H) in H7. discriminate. left. apply in_dom_is_internal. assumption. 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