proposition: Lemma BDDand_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 (BDDand cfg negm orm node1 node2)) (fst (snd (snd (BDDand cfg negm orm node1 node2)))).
proof: Proof. intros. unfold BDDand 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 _ _ (BDDneg cfg' negm' node2)). intros cfg'' H5. elim H5; clear H5. intro. elim x; clear x. intros node2' negm'' H5. rewrite H5. elim (prod_sum _ _ (BDDor cfg'' orm node1' node2')). intros cfg''' H6. elim H6; clear H6. intro. elim x; clear x. intros node orm' H6. rewrite H6. elim (prod_sum _ _ (BDDneg cfg''' negm'' node)). intros cfg'''' H7. elim H7; clear H7. intro. elim x; clear x. intros node' negm''' H7. rewrite H7. 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. 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. cut (BDDconfig_OK cfg'''). cut (config_node_OK cfg''' node). cut (BDDneg_memo_OK_2 cfg''' negm''). cut (BDDor_memo_OK cfg''' orm'). intros. replace cfg'''' with (fst (BDDneg cfg''' negm'' node)). replace negm''' with (snd (snd (BDDneg cfg''' negm'' node))). apply BDDneg_keeps_neg_memo_OK. assumption. assumption. assumption. rewrite H7; reflexivity. rewrite H7; reflexivity. replace cfg''' with (fst (BDDor cfg'' orm node1' node2')). replace orm' with (snd (snd (BDDor cfg'' orm node1' node2'))). apply BDDor_keeps_or_memo_OK. assumption. assumption. assumption. assumption. rewrite H6; reflexivity. rewrite H6; reflexivity. replace cfg''' with (fst (BDDor cfg'' orm node1' node2')). apply BDDor_keeps_neg_memo_OK. assumption. assumption. assumption. assumption. assumption. rewrite H6; reflexivity. replace cfg''' with (fst (BDDor cfg'' orm node1' node2')). replace node with (fst (snd (BDDor cfg'' orm node1' node2'))). apply BDDor_node_OK. assumption. assumption. assumption. assumption. rewrite H6; reflexivity. rewrite H6; reflexivity. replace cfg''' with (fst (BDDor cfg'' orm node1' node2')). apply BDDor_keeps_config_OK. assumption. assumption. assumption. assumption. rewrite H6; reflexivity. replace cfg'' with (fst (BDDneg cfg' negm' node2)). apply BDDneg_keeps_or_memo_OK. assumption. assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg'' with (fst (BDDneg cfg' negm' node2)). replace negm'' with (snd (snd (BDDneg cfg' negm' node2))). apply BDDneg_keeps_neg_memo_OK. assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDneg cfg' negm' node2)). apply BDDneg_keeps_node_OK. assumption. assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg'' with (fst (BDDneg cfg' negm' node2)). replace node2' with (fst (snd (BDDneg cfg' negm' node2))). apply BDDneg_node_OK. assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDneg cfg' negm' node2)). apply BDDneg_keeps_config_OK. 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