proposition: Lemma nodes_preserved_orm_OK : forall (cfg cfg' : BDDconfig) (orm : BDDor_memo), BDDconfig_OK cfg -> BDDconfig_OK cfg' -> nodes_preserved cfg cfg' -> BDDor_memo_OK cfg orm -> BDDor_memo_OK cfg' orm.
proof: Proof. intros. unfold BDDor_memo_OK in |- *. intros. unfold BDDor_memo_OK in H2. cut (config_node_OK cfg node1). cut (config_node_OK cfg node2). cut (config_node_OK cfg node). intros. cut (BDDvar_le (var cfg node) (BDDvar_max (var cfg node1) (var cfg node2)) = true). intro. cut (bool_fun_eq (bool_fun_of_BDD cfg node) (bool_fun_or (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2))). intro. split. apply nodes_preserved_2 with (cfg := cfg). assumption. assumption. split. apply nodes_preserved_2 with (cfg := cfg). assumption. assumption. split. apply nodes_preserved_2 with (cfg := cfg). assumption. assumption. split. cut (var cfg' node = var cfg node). cut (var cfg' node1 = var cfg node1). cut (var cfg' node2 = var cfg node2). intros. rewrite H9. rewrite H10. rewrite H11. assumption. apply nodes_preserved_var_1. assumption. assumption. assumption. assumption. apply nodes_preserved_var_1. assumption. assumption. assumption. assumption. apply nodes_preserved_var_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_or (bool_fun_of_BDD cfg node1) (bool_fun_of_BDD cfg node2)). assumption. apply bool_fun_eq_symm. apply bool_fun_or_preserves_eq. apply nodes_preserved_3. assumption. assumption. assumption. assumption. apply nodes_preserved_3. assumption. assumption. assumption. assumption. exact (proj2 (proj2 (proj2 (proj2 (H2 node1 node2 node H3))))). exact (proj1 (proj2 (proj2 (proj2 (H2 node1 node2 node H3))))). exact (proj1 (proj2 (proj2 (H2 node1 node2 node H3)))). exact (proj1 (proj2 (H2 node1 node2 node H3))). exact (proj1 (H2 node1 node2 node H3)). 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