proposition: Lemma BDDimpl_keeps_neg_memo_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 -> BDDneg_memo_OK_2 (fst (BDDimpl cfg negm orm node1 node2)) (fst (snd (snd (BDDimpl cfg negm orm node1 node2)))).
proof: Proof. intros. unfold BDDimpl in |- *. elim (prod_sum _ _ (BDDneg cfg negm node1)). intros cfg' H4. elim H4; clear H4. intro. elim x; clear x. intros node1' negm' H4. rewrite H4. elim (prod_sum _ _ (BDDor cfg' orm node1' node2)). intros cfg'' H5. elim H5; clear H5. intro. elim x; clear x. intros node negm'' H5. rewrite H5. simpl in |- *. cut (BDDconfig_OK cfg'). 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. replace cfg'' with (fst (BDDor cfg' orm node1' node2)). apply BDDor_keeps_neg_memo_OK. assumption. assumption. assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg' with (fst (BDDneg cfg negm node1)). apply BDDneg_keeps_or_memo_OK. assumption. assumption. assumption. assumption. rewrite H4; reflexivity. replace cfg' with (fst (BDDneg cfg negm node1)). replace negm' with (snd (snd (BDDneg cfg negm node1))). apply BDDneg_keeps_neg_memo_OK. assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDneg cfg negm node1)). apply BDDneg_keeps_node_OK. assumption. assumption. assumption. assumption. rewrite H4; reflexivity. replace cfg' with (fst (BDDneg cfg negm node1)). replace node1' with (fst (snd (BDDneg cfg negm node1))). apply BDDneg_node_OK. assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDneg cfg negm node1)). apply BDDneg_keeps_config_OK. 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