proposition: Lemma BDDneg_memo_OK_1_lemma_1_2' : forall (cfg : BDDconfig) (x : BDDvar) (l r node : ad) (n m : nat) (memo : BDDneg_memo), BDDconfig_OK cfg -> MapGet _ (fst cfg) node = Some (x, (l, r)) -> nat_of_N (var cfg node) < n -> n = S m -> BDDneg_memo_OK_2 (fst (BDDneg_2 (fst (BDDneg_2 cfg l m)) r m)) memo -> BDDneg_memo_OK_2 (fst (BDDneg_2 cfg node n)) (BDDneg_memo_put memo node (snd (BDDneg_2 cfg node n))).
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y; elim y; clear y; intros share counter. intros x l r node n m memo H H0 H1. intro H3. intros H2. unfold BDDneg_memo_OK_2 in |- *. intros node0 node' bound H4 H5. unfold BDDneg_memo_put, BDDneg_memo_lookup in H4. rewrite (MapPut_semantics ad memo node (snd (BDDneg_2 (bs, (share, counter)) node n)) node0) in H4. elim (sumbool_of_bool (N.eqb node node0)). intro y. rewrite y in H4. injection H4; intros. cut (node = node0). intro H7. rewrite <- H7. rewrite <- H7 in H5. split. apply nodes_preserved_2 with (cfg := (bs, (share, counter))). right; right. unfold in_dom in |- *. rewrite H0. reflexivity. unfold nodes_preserved in |- *. cut (config_node_OK (bs, (share, counter)) node). cut (is_internal_node (bs, (share, counter)) node -> nat_of_N (var (bs, (share, counter)) node) < n). intros H8 H9. exact (proj1 (proj2 (BDDneg_2_lemma n (bs, (share, counter)) node H H9 H8))). intro; assumption. right; right. unfold in_dom in |- *. rewrite H0; reflexivity. apply BDDneg_memo_OK_1_lemma_1_1_1. cut (config_node_OK (bs, (share, counter)) node). intro H8. cut (is_internal_node (bs, (share, counter)) node -> nat_of_N (var (bs, (share, counter)) node) < n). intros H9. exact (proj1 (BDDneg_2_lemma n (bs, (share, counter)) node H H8 H9)). intro H9. assumption. right. right. unfold in_dom in |- *. rewrite H0. reflexivity. apply nodes_preserved_2 with (cfg := (bs, (share, counter))). right; right. unfold in_dom in |- *. rewrite H0. reflexivity. unfold nodes_preserved in |- *. cut (config_node_OK (bs, (share, counter)) node). cut (is_internal_node (bs, (share, counter)) node -> nat_of_N (var (bs, (share, counter)) node) < n). intros H8 H9. exact (proj1 (proj2 (BDDneg_2_lemma n (bs, (share, counter)) node H H9 H8))). intro; assumption. right; right. unfold in_dom in |- *. rewrite H0; reflexivity. rewrite <- H6. cut (config_node_OK (bs, (share, counter)) node). intro H8. cut (is_internal_node (bs, (share, counter)) node -> nat_of_N (var (bs, (share, counter)) node) < n). intros H9. exact (proj1 (proj2 (proj2 (proj2 (BDDneg_2_lemma n (bs, (share, counter)) node H H8 H9))))). intro; assumption. right; right. unfold in_dom in |- *. rewrite H0; reflexivity. assumption. rewrite <- H6. cut (config_node_OK (bs, (share, counter)) node). intro H8. cut (is_internal_node (bs, (share, counter)) node -> nat_of_N (var (bs, (share, counter)) node) < n). intro H9. apply bool_fun_eq_trans with (bf2 := bool_fun_neg (bool_fun_of_BDD (bs, (share, counter)) node)). exact (proj2 (proj2 (proj2 (proj2 (BDDneg_2_lemma n (bs, (share, counter)) node H H8 H9))))). apply bool_fun_eq_neg_1. apply bool_fun_eq_symm. apply bool_fun_preservation. assumption. exact (proj1 (BDDneg_2_lemma n (bs, (share, counter)) node H H8 H9)). exact (proj1 (proj2 (BDDneg_2_lemma n (bs, (share, counter)) node H H8 H9))). assumption. intro; assumption. right; right. unfold in_dom in |- *. rewrite H0. reflexivity. apply Neqb_complete. assumption. intro y. rewrite y in H4. unfold BDDneg_memo_OK_2 in H2. split. apply nodes_preserved_2 with (cfg := fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)). cut (is_internal_node (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0 -> nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0) < S (nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0))). intro H6. exact (proj1 (H2 node0 node' (S (nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0))) H4 H6)). intro H6. unfold lt in |- *. apply le_n. apply nodes_preserved_1 with (n := n) (x := x). assumption. assumption. assumption. assumption. apply BDDneg_memo_OK_1_lemma_1_1_1. cut (config_node_OK (bs, (share, counter)) node). intro H6. cut (is_internal_node (bs, (share, counter)) node -> nat_of_N (var (bs, (share, counter)) node) < n). intro H7. exact (proj1 (BDDneg_2_lemma n (bs, (share, counter)) node H H6 H7)). intro H7. assumption. right. right. unfold in_dom in |- *. rewrite H0. reflexivity. apply nodes_preserved_2 with (cfg := fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)). cut (is_internal_node (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0 -> nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0) < S (nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0))). intro H6. exact (proj1 (H2 node0 node' (S (nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0))) H4 H6)). intro H6. unfold lt in |- *. apply le_n. apply nodes_preserved_1 with (n := n) (x := x). assumption. assumption. assumption. assumption. cut (config_node_OK (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node'). intro H6. cut (nodes_preserved (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) (fst (BDDneg_2 (bs, (share, counter)) node n))). intro H7. apply nodes_preserved_2 with (cfg := fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)). assumption. assumption. apply nodes_preserved_1 with (x := x). assumption. assumption. assumption. assumption. apply BDDneg_memo_OK_lemma_1_4' with (memo := memo) (node := node0). apply BDDneg_2_config_OK_lemma_2 with (n := n) (x := x) (node := node). assumption. assumption. assumption. assumption. assumption. cut (is_internal_node (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0 -> nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0) < S (nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0))). intro H6. exact (proj1 (H2 node0 node' (S (nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0))) H4 H6)). intro H6. unfold lt in |- *. apply le_n. assumption. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node'). apply bool_fun_preservation. apply BDDneg_2_config_OK_lemma_2 with (node := node) (x := x) (n := n). assumption. assumption. assumption. assumption. cut (config_node_OK (bs, (share, counter)) node). intro H6. cut (is_internal_node (bs, (share, counter)) node -> nat_of_N (var (bs, (share, counter)) node) < n). intro H7. exact (proj1 (BDDneg_2_lemma n (bs, (share, counter)) node H H6 H7)). intro; assumption. right; right. unfold in_dom in |- *. rewrite H0. reflexivity. cut (nodes_preserved (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) (fst (BDDneg_2 (bs, (share, counter)) node n))). unfold nodes_preserved in |- *. intro H6. assumption. apply nodes_preserved_1 with (x := x). assumption. assumption. assumption. assumption. apply BDDneg_memo_OK_lemma_1_4' with (memo := memo) (node := node0). apply BDDneg_2_config_OK_lemma_2 with (node := node) (x := x) (n := n). assumption. assumption. assumption. assumption. assumption. cut (is_internal_node (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0 -> nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0) < S (nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0))). intro H6. exact (proj1 (H2 node0 node' (S (nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0))) H4 H6)). intro H6. unfold lt in |- *. apply le_n. assumption. apply bool_fun_eq_trans with (bf2 := bool_fun_neg (bool_fun_of_BDD (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0)). apply BDDneg_memo_OK_bool_fun_1' with (memo := memo). apply BDDneg_2_config_OK_lemma_2 with (node := node) (x := x) (n := n). assumption. assumption. assumption. assumption. assumption. cut (is_internal_node (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0 -> nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0) < S (nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0))). intro H6. exact (proj1 (H2 node0 node' (S (nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0))) H4 H6)). intro H6. unfold lt in |- *. apply le_n. assumption. apply bool_fun_eq_neg_1. apply bool_fun_eq_symm. apply bool_fun_preservation. apply BDDneg_2_config_OK_lemma_2 with (n := n) (x := x) (node := node). assumption. assumption. assumption. assumption. cut (config_node_OK (bs, (share, counter)) node). intro H6. cut (is_internal_node (bs, (share, counter)) node -> nat_of_N (var (bs, (share, counter)) node) < n). intro H7. exact (proj1 (BDDneg_2_lemma n (bs, (share, counter)) node H H6 H7)). intro; assumption. right; right. unfold in_dom in |- *. rewrite H0. reflexivity. cut (nodes_preserved (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) (fst (BDDneg_2 (bs, (share, counter)) node n))). unfold nodes_preserved in |- *. intro H6. assumption. apply nodes_preserved_1 with (x := x). assumption. assumption. assumption. assumption. cut (is_internal_node (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0 -> nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0) < S (nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0))). intro H6. exact (proj1 (H2 node0 node' (S (nat_of_N (var (fst (BDDneg_2 (fst (BDDneg_2 (bs, (share, counter)) l m)) r m)) node0))) H4 H6)). intro H6. unfold lt in |- *. apply le_n. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1