proposition: Lemma BDDneg_2_config_OK_lemma_2 : forall (cfg : BDDconfig) (node : ad) (x : BDDvar) (l r : ad) (n m : nat), BDDconfig_OK cfg -> MapGet _ (fst cfg) node = Some (x, (l, r)) -> nat_of_N (var cfg node) < n -> n = S m -> BDDconfig_OK (fst (BDDneg_2 (fst (BDDneg_2 cfg l m)) r m)).
proof: Proof. intro cfg. elim cfg; clear cfg. intros bs y. elim y; clear y; intros share counter. intros node x l r n m H H0 H1 H2. cut (is_internal_node (bs, (share, counter)) node -> nat_of_N (var (bs, (share, counter)) node) < n). intro H3. cut (BDDconfig_OK (fst (BDDneg_2 (bs, (share, counter)) l m)) /\ (forall (x0 : BDDvar) (l0 r0 a : ad), MapGet _ (fst (bs, (share, counter))) a = Some (x0, (l0, r0)) -> MapGet _ (fst (fst (BDDneg_2 (bs, (share, counter)) l m))) a = Some (x0, (l0, r0))) /\ (is_internal_node (bs, (share, counter)) l -> is_internal_node (fst (BDDneg_2 (bs, (share, counter)) l m)) (snd (BDDneg_2 (bs, (share, counter)) l m)) /\ var (bs, (share, counter)) l = var (fst (BDDneg_2 (bs, (share, counter)) l m)) (snd (BDDneg_2 (bs, (share, counter)) l m))) /\ config_node_OK (fst (BDDneg_2 (bs, (share, counter)) l m)) (snd (BDDneg_2 (bs, (share, counter)) l m)) /\ bool_fun_eq (bool_fun_of_BDD (fst (BDDneg_2 (bs, (share, counter)) l m)) (snd (BDDneg_2 (bs, (share, counter)) l m))) (bool_fun_neg (bool_fun_of_BDD (bs, (share, counter)) l))). intro H4. elim H4; clear H4; intros. elim H5; clear H5; intros. elim H6; clear H6; intros. elim H7; clear H7; intros. cut (is_internal_node (fst (BDDneg_2 (bs, (share, counter)) l m)) r -> nat_of_N (var (fst (BDDneg_2 (bs, (share, counter)) l m)) r) < m). intro H9. cut (config_node_OK (fst (BDDneg_2 (bs, (share, counter)) l m)) r). intro H10. exact (proj1 (BDDneg_2_lemma m (fst (BDDneg_2 (bs, (share, counter)) l m)) r H4 H10 H9)). apply nodes_preserved_2 with (cfg := (bs, (share, counter))). cut (r = high (bs, (share, counter)) node). intro H10. rewrite H10. apply high_OK. assumption. split with x; split with l; split with r; assumption. unfold high in |- *. rewrite H0. reflexivity. unfold nodes_preserved in |- *. assumption. intro H9. cut (config_node_OK (bs, (share, counter)) (high (bs, (share, counter)) node)). intro H10. unfold high in H10. rewrite H0 in H10. elim H10. intro H11. inversion H9. inversion H12. inversion H13. rewrite H11 in H14. rewrite (config_OK_zero (fst (BDDneg_2 (bs, (share, counter)) l m)) H4) in H14; discriminate. intro H11. elim H11; intro. inversion H9. inversion H13. inversion H14. rewrite H12 in H15. rewrite (config_OK_one (fst (BDDneg_2 (bs, (share, counter)) l m)) H4) in H15; discriminate. elim (option_sum _ (MapGet _ (fst (bs, (share, counter))) r)). intro y. elim y. intro x0. elim x0. intro y0. intro y1. elim y1. intros y2 y3 y4. cut (var (fst (BDDneg_2 (bs, (share, counter)) l m)) r = var (bs, (share, counter)) r). intro H13. rewrite H13. apply lt_trans_1 with (y := nat_of_N (var (bs, (share, counter)) node)). replace r with (high (bs, (share, counter)) node). apply BDDcompare_lt. apply BDDvar_ordered_high. assumption. split with x; split with l; split with r; assumption. unfold high in |- *. rewrite H0. split with y0; split with y2; split with y3; assumption. unfold high in |- *; rewrite H0; reflexivity. rewrite <- H2; assumption. unfold var in |- *. rewrite y4. rewrite (H5 y0 y2 y3 r y4). reflexivity. intro y. unfold in_dom in H12. rewrite y in H12; discriminate. apply high_OK. assumption. split with x; split with l; split with r; assumption. apply BDDneg_2_lemma. assumption. replace l with (low (bs, (share, counter)) node). apply low_OK. assumption. split with x; split with l; split with r; assumption. unfold low in |- *; rewrite H0; reflexivity. intro H4. apply lt_trans_1 with (y := nat_of_N (var (bs, (share, counter)) node)). apply BDDcompare_lt. replace l with (low (bs, (share, counter)) node). apply BDDvar_ordered_low. assumption. split with x. split with l. split with r. assumption. unfold low in |- *. rewrite H0. assumption. unfold low in |- *; rewrite H0; reflexivity. rewrite <- H2; assumption. intro; assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4