proposition: Lemma BDDneg_keeps_neg_memo_OK : forall (cfg : BDDconfig) (negm : BDDneg_memo) (node : ad), BDDconfig_OK cfg -> BDDneg_memo_OK_2 cfg negm -> config_node_OK cfg node -> BDDneg_memo_OK_2 (fst (BDDneg cfg negm node)) (snd (snd (BDDneg cfg negm node))).
proof: Proof. intros. unfold BDDneg in |- *. elim (prod_sum _ _ (BDDneg_1_1 cfg negm node (S (nat_of_N (var cfg node))))). intro. elim x; clear x. intros cfg' node'. intro. elim H2; clear H2. intros negm' H2. rewrite H2. simpl in |- *. rewrite (BDDneg_1_1_eq_1 (S (nat_of_N (var cfg node))) cfg negm node) in H2. cut (is_internal_node cfg node -> nat_of_N (var cfg node) < S (nat_of_N (var cfg node))). intro. replace cfg' with (fst (fst (BDDneg_1 (cfg, node, negm) (S (nat_of_N (var cfg node)))))). replace negm' with (snd (BDDneg_1 (cfg, node, negm) (S (nat_of_N (var cfg node))))). refine (proj2 (BDDneg_1_lemma' _ _ _ _ _ _)). assumption. assumption. assumption. assumption. rewrite H2; reflexivity. rewrite H2; reflexivity. intro. 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