proposition: Lemma BDDor_node_OK : forall (cfg : BDDconfig) (orm : BDDor_memo) (node1 node2 : ad), BDDconfig_OK cfg -> BDDor_memo_OK cfg orm -> config_node_OK cfg node1 -> config_node_OK cfg node2 -> config_node_OK (fst (BDDor cfg orm node1 node2)) (fst (snd (BDDor cfg orm node1 node2))).
proof: Proof. intros. unfold BDDor in |- *. rewrite (BDDor_1_1_eq_1 (S (max (nat_of_N (var cfg node1)) (nat_of_N (var cfg node2)))) cfg orm node1 node2). cut (is_internal_node cfg node1 -> is_internal_node cfg node2 -> max (nat_of_N (var cfg node1)) (nat_of_N (var cfg node2)) < S (max (nat_of_N (var cfg node1)) (nat_of_N (var cfg node2)))). intros. refine (proj1 (proj2 (proj2 (BDDor_1_lemma _ _ _ _ _ _ _ _ _ _)))). assumption. assumption. assumption. assumption. assumption. intros. unfold lt in |- *. apply le_n. 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 bdd9