proposition: Lemma BDDor_1_lemma_internal_1 : forall (cfg : BDDconfig) (memo : BDDor_memo) (node1 node2 : ad) (bound bound' : nat), BDDor_memo_lookup memo node1 node2 = None -> BDDconfig_OK cfg -> is_internal_node cfg node1 -> is_internal_node cfg node2 -> max (nat_of_N (var cfg node1)) (nat_of_N (var cfg node2)) < bound -> bound = S bound' -> BDDcompare (var cfg node1) (var cfg node2) = Datatypes.Eq -> BDDor_1 cfg memo node1 node2 bound = (fst (BDDmake (fst (BDDor_1 (fst (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound')) (snd (snd (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound'))) (high cfg node1) (high cfg node2) bound')) (var cfg node1) (fst (snd (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound'))) (fst (snd (BDDor_1 (fst (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound')) (snd (snd (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound'))) (high cfg node1) (high cfg node2) bound')))), (snd (BDDmake (fst (BDDor_1 (fst (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound')) (snd (snd (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound'))) (high cfg node1) (high cfg node2) bound')) (var cfg node1) (fst (snd (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound'))) (fst (snd (BDDor_1 (fst (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound')) (snd (snd (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound'))) (high cfg node1) (high cfg node2) bound')))), BDDor_memo_put (snd (snd (BDDor_1 (fst (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound')) (snd (snd (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound'))) (high cfg node1) (high cfg node2) bound'))) node1 node2 (snd (BDDmake (fst (BDDor_1 (fst (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound')) (snd (snd (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound'))) (high cfg node1) (high cfg node2) bound')) (var cfg node1) (fst (snd (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound'))) (fst (snd (BDDor_1 (fst (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound')) (snd (snd (BDDor_1 cfg memo (low cfg node1) (low cfg node2) bound'))) (high cfg node1) (high cfg node2) bound'))))))).
proof: Proof. intros cfg memo node1 node2 bound bound' H H0 H1 H2 H3 H4 H5. rewrite H4. simpl in |- *. rewrite H. cut (N.eqb node1 BDDzero = false). cut (N.eqb node1 BDDone = false). cut (N.eqb node2 BDDzero = false). cut (N.eqb node2 BDDone = false). intros H6 H7 H8 H9. rewrite H6; rewrite H7; rewrite H8; rewrite H9; rewrite H5; reflexivity. apply not_true_is_false. unfold not in |- *. intro H6. cut (node2 = BDDone). intro H7. inversion H2. inversion H8. inversion H9. rewrite H7 in H10. rewrite (config_OK_one cfg H0) in H10; discriminate. apply Neqb_complete. assumption. apply not_true_is_false. unfold not in |- *; intro. cut (node2 = BDDzero). intro H7. inversion H2. inversion H8. inversion H9. rewrite H7 in H10. rewrite (config_OK_zero cfg H0) in H10; discriminate. apply Neqb_complete; assumption. apply not_true_is_false. unfold not in |- *; intro. cut (node1 = BDDone). intro H7. inversion H1. inversion H8. inversion H9. rewrite H7 in H10. rewrite (config_OK_one cfg H0) in H10; discriminate. apply Neqb_complete; assumption. apply not_true_is_false. unfold not in |- *; intro. cut (node1 = BDDzero). intro H7. inversion H1. inversion H8. inversion H9. rewrite H7 in H10. rewrite (config_OK_zero cfg H0) in H10; discriminate. apply Neqb_complete; 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