proposition: Lemma nodes_preserved_negm_OK : forall (cfg cfg' : BDDconfig) (negm : BDDneg_memo), BDDconfig_OK cfg -> BDDconfig_OK cfg' -> nodes_preserved cfg cfg' -> BDDneg_memo_OK_2 cfg negm -> BDDneg_memo_OK_2 cfg' negm.
proof: Proof. intros. unfold BDDneg_memo_OK_2 in |- *. unfold BDDneg_memo_OK_2 in H2. intros. cut (is_internal_node cfg node -> nat_of_N (var cfg node) < bound). intro. cut (config_node_OK cfg node). cut (BDDneg_2 cfg node bound = (cfg, node')). intros. cut (config_node_OK cfg node'). intro. cut (config_node_OK cfg' node). cut (config_node_OK cfg' node'). intros. split. assumption. apply BDDneg_memo_OK_1_lemma_1_1_1. assumption. assumption. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD cfg node'). apply nodes_preserved_3. assumption. assumption. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_neg (bool_fun_of_BDD cfg node)). replace (bool_fun_of_BDD cfg node') with (bool_fun_of_BDD (fst (BDDneg_2 cfg node bound)) (snd (BDDneg_2 cfg node bound))). refine (proj2 (proj2 (proj2 (proj2 (BDDneg_2_lemma _ _ _ _ _ _))))). assumption. assumption. assumption. rewrite H6. reflexivity. apply bool_fun_eq_symm. apply bool_fun_eq_neg_1. apply nodes_preserved_3. assumption. assumption. assumption. assumption. apply nodes_preserved_2 with (cfg := cfg). assumption. assumption. apply nodes_preserved_2 with (cfg := cfg). assumption. assumption. replace cfg with (fst (BDDneg_2 cfg node bound)). replace node' with (snd (BDDneg_2 cfg node bound)). refine (proj1 (proj2 (proj2 (proj2 (BDDneg_2_lemma _ _ _ _ _ _))))). assumption. assumption. assumption. rewrite H6; reflexivity. rewrite H6; reflexivity. exact (proj2 (H2 node node' bound H3 H5)). exact (proj1 (H2 node node' bound H3 H5)). intro. cut (var cfg' node = var cfg node). intro. rewrite <- H6. apply H4. inversion H5. inversion H7. inversion H8. split with x. split with x0. split with x1. apply H1. assumption. apply nodes_preserved_var. assumption. 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 bdd7 BDDdummy_lemma_2 BDDdummy_lemma_3 BDDdummy_lemma_4 bdd8 bdd9