proposition: Lemma BDDiff_keeps_config_OK : forall (cfg : BDDconfig) (negm : BDDneg_memo) (orm : BDDor_memo) (node1 node2 : ad), BDDconfig_OK cfg -> BDDneg_memo_OK_2 cfg negm -> BDDor_memo_OK cfg orm -> config_node_OK cfg node1 -> config_node_OK cfg node2 -> BDDconfig_OK (fst (BDDiff cfg negm orm node1 node2)).
proof: Proof. intros. unfold BDDiff in |- *. elim (prod_sum _ _ (BDDimpl cfg negm orm node1 node2)). intros cfg' H4. elim H4; clear H4. intro. elim x; clear x. intros node1' y. elim y; clear y. intros negm' orm' H4. rewrite H4. elim (prod_sum _ _ (BDDimpl cfg' negm' orm' node2 node1)). intros cfg'' H5. elim H5; clear H5. intro. elim x; clear x. intros node2' y. elim y; clear y. intros negm'' orm'' H5. rewrite H5. cut (BDDconfig_OK cfg'). cut (config_node_OK cfg' node1'). cut (config_node_OK cfg' node1). cut (config_node_OK cfg' node2). cut (BDDneg_memo_OK_2 cfg' negm'). cut (BDDor_memo_OK cfg' orm'). intros. cut (BDDconfig_OK cfg''). cut (config_node_OK cfg'' node2'). cut (config_node_OK cfg'' node1'). cut (BDDneg_memo_OK_2 cfg'' negm''). cut (BDDor_memo_OK cfg'' orm''). intros. apply BDDand_keeps_config_OK. assumption. assumption. assumption. assumption. assumption. replace cfg'' with (fst (BDDimpl cfg' negm' orm' node2 node1)). replace orm'' with (snd (snd (snd (BDDimpl cfg' negm' orm' node2 node1)))). apply BDDimpl_keeps_or_memo_OK. assumption. assumption. assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDimpl cfg' negm' orm' node2 node1)). replace negm'' with (fst (snd (snd (BDDimpl cfg' negm' orm' node2 node1)))). apply BDDimpl_keeps_neg_memo_OK. assumption. assumption. assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDimpl cfg' negm' orm' node2 node1)). apply BDDimpl_keeps_node_OK. assumption. assumption. assumption. assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg'' with (fst (BDDimpl cfg' negm' orm' node2 node1)). replace node2' with (fst (snd (BDDimpl cfg' negm' orm' node2 node1))). apply BDDimpl_node_OK. assumption. assumption. assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDimpl cfg' negm' orm' node2 node1)). apply BDDimpl_keeps_config_OK. assumption. assumption. assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg' with (fst (BDDimpl cfg negm orm node1 node2)). replace orm' with (snd (snd (snd (BDDimpl cfg negm orm node1 node2)))). apply BDDimpl_keeps_or_memo_OK. assumption. assumption. assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDimpl cfg negm orm node1 node2)). replace negm' with (fst (snd (snd (BDDimpl cfg negm orm node1 node2)))). apply BDDimpl_keeps_neg_memo_OK. assumption. assumption. assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDimpl cfg negm orm node1 node2)). apply BDDimpl_keeps_node_OK. assumption. assumption. assumption. assumption. assumption. assumption. rewrite H4; reflexivity. replace cfg' with (fst (BDDimpl cfg negm orm node1 node2)). apply BDDimpl_keeps_node_OK. assumption. assumption. assumption. assumption. assumption. assumption. rewrite H4; reflexivity. replace cfg' with (fst (BDDimpl cfg negm orm node1 node2)). replace node1' with (fst (snd (BDDimpl cfg negm orm node1 node2))). apply BDDimpl_node_OK. assumption. assumption. assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDimpl cfg negm orm node1 node2)). apply BDDimpl_keeps_config_OK. assumption. assumption. assumption. assumption. assumption. rewrite H4; reflexivity. 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 bdd10