proposition: Lemma BDDof_bool_expr_correct : forall (be : bool_expr) (cfg : BDDconfig) (negm : BDDneg_memo) (orm : BDDor_memo), BDDconfig_OK cfg -> BDDneg_memo_OK_2 cfg negm -> BDDor_memo_OK cfg orm -> BDDconfig_OK (fst (BDDof_bool_expr cfg negm orm be)) /\ config_node_OK (fst (BDDof_bool_expr cfg negm orm be)) (fst (snd (BDDof_bool_expr cfg negm orm be))) /\ BDDneg_memo_OK_2 (fst (BDDof_bool_expr cfg negm orm be)) (fst (snd (snd (BDDof_bool_expr cfg negm orm be)))) /\ BDDor_memo_OK (fst (BDDof_bool_expr cfg negm orm be)) (snd (snd (snd (BDDof_bool_expr cfg negm orm be)))) /\ nodes_preserved cfg (fst (BDDof_bool_expr cfg negm orm be)) /\ bool_fun_eq (bool_fun_of_BDD (fst (BDDof_bool_expr cfg negm orm be)) (fst (snd (BDDof_bool_expr cfg negm orm be)))) (bool_fun_of_bool_expr be).
proof: Proof. simple induction be. intros. simpl in |- *. split. assumption. split. left; reflexivity. split. assumption. split. assumption. split. unfold nodes_preserved in |- *. intros. assumption. apply bool_fun_of_BDDzero. assumption. simpl in |- *. split. assumption. split. right; left; reflexivity. split. assumption. split. assumption. split. unfold nodes_preserved in |- *. intros; assumption. apply bool_fun_of_BDDone. assumption. simpl in |- *. intros. elim (prod_sum _ _ (BDDvar_make cfg b)). intros cfg' H2. elim H2; clear H2. intros node H2. rewrite H2. simpl in |- *. split. replace cfg' with (fst (BDDvar_make cfg b)). apply BDDvar_make_keeps_config_OK. assumption. rewrite H2; reflexivity. split. replace cfg' with (fst (BDDvar_make cfg b)). replace node with (snd (BDDvar_make cfg b)). apply BDDvar_make_node_OK. assumption. rewrite H2; reflexivity. rewrite H2; reflexivity. split. replace cfg' with (fst (BDDvar_make cfg b)). apply BDDvar_make_keeps_neg_memo_OK. assumption. assumption. rewrite H2; reflexivity. split. replace cfg' with (fst (BDDvar_make cfg b)). apply BDDvar_make_keeps_or_memo_OK. assumption. assumption. rewrite H2; reflexivity. split. replace cfg' with (fst (BDDvar_make cfg b)). apply BDDvar_make_preserves_nodes. assumption. rewrite H2; reflexivity. replace cfg' with (fst (BDDvar_make cfg b)). replace node with (snd (BDDvar_make cfg b)). apply BDDvar_make_is_var. assumption. rewrite H2; reflexivity. rewrite H2; reflexivity. intros. simpl in |- *. elim (prod_sum _ _ (BDDof_bool_expr cfg negm orm b)). intros cfg' H3. elim H3; clear H3. intro. elim x; clear x. intros node y. elim y; clear y. intros negm' orm' H3. rewrite H3. elim (prod_sum _ _ (BDDneg cfg' negm' node)). intros cfg'' H4. elim H4; clear H4. intro. elim x; clear x. intros node' negm''. intro H4. rewrite H4. simpl in |- *. cut (BDDconfig_OK cfg'). cut (config_node_OK cfg' node). cut (BDDneg_memo_OK_2 cfg' negm'). cut (BDDor_memo_OK cfg' orm'). cut (nodes_preserved cfg cfg'). cut (bool_fun_eq (bool_fun_of_BDD cfg' node) (bool_fun_of_bool_expr b)). intros. split. replace cfg'' with (fst (BDDneg cfg' negm' node)). apply BDDneg_keeps_config_OK. assumption. assumption. assumption. rewrite H4; reflexivity. split. replace cfg'' with (fst (BDDneg cfg' negm' node)). replace node' with (fst (snd (BDDneg cfg' negm' node))). apply BDDneg_node_OK. assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. split. 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 H4; reflexivity. rewrite H4; reflexivity. split. replace cfg'' with (fst (BDDneg cfg' negm' node)). apply BDDneg_keeps_or_memo_OK. assumption. assumption. assumption. assumption. rewrite H4; reflexivity. split. apply nodes_preserved_trans with (cfg2 := cfg'). assumption. replace cfg'' with (fst (BDDneg cfg' negm' node)). apply BDDneg_preserves_nodes. assumption. assumption. assumption. rewrite H4; reflexivity. apply bool_fun_eq_trans with (bf2 := bool_fun_neg (bool_fun_of_BDD cfg' node)). replace cfg'' with (fst (BDDneg cfg' negm' node)). replace node' with (fst (snd (BDDneg cfg' negm' node))). apply BDDneg_is_neg. assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. apply bool_fun_eq_neg_1. assumption. replace cfg' with (fst (BDDof_bool_expr cfg negm orm b)). replace node with (fst (snd (BDDof_bool_expr cfg negm orm b))). refine (proj2 (proj2 (proj2 (proj2 (proj2 (H _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H3; reflexivity. rewrite H3; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm b)). refine (proj1 (proj2 (proj2 (proj2 (proj2 (H _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H3; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm b)). replace orm' with (snd (snd (snd (BDDof_bool_expr cfg negm orm b)))). refine (proj1 (proj2 (proj2 (proj2 (H _ _ _ _ _ _))))). assumption. assumption. assumption. rewrite H3; reflexivity. rewrite H3; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm b)). replace negm' with (fst (snd (snd (BDDof_bool_expr cfg negm orm b)))). refine (proj1 (proj2 (proj2 (H _ _ _ _ _ _)))). assumption. assumption. assumption. rewrite H3; reflexivity. rewrite H3; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm b)). replace node with (fst (snd (BDDof_bool_expr cfg negm orm b))). refine (proj1 (proj2 (H _ _ _ _ _ _))). assumption. assumption. assumption. rewrite H3; reflexivity. rewrite H3; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm b)). refine (proj1 (H _ _ _ _ _ _)). assumption. assumption. assumption. rewrite H3; reflexivity. clear be. intros be1 H. intros be2 H0. intros. simpl in |- *. elim (prod_sum _ _ (BDDof_bool_expr cfg negm orm be1)). 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 _ _ (BDDof_bool_expr cfg' negm' orm' be2)). 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. 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. simpl in |- *. cut (BDDconfig_OK cfg'). cut (config_node_OK cfg' node1). cut (BDDneg_memo_OK_2 cfg' negm'). cut (BDDor_memo_OK cfg' orm'). cut (nodes_preserved cfg cfg'). cut (bool_fun_eq (bool_fun_of_BDD cfg' node1) (bool_fun_of_bool_expr be1)). intros. cut (BDDconfig_OK cfg''). cut (config_node_OK cfg'' node2). cut (BDDneg_memo_OK_2 cfg'' negm''). cut (BDDor_memo_OK cfg'' orm''). cut (nodes_preserved cfg' cfg''). cut (bool_fun_eq (bool_fun_of_BDD cfg'' node2) (bool_fun_of_bool_expr be2)). intros. cut (config_node_OK cfg'' node1). intros. split. replace cfg''' with (fst (BDDor cfg'' orm'' node1 node2)). apply BDDor_keeps_config_OK. assumption. assumption. assumption. assumption. rewrite H6; reflexivity. split. 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. split. replace cfg''' with (fst (BDDor cfg'' orm'' node1 node2)). apply BDDor_keeps_neg_memo_OK. assumption. assumption. assumption. assumption. assumption. rewrite H6; reflexivity. split. 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. split. apply nodes_preserved_trans with (cfg2 := cfg'). assumption. apply nodes_preserved_trans with (cfg2 := cfg''). assumption. replace cfg''' with (fst (BDDor cfg'' orm'' node1 node2)). apply BDDor_preserves_nodes. assumption. assumption. assumption. assumption. rewrite H6; reflexivity. apply bool_fun_eq_trans with (bf2 := bool_fun_or (bool_fun_of_BDD cfg'' node1) (bool_fun_of_BDD cfg'' node2)). replace cfg''' with (fst (BDDor cfg'' orm'' node1 node2)). replace node with (fst (snd (BDDor cfg'' orm'' node1 node2))). apply BDDor_is_or. assumption. assumption. assumption. assumption. rewrite H6; reflexivity. rewrite H6; reflexivity. apply bool_fun_or_preserves_eq. apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD cfg' node1). apply nodes_preserved_3. assumption. assumption. assumption. assumption. assumption. assumption. apply nodes_preserved_2 with (cfg := cfg'). assumption. assumption. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace node2 with (fst (snd (BDDof_bool_expr cfg' negm' orm' be2))). refine (proj2 (proj2 (proj2 (proj2 (proj2 (H0 _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). refine (proj1 (proj2 (proj2 (proj2 (proj2 (H0 _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace orm'' with (snd (snd (snd (BDDof_bool_expr cfg' negm' orm' be2)))). refine (proj1 (proj2 (proj2 (proj2 (H0 _ _ _ _ _ _))))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace negm'' with (fst (snd (snd (BDDof_bool_expr cfg' negm' orm' be2)))). refine (proj1 (proj2 (proj2 (H0 _ _ _ _ _ _)))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace node2 with (fst (snd (BDDof_bool_expr cfg' negm' orm' be2))). refine (proj1 (proj2 (H0 _ _ _ _ _ _))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). refine (proj1 (H0 _ _ _ _ _ _)). assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace node1 with (fst (snd (BDDof_bool_expr cfg negm orm be1))). refine (proj2 (proj2 (proj2 (proj2 (proj2 (H _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). refine (proj1 (proj2 (proj2 (proj2 (proj2 (H _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace orm' with (snd (snd (snd (BDDof_bool_expr cfg negm orm be1)))). refine (proj1 (proj2 (proj2 (proj2 (H _ _ _ _ _ _))))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace negm' with (fst (snd (snd (BDDof_bool_expr cfg negm orm be1)))). refine (proj1 (proj2 (proj2 (H _ _ _ _ _ _)))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace node1 with (fst (snd (BDDof_bool_expr cfg negm orm be1))). refine (proj1 (proj2 (H _ _ _ _ _ _))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). refine (proj1 (H _ _ _ _ _ _)). assumption. assumption. assumption. rewrite H4; reflexivity. clear be. intros be1 H. intros be2 H0. intros. simpl in |- *. elim (prod_sum _ _ (BDDof_bool_expr cfg negm orm be1)). 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 _ _ (BDDof_bool_expr cfg' negm' orm' be2)). 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 (BDDneg_memo_OK_2 cfg' negm'). cut (BDDor_memo_OK cfg' orm'). cut (nodes_preserved cfg cfg'). cut (bool_fun_eq (bool_fun_of_BDD cfg' node1) (bool_fun_of_bool_expr be1)). intros. cut (BDDconfig_OK cfg''). cut (config_node_OK cfg'' node2). cut (BDDneg_memo_OK_2 cfg'' negm''). cut (BDDor_memo_OK cfg'' orm''). cut (nodes_preserved cfg' cfg''). cut (bool_fun_eq (bool_fun_of_BDD cfg'' node2) (bool_fun_of_bool_expr be2)). intros. cut (config_node_OK cfg'' node1). intros. split. apply BDDand_keeps_config_OK. assumption. assumption. assumption. assumption. assumption. split. apply BDDand_node_OK. assumption. assumption. assumption. assumption. assumption. split. apply BDDand_keeps_neg_memo_OK. assumption. assumption. assumption. assumption. assumption. split. apply BDDand_keeps_or_memo_OK. assumption. assumption. assumption. assumption. assumption. split. apply nodes_preserved_trans with (cfg2 := cfg'). assumption. apply nodes_preserved_trans with (cfg2 := cfg''). assumption. apply BDDand_preserves_nodes. assumption. assumption. assumption. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_and (bool_fun_of_BDD cfg'' node1) (bool_fun_of_BDD cfg'' node2)). apply BDDand_is_and. assumption. assumption. assumption. assumption. assumption. apply bool_fun_and_preserves_eq. apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD cfg' node1). apply nodes_preserved_3. assumption. assumption. assumption. assumption. assumption. assumption. apply nodes_preserved_2 with (cfg := cfg'). assumption. assumption. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace node2 with (fst (snd (BDDof_bool_expr cfg' negm' orm' be2))). refine (proj2 (proj2 (proj2 (proj2 (proj2 (H0 _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). refine (proj1 (proj2 (proj2 (proj2 (proj2 (H0 _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace orm'' with (snd (snd (snd (BDDof_bool_expr cfg' negm' orm' be2)))). refine (proj1 (proj2 (proj2 (proj2 (H0 _ _ _ _ _ _))))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace negm'' with (fst (snd (snd (BDDof_bool_expr cfg' negm' orm' be2)))). refine (proj1 (proj2 (proj2 (H0 _ _ _ _ _ _)))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace node2 with (fst (snd (BDDof_bool_expr cfg' negm' orm' be2))). refine (proj1 (proj2 (H0 _ _ _ _ _ _))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). refine (proj1 (H0 _ _ _ _ _ _)). assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace node1 with (fst (snd (BDDof_bool_expr cfg negm orm be1))). refine (proj2 (proj2 (proj2 (proj2 (proj2 (H _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). refine (proj1 (proj2 (proj2 (proj2 (proj2 (H _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace orm' with (snd (snd (snd (BDDof_bool_expr cfg negm orm be1)))). refine (proj1 (proj2 (proj2 (proj2 (H _ _ _ _ _ _))))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace negm' with (fst (snd (snd (BDDof_bool_expr cfg negm orm be1)))). refine (proj1 (proj2 (proj2 (H _ _ _ _ _ _)))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace node1 with (fst (snd (BDDof_bool_expr cfg negm orm be1))). refine (proj1 (proj2 (H _ _ _ _ _ _))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). refine (proj1 (H _ _ _ _ _ _)). assumption. assumption. assumption. rewrite H4; reflexivity. clear be. intros be1 H. intros be2 H0. intros. simpl in |- *. elim (prod_sum _ _ (BDDof_bool_expr cfg negm orm be1)). 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 _ _ (BDDof_bool_expr cfg' negm' orm' be2)). 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 (BDDneg_memo_OK_2 cfg' negm'). cut (BDDor_memo_OK cfg' orm'). cut (nodes_preserved cfg cfg'). cut (bool_fun_eq (bool_fun_of_BDD cfg' node1) (bool_fun_of_bool_expr be1)). intros. cut (BDDconfig_OK cfg''). cut (config_node_OK cfg'' node2). cut (BDDneg_memo_OK_2 cfg'' negm''). cut (BDDor_memo_OK cfg'' orm''). cut (nodes_preserved cfg' cfg''). cut (bool_fun_eq (bool_fun_of_BDD cfg'' node2) (bool_fun_of_bool_expr be2)). intros. cut (config_node_OK cfg'' node1). intros. split. apply BDDimpl_keeps_config_OK. assumption. assumption. assumption. assumption. assumption. split. apply BDDimpl_node_OK. assumption. assumption. assumption. assumption. assumption. split. apply BDDimpl_keeps_neg_memo_OK. assumption. assumption. assumption. assumption. assumption. split. apply BDDimpl_keeps_or_memo_OK. assumption. assumption. assumption. assumption. assumption. split. apply nodes_preserved_trans with (cfg2 := cfg'). assumption. apply nodes_preserved_trans with (cfg2 := cfg''). assumption. apply BDDimpl_preserves_nodes. assumption. assumption. assumption. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_impl (bool_fun_of_BDD cfg'' node1) (bool_fun_of_BDD cfg'' node2)). apply BDDimpl_is_impl. assumption. assumption. assumption. assumption. assumption. apply bool_fun_impl_preserves_eq. apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD cfg' node1). apply nodes_preserved_3. assumption. assumption. assumption. assumption. assumption. assumption. apply nodes_preserved_2 with (cfg := cfg'). assumption. assumption. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace node2 with (fst (snd (BDDof_bool_expr cfg' negm' orm' be2))). refine (proj2 (proj2 (proj2 (proj2 (proj2 (H0 _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). refine (proj1 (proj2 (proj2 (proj2 (proj2 (H0 _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace orm'' with (snd (snd (snd (BDDof_bool_expr cfg' negm' orm' be2)))). refine (proj1 (proj2 (proj2 (proj2 (H0 _ _ _ _ _ _))))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace negm'' with (fst (snd (snd (BDDof_bool_expr cfg' negm' orm' be2)))). refine (proj1 (proj2 (proj2 (H0 _ _ _ _ _ _)))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace node2 with (fst (snd (BDDof_bool_expr cfg' negm' orm' be2))). refine (proj1 (proj2 (H0 _ _ _ _ _ _))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). refine (proj1 (H0 _ _ _ _ _ _)). assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace node1 with (fst (snd (BDDof_bool_expr cfg negm orm be1))). refine (proj2 (proj2 (proj2 (proj2 (proj2 (H _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). refine (proj1 (proj2 (proj2 (proj2 (proj2 (H _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace orm' with (snd (snd (snd (BDDof_bool_expr cfg negm orm be1)))). refine (proj1 (proj2 (proj2 (proj2 (H _ _ _ _ _ _))))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace negm' with (fst (snd (snd (BDDof_bool_expr cfg negm orm be1)))). refine (proj1 (proj2 (proj2 (H _ _ _ _ _ _)))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace node1 with (fst (snd (BDDof_bool_expr cfg negm orm be1))). refine (proj1 (proj2 (H _ _ _ _ _ _))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). refine (proj1 (H _ _ _ _ _ _)). assumption. assumption. assumption. rewrite H4; reflexivity. clear be. intros be1 H. intros be2 H0. intros. simpl in |- *. elim (prod_sum _ _ (BDDof_bool_expr cfg negm orm be1)). 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 _ _ (BDDof_bool_expr cfg' negm' orm' be2)). 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 (BDDneg_memo_OK_2 cfg' negm'). cut (BDDor_memo_OK cfg' orm'). cut (nodes_preserved cfg cfg'). cut (bool_fun_eq (bool_fun_of_BDD cfg' node1) (bool_fun_of_bool_expr be1)). intros. cut (BDDconfig_OK cfg''). cut (config_node_OK cfg'' node2). cut (BDDneg_memo_OK_2 cfg'' negm''). cut (BDDor_memo_OK cfg'' orm''). cut (nodes_preserved cfg' cfg''). cut (bool_fun_eq (bool_fun_of_BDD cfg'' node2) (bool_fun_of_bool_expr be2)). intros. cut (config_node_OK cfg'' node1). intros. split. apply BDDiff_keeps_config_OK. assumption. assumption. assumption. assumption. assumption. split. apply BDDiff_node_OK. assumption. assumption. assumption. assumption. assumption. split. apply BDDiff_keeps_neg_memo_OK. assumption. assumption. assumption. assumption. assumption. split. apply BDDiff_keeps_or_memo_OK. assumption. assumption. assumption. assumption. assumption. split. apply nodes_preserved_trans with (cfg2 := cfg'). assumption. apply nodes_preserved_trans with (cfg2 := cfg''). assumption. apply BDDiff_preserves_nodes. assumption. assumption. assumption. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_iff (bool_fun_of_BDD cfg'' node1) (bool_fun_of_BDD cfg'' node2)). apply BDDiff_is_iff. assumption. assumption. assumption. assumption. assumption. apply bool_fun_iff_preserves_eq. apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD cfg' node1). apply nodes_preserved_3. assumption. assumption. assumption. assumption. assumption. assumption. apply nodes_preserved_2 with (cfg := cfg'). assumption. assumption. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace node2 with (fst (snd (BDDof_bool_expr cfg' negm' orm' be2))). refine (proj2 (proj2 (proj2 (proj2 (proj2 (H0 _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). refine (proj1 (proj2 (proj2 (proj2 (proj2 (H0 _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace orm'' with (snd (snd (snd (BDDof_bool_expr cfg' negm' orm' be2)))). refine (proj1 (proj2 (proj2 (proj2 (H0 _ _ _ _ _ _))))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace negm'' with (fst (snd (snd (BDDof_bool_expr cfg' negm' orm' be2)))). refine (proj1 (proj2 (proj2 (H0 _ _ _ _ _ _)))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). replace node2 with (fst (snd (BDDof_bool_expr cfg' negm' orm' be2))). refine (proj1 (proj2 (H0 _ _ _ _ _ _))). assumption. assumption. assumption. rewrite H5; reflexivity. rewrite H5; reflexivity. replace cfg'' with (fst (BDDof_bool_expr cfg' negm' orm' be2)). refine (proj1 (H0 _ _ _ _ _ _)). assumption. assumption. assumption. rewrite H5; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace node1 with (fst (snd (BDDof_bool_expr cfg negm orm be1))). refine (proj2 (proj2 (proj2 (proj2 (proj2 (H _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). refine (proj1 (proj2 (proj2 (proj2 (proj2 (H _ _ _ _ _ _)))))). assumption. assumption. assumption. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace orm' with (snd (snd (snd (BDDof_bool_expr cfg negm orm be1)))). refine (proj1 (proj2 (proj2 (proj2 (H _ _ _ _ _ _))))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace negm' with (fst (snd (snd (BDDof_bool_expr cfg negm orm be1)))). refine (proj1 (proj2 (proj2 (H _ _ _ _ _ _)))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). replace node1 with (fst (snd (BDDof_bool_expr cfg negm orm be1))). refine (proj1 (proj2 (H _ _ _ _ _ _))). assumption. assumption. assumption. rewrite H4; reflexivity. rewrite H4; reflexivity. replace cfg' with (fst (BDDof_bool_expr cfg negm orm be1)). refine (proj1 (H _ _ _ _ _ _)). 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