proposition: Lemma BDDneg_memo_OK_lemma_1_4' : forall (cfg : BDDconfig) (memo : BDDneg_memo) (node node' : ad), BDDconfig_OK cfg -> BDDneg_memo_OK_2 cfg memo -> config_node_OK cfg node -> BDDneg_memo_lookup memo node = Some node' -> config_node_OK cfg node'.
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y; elim y; clear y; intros share counter. intros memo node node' H H0 H1 H2. unfold BDDneg_memo_OK_2 in H0. cut (config_node_OK (bs, (share, counter)) node /\ BDDneg_2 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node))) = (bs, (share, counter), node')). intro H3. cut (config_node_OK (fst (BDDneg_2 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node))))) (snd (BDDneg_2 (bs, (share, counter)) node (S (nat_of_N (var (bs, (share, counter)) node)))))). intro H4. rewrite (proj2 H3) in H4. exact H4. cut (is_internal_node (bs, (share, counter)) node -> nat_of_N (var (bs, (share, counter)) node) < S (nat_of_N (var (bs, (share, counter)) node))). intro H4. exact (proj1 (proj2 (proj2 (proj2 (BDDneg_2_lemma (S (nat_of_N (var (bs, (share, counter)) node))) (bs, (share, counter)) node H H1 H4))))). intro H4. unfold lt in |- *. apply le_n. apply H0. assumption. unfold lt in |- *. intro H3. apply le_n. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4