(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Require Import Bool.	
Require Import Sumbool.
Require Import Arith.
Require Import ZArith NArith Nnat Ndec Ndigits.		
From IntMap Require Import Map.
From IntMap Require Import Allmaps.			
Require Import List.
Require Import Wf_nat.
  
Require Import misc.
Require Import bool_fun.
Require Import myMap.
Require Import config.

Section BDD_alloc.

Variable gc : BDDconfig -> list ad -> BDDconfig.
Hypothesis gc_is_OK : gc_OK gc.

(* The arguments for the allocation function *)
Variable cfg : BDDconfig.
Variable x : BDDvar.
Variable l r : ad.
Variable ul : list ad.

(* Conditions on the arguments for the allocation function *)
Hypothesis cfg_OK : BDDconfig_OK cfg.
Hypothesis ul_OK : used_list_OK cfg ul.
Hypothesis l_used' : used_node' cfg ul l.
Hypothesis r_used' : used_node' cfg ul r.
Hypothesis l_neq_r : Neqb l r = false.
Hypothesis
  xl_lt_x :
    forall (xl : BDDvar) (ll rl : ad),
    MapGet _ (bs_of_cfg cfg) l = Some (xl, (ll, rl)) ->
    BDDcompare xl x = Datatypes.Lt.
Hypothesis
  xr_lt_x :
    forall (xr : BDDvar) (lr rr : ad),
    MapGet _ (bs_of_cfg cfg) r = Some (xr, (lr, rr)) ->
    BDDcompare xr x = Datatypes.Lt.
Hypothesis
  no_dup :
    forall (x' : BDDvar) (l' r' a : ad),
    MapGet _ (bs_of_cfg cfg) a = Some (x', (l', r')) ->
    (x, (l, r)) <> (x', (l', r')).

Let new_cfg := gc cfg ul.

Lemma no_dup_new :
 forall (x' : BDDvar) (l' r' a : ad),
 MapGet _ (bs_of_cfg new_cfg) a = Some (x', (l', r')) ->
 (x, (l, r)) <> (x', (l', r')).
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  apply no_dup with (a := a).
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
  apply (proj2 (proj2 (gc_is_OK _ _ cfg_OK ul_OK))).  assumption.
Qed.

Lemma new_cfg_OK : BDDconfig_OK new_cfg.
Proof.
(* Goal: BDDconfig_OK new_cfg *)
  exact (proj1 (gc_is_OK _ _ cfg_OK ul_OK)).
Qed.

Lemma new_cfg_nodes_preserved : used_nodes_preserved cfg new_cfg ul.
Proof.
(* Goal: used_nodes_preserved cfg new_cfg ul *)
  exact (proj1 (proj2 (gc_is_OK _ _ cfg_OK ul_OK))).
Qed.

Lemma new_l_OK : node_OK (bs_of_cfg new_cfg) l.
Proof.
(* Goal: node_OK (bs_of_cfg new_cfg) r *)
  apply node_preserved_OK_bs with (bs := bs_of_cfg cfg).
(* Goal: node_OK (bs_of_cfg cfg) r *)
  apply used_node'_OK_bs with (ul := ul).  exact (bs_of_cfg_OK _ cfg_OK).  
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  assumption.  assumption.
(* Goal: node_preserved_bs (bs_of_cfg cfg) (bs_of_cfg new_cfg) r *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg cfg) r) (@None (prod BDDvar (prod ad ad))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) r *)
  apply used_nodes_preserved_preserved'_bs with (ul := ul).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  exact (bs_of_cfg_OK _ cfg_OK).  exact new_cfg_nodes_preserved.  assumption.
Qed.

Lemma new_r_OK : node_OK (bs_of_cfg new_cfg) r.
Proof.
(* Goal: node_OK (bs_of_cfg new_cfg) r *)
  apply node_preserved_OK_bs with (bs := bs_of_cfg cfg).
(* Goal: node_OK (bs_of_cfg cfg) r *)
  apply used_node'_OK_bs with (ul := ul).  exact (bs_of_cfg_OK _ cfg_OK).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  assumption.  assumption.  
(* Goal: node_preserved_bs (bs_of_cfg cfg) (bs_of_cfg new_cfg) r *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg cfg) r) (@None (prod BDDvar (prod ad ad))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) r *)
  apply used_nodes_preserved_preserved'_bs with (ul := ul).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  exact (bs_of_cfg_OK _ cfg_OK).  exact new_cfg_nodes_preserved.  assumption.
Qed.

Lemma BDD_OK_l : BDD_OK (bs_of_cfg new_cfg) l.
Proof.
(* Goal: BDD_OK (bs_of_cfg new_cfg) r *)
  apply node_OK_BDD_OK.  exact (proj1 new_cfg_OK).  exact new_l_OK.
Qed.

Lemma BDD_OK_r : BDD_OK (bs_of_cfg new_cfg) r.
Proof.
(* Goal: BDD_OK (bs_of_cfg new_cfg) r *)
  apply node_OK_BDD_OK.  exact (proj1 new_cfg_OK).  exact new_r_OK.
Qed.

Lemma new_xl_lt_x :
 forall (xl : BDDvar) (ll rl : ad),
 MapGet _ (bs_of_cfg new_cfg) l = Some (xl, (ll, rl)) ->
 BDDcompare xl x = Datatypes.Lt.
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  cut (node_OK (bs_of_cfg cfg) l).  intro H00.  elim H00.  intros.
(* Goal: @eq comparison (BDDcompare xr x) Lt *)
(* Goal: forall (_ : or (@eq ad r BDDone) (@eq bool (in_dom (prod BDDvar (prod ad ad)) r (bs_of_cfg cfg)) true)) (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) r) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) r *)
  rewrite H in H0.  unfold bs_of_cfg in H0.
(* Goal: @eq comparison (BDDcompare xr x) Lt *)
(* Goal: forall (_ : or (@eq ad r BDDone) (@eq bool (in_dom (prod BDDvar (prod ad ad)) r (bs_of_cfg cfg)) true)) (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) r) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) r *)
  rewrite (config_OK_zero _ new_cfg_OK) in H0.  discriminate.  intro.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim H; intros.  rewrite H0 in H1.  unfold bs_of_cfg in H1.
(* Goal: @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  rewrite (config_OK_one _ new_cfg_OK) in H1.  discriminate.
(* Goal: @eq comparison (BDDcompare xl x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) l *)
  elim (option_sum _ (MapGet _ (bs_of_cfg cfg) l)).  intro y.  elim y.  intro x0.
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg cfg) r) (@Some (prod BDDvar (prod ad ad)) x0), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg cfg) r) (@None (prod BDDvar (prod ad ad))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) r *)
  elim x0.  intro y0.  intro y1.  elim y1; intros y2 y3 y4.
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  cut (MapGet _ (bs_of_cfg new_cfg) l = Some (y0, (y2, y3))).  intro.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  rewrite H2 in H1.  injection H1.  intros.  rewrite H3 in y4.
(* Goal: @eq comparison (BDDcompare xr x) Lt *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) r) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) y0 (@pair ad ad y2 y3))) *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg cfg) r) (@None (prod BDDvar (prod ad ad))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) r *)
  rewrite H4 in y4.  rewrite H5 in y4.  apply xl_lt_x with (ll := ll) (rl := rl).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  assumption.  cut (node_preserved_bs (bs_of_cfg cfg) (bs_of_cfg new_cfg) l).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  intro.  apply H2.  apply nodes_reachable_0.  assumption.  
(* Goal: node_preserved_bs (bs_of_cfg cfg) (bs_of_cfg new_cfg) r *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg cfg) r) (@None (prod BDDvar (prod ad ad))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) r *)
  apply used_nodes_preserved_preserved'_bs with (ul := ul).
(* Goal: BDDstate_OK (bs_of_cfg cfg) *)
(* Goal: used_list_OK_bs (bs_of_cfg cfg) ul *)
(* Goal: used_node'_bs (bs_of_cfg cfg) ul r *)
  exact (bs_of_cfg_OK _ cfg_OK).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  exact new_cfg_nodes_preserved.  assumption.  intro y.  unfold in_dom in H0.
(* Goal: node_OK (bs_of_cfg cfg) r *)
  rewrite y in H0.  discriminate.  apply used_node'_OK_bs with (ul := ul).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  exact (bs_of_cfg_OK _ cfg_OK).  assumption.  assumption.
Qed.

Lemma new_xr_lt_x :
 forall (xr : BDDvar) (lr rr : ad),
 MapGet _ (bs_of_cfg new_cfg) r = Some (xr, (lr, rr)) ->
 BDDcompare xr x = Datatypes.Lt.
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  cut (node_OK (bs_of_cfg cfg) r).  intro H00.  elim H00.  intros.
(* Goal: @eq comparison (BDDcompare xr x) Lt *)
(* Goal: forall (_ : or (@eq ad r BDDone) (@eq bool (in_dom (prod BDDvar (prod ad ad)) r (bs_of_cfg cfg)) true)) (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) r) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) r *)
  rewrite H in H0.  unfold bs_of_cfg in H0.
(* Goal: @eq comparison (BDDcompare xr x) Lt *)
(* Goal: forall (_ : or (@eq ad r BDDone) (@eq bool (in_dom (prod BDDvar (prod ad ad)) r (bs_of_cfg cfg)) true)) (xr : BDDvar) (lr rr : ad) (_ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) r) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) xr (@pair ad ad lr rr)))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) r *)
  rewrite (config_OK_zero _ new_cfg_OK) in H0.  discriminate.  intro.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim H; intros.  rewrite H0 in H1.  unfold bs_of_cfg in H1.
(* Goal: @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  rewrite (config_OK_one _ new_cfg_OK) in H1.  discriminate.
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim (option_sum _ (MapGet _ (bs_of_cfg cfg) r)).  intro y.  elim y.  intro x0.
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg cfg) r) (@Some (prod BDDvar (prod ad ad)) x0), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg cfg) r) (@None (prod BDDvar (prod ad ad))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) r *)
  elim x0.  intro y0.  intro y1.  elim y1; intros y2 y3 y4.
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  cut (MapGet _ (bs_of_cfg new_cfg) r = Some (y0, (y2, y3))).  intro.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  rewrite H2 in H1.  injection H1.  intros.  rewrite H3 in y4.
(* Goal: @eq comparison (BDDcompare xr x) Lt *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) r) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) y0 (@pair ad ad y2 y3))) *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg cfg) r) (@None (prod BDDvar (prod ad ad))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) r *)
  rewrite H4 in y4.  rewrite H5 in y4.  apply xr_lt_x with (lr := lr) (rr := rr).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  assumption.  cut (node_preserved_bs (bs_of_cfg cfg) (bs_of_cfg new_cfg) r).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  intro.  apply H2.  apply nodes_reachable_0.  assumption.
(* Goal: node_preserved_bs (bs_of_cfg cfg) (bs_of_cfg new_cfg) r *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg cfg) r) (@None (prod BDDvar (prod ad ad))), @eq comparison (BDDcompare xr x) Lt *)
(* Goal: node_OK (bs_of_cfg cfg) r *)
  apply used_nodes_preserved_preserved'_bs with (ul := ul).
(* Goal: BDDstate_OK (bs_of_cfg cfg) *)
(* Goal: used_list_OK_bs (bs_of_cfg cfg) ul *)
(* Goal: used_node'_bs (bs_of_cfg cfg) ul r *)
  exact (bs_of_cfg_OK _ cfg_OK).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  exact new_cfg_nodes_preserved.  assumption.  intro y.  unfold in_dom in H0.
(* Goal: node_OK (bs_of_cfg cfg) r *)
  rewrite y in H0.  discriminate.  apply used_node'_OK_bs with (ul := ul).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  exact (bs_of_cfg_OK _ cfg_OK).  assumption.  assumption.
Qed.

Definition BDDalloc : BDDconfig * ad :=
  match new_cfg with
  | (bs, (share, (fl, (cnt, (negm, orm))))) =>
      match fl with
      | a :: fl' =>
          (MapPut _ bs a (x, (l, r)),
          (MapPut3 _ share l r x a, (fl', (cnt, (negm, orm)))), a)
      | nil =>
          (MapPut _ bs cnt (x, (l, r)),
          (MapPut3 _ share l r x cnt, (fl, (ad_S cnt, (negm, orm)))), cnt)
      end
  end.
  
Lemma BDDalloc_lemma_1 :
 forall a : ad,
 MapGet _ (fst (fst BDDalloc)) a =
 (if Neqb a (snd BDDalloc)
  then Some (x, (l, r))
  else MapGet _ (fst new_cfg) a).
Proof.
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  intro.  unfold BDDalloc in |- *.  rewrite (cfg_comp new_cfg).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  elim (list_sum _ (fl_of_cfg new_cfg)).  intro.  rewrite H.  simpl in |- *.
  rewrite
   (MapPut_semantics (BDDvar * (ad * ad)) (bs_of_cfg new_cfg)
      (cnt_of_cfg new_cfg) (x, (l, r)) a).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  rewrite (Neqb_comm a (cnt_of_cfg new_cfg)).  reflexivity.  intro.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim H; clear H.  intros.  elim H; clear H; intros.  rewrite H.  simpl in |- *.
  rewrite
   (MapPut_semantics (BDDvar * (ad * ad)) (bs_of_cfg new_cfg) x0 
      (x, (l, r)) a).
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) *)
  rewrite (Neqb_comm a x0).  reflexivity.
Qed.

Lemma BDDalloc_lemma_2 :
 In (snd BDDalloc) (fl_of_cfg new_cfg) \/ cnt_of_cfg new_cfg = snd BDDalloc.
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  unfold BDDalloc in |- *.  rewrite (cfg_comp new_cfg).
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim (list_sum _ (fl_of_cfg new_cfg)).  intros.  rewrite H.  simpl in |- *.
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  unfold cnt_of_cfg in |- *.  simpl in |- *.  right; reflexivity.  intro.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim H; intros.  elim H0; intros.  rewrite H1.  simpl in |- *.  left.  left.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) *)
  reflexivity.
Qed.

Lemma BDDalloc_lemma_3 : MapGet _ (bs_of_cfg new_cfg) (snd BDDalloc) = None.
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  elim BDDalloc_lemma_2.  intros.  elim new_cfg_OK.  intros.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim H1; intros.  elim H3; intros.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (@snd BDDconfig ad BDDalloc)) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @eq ad (cnt_of_cfg new_cfg) (@snd BDDconfig ad BDDalloc), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (@snd BDDconfig ad BDDalloc)) (@None (prod BDDvar (prod ad ad))) *)
  exact (proj2 (proj2 (proj1 (proj2 H4 (snd BDDalloc)) H))).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  intro.  rewrite <- H.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: @eq bool (N.eqb x0 a) false *)
  apply (proj2 (proj1 (proj2 (proj2 (proj2 new_cfg_OK))))).
(* Goal: @eq bool (Nleb (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg)))) (cnt_of_cfg new_cfg)) true *)
  apply Nleb_refl.
Qed.

Lemma BDDalloc_lemma_4 :
 fst (fst BDDalloc) = MapPut _ (bs_of_cfg new_cfg) (snd BDDalloc) (x, (l, r)).
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  unfold BDDalloc in |- *.  rewrite (cfg_comp new_cfg).  simpl in |- *.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim (fl_of_cfg new_cfg).  reflexivity.  intros.  reflexivity.
Qed.

Lemma BDDalloc_lemma_5 :
 fst (snd (fst BDDalloc)) =
 MapPut3 _ (share_of_cfg new_cfg) l r x (snd BDDalloc).
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  unfold BDDalloc in |- *.  rewrite (cfg_comp new_cfg).  simpl in |- *.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim (fl_of_cfg new_cfg).  reflexivity.  intros.  reflexivity.
Qed.

Lemma BDDalloc_preserves_nodes :
 nodes_preserved_bs (bs_of_cfg new_cfg) (fst (fst BDDalloc)).
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  unfold nodes_preserved_bs in |- *.  intros.  rewrite BDDalloc_lemma_1.
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim (sumbool_of_bool (Neqb node (snd BDDalloc))).  intro y.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (if N.eqb node (@snd BDDconfig ad BDDalloc) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) node) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall _ : @eq bool (N.eqb node (@snd BDDconfig ad BDDalloc)) false, @eq (option (prod BDDvar (prod ad ad))) (if N.eqb node (@snd BDDconfig ad BDDalloc) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) node) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
  rewrite (Neqb_complete _ _ y) in H.  rewrite BDDalloc_lemma_3 in H.
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  discriminate H.  intro y.  rewrite y.  assumption.  
Qed.

Lemma BDDalloc_zero : MapGet _ (fst (fst BDDalloc)) BDDzero = None.
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  elim BDDalloc_lemma_2.  intro.  rewrite (BDDalloc_lemma_1 BDDzero).
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim (sumbool_of_bool (Neqb BDDzero (snd BDDalloc))).  intro y.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDone (@snd BDDconfig ad BDDalloc) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDone) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @eq bool (N.eqb BDDone (@snd BDDconfig ad BDDalloc)) false, @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDone (@snd BDDconfig ad BDDalloc) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDone) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @eq ad (cnt_of_cfg new_cfg) (@snd BDDconfig ad BDDalloc), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) BDDone) (@None (prod BDDvar (prod ad ad))) *)
  rewrite <- (Neqb_complete _ _ y) in H.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDzero (@snd BDDconfig ad BDDalloc) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDzero) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @eq bool (N.eqb BDDzero (@snd BDDconfig ad BDDalloc)) false, @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDzero (@snd BDDconfig ad BDDalloc) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDzero) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @eq ad (cnt_of_cfg new_cfg) (@snd BDDconfig ad BDDalloc), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) BDDzero) (@None (prod BDDvar (prod ad ad))) *)
  absurd (Nleb (Npos 2) BDDzero = true).  unfold BDDzero in |- *.  unfold not in |- *.
(* Goal: @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  intro.  unfold Nleb in H0.  simpl in H0.  discriminate.  
(* Goal: @eq bool (Nleb (Npos (xO xH)) BDDzero) true *)
(* Goal: forall _ : @eq bool (N.eqb BDDzero (@snd BDDconfig ad BDDalloc)) false, @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDzero (@snd BDDconfig ad BDDalloc) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDzero) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @eq ad (cnt_of_cfg new_cfg) (@snd BDDconfig ad BDDalloc), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) BDDzero) (@None (prod BDDvar (prod ad ad))) *)
  apply (proj1 (proj1 (proj2 (fl_of_cfg_OK _ new_cfg_OK) BDDzero) H)).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  intro y.  rewrite y.  exact (proj1 (bs_of_cfg_OK _ new_cfg_OK)).  intro.
(* Goal: no_dup_list ad (@cons ad x0 x1) *)
  rewrite (BDDalloc_lemma_1 BDDzero).  rewrite <- H.
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim (sumbool_of_bool (Neqb BDDzero (cnt_of_cfg new_cfg))).  intro y.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDone (cnt_of_cfg new_cfg) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDone) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @eq bool (N.eqb BDDone (cnt_of_cfg new_cfg)) false, @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDone (cnt_of_cfg new_cfg) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDone) (@None (prod BDDvar (prod ad ad))) *)
  cut (Nleb (Npos 2) (cnt_of_cfg new_cfg) = true).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  rewrite <- (Neqb_complete _ _ y).  intro.  unfold Nleb in H0.  simpl in H0.
(* Goal: @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  discriminate.  exact (proj1 (cnt_of_cfg_OK _ new_cfg_OK)).  intro y.
(* Goal: and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))) *)
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  rewrite y.  exact (proj1 (bs_of_cfg_OK _ new_cfg_OK)).
Qed.

Lemma BDDalloc_one : MapGet _ (fst (fst BDDalloc)) BDDone = None.
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  elim BDDalloc_lemma_2.  intro.  rewrite (BDDalloc_lemma_1 BDDone).
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim (sumbool_of_bool (Neqb BDDone (snd BDDalloc))).  intro y.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDone (@snd BDDconfig ad BDDalloc) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDone) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @eq bool (N.eqb BDDone (@snd BDDconfig ad BDDalloc)) false, @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDone (@snd BDDconfig ad BDDalloc) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDone) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @eq ad (cnt_of_cfg new_cfg) (@snd BDDconfig ad BDDalloc), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) BDDone) (@None (prod BDDvar (prod ad ad))) *)
  rewrite <- (Neqb_complete _ _ y) in H.
(* Goal: not (@eq bool (Nleb (Npos (xO xH)) (Npos xH)) true) *)
(* Goal: @eq bool (Nleb (Npos (xO xH)) BDDone) true *)
(* Goal: forall _ : @eq bool (N.eqb BDDone (@snd BDDconfig ad BDDalloc)) false, @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDone (@snd BDDconfig ad BDDalloc) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDone) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @eq ad (cnt_of_cfg new_cfg) (@snd BDDconfig ad BDDalloc), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) BDDone) (@None (prod BDDvar (prod ad ad))) *)
  absurd (Nleb (Npos 2) BDDone = true).  unfold BDDone in |- *.  unfold not in |- *.
(* Goal: @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  intro.  unfold Nleb in H0.  simpl in H0.  discriminate.  
(* Goal: @eq bool (Nleb (Npos (xO xH)) BDDone) true *)
(* Goal: forall _ : @eq bool (N.eqb BDDone (@snd BDDconfig ad BDDalloc)) false, @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDone (@snd BDDconfig ad BDDalloc) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDone) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @eq ad (cnt_of_cfg new_cfg) (@snd BDDconfig ad BDDalloc), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) BDDone) (@None (prod BDDvar (prod ad ad))) *)
  apply (proj1 (proj1 (proj2 (fl_of_cfg_OK _ new_cfg_OK) BDDone) H)).
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intro y.  rewrite y.  exact (proj1 (proj2 (bs_of_cfg_OK _ new_cfg_OK))).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  intro.  rewrite (BDDalloc_lemma_1 BDDone).  rewrite <- H.
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim (sumbool_of_bool (Neqb BDDone (cnt_of_cfg new_cfg))).  intro y.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDone (cnt_of_cfg new_cfg) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDone) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @eq bool (N.eqb BDDone (cnt_of_cfg new_cfg)) false, @eq (option (prod BDDvar (prod ad ad))) (if N.eqb BDDone (cnt_of_cfg new_cfg) then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) BDDone) (@None (prod BDDvar (prod ad ad))) *)
  cut (Nleb (Npos 2) (cnt_of_cfg new_cfg) = true).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  rewrite <- (Neqb_complete _ _ y).  intro.  unfold Nleb in H0.  simpl in H0.
(* Goal: @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  discriminate.  exact (proj1 (cnt_of_cfg_OK _ new_cfg_OK)).  intro y.
(* Goal: and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))) *)
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  rewrite y.  exact (proj1 (proj2 (bs_of_cfg_OK _ new_cfg_OK))).
Qed.

Lemma BDDalloc_BDD_OK : BDD_OK (fst (fst BDDalloc)) (snd BDDalloc).
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  unfold BDD_OK in |- *.  cut
   (MapGet (BDDvar * (ad * ad)) (fst (fst BDDalloc)) (snd BDDalloc) =
    Some (x, (l, r))).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  intro H.  rewrite H.  apply BDDbounded_2 with (x := x) (l := l) (r := r).  assumption.
(* Goal: @eq comparison (BDDcompare x (ad_S x)) Lt *)
(* Goal: @eq bool (N.eqb l r) false *)
(* Goal: BDDbounded (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) l x *)
(* Goal: BDDbounded (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) r x *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDconfig ad BDDalloc)) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) *)
  apply BDDlt_compare.  rewrite (ad_S_is_S x).  unfold lt in |- *.  apply le_n.
(* Goal: @eq bool (N.eqb l r) false *)
(* Goal: BDDbounded (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) l x *)
(* Goal: BDDbounded (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) r x *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDconfig ad BDDalloc)) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) *)
  apply not_true_is_false.  unfold not in |- *; intro H0.  rewrite l_neq_r in H0.
(* Goal: @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  discriminate.  elim (option_sum _ (MapGet _ (bs_of_cfg new_cfg) l)).  intro y.
(* Goal: forall (x0 : prod BDDvar (prod ad ad)) (_ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) r) (@Some (prod BDDvar (prod ad ad)) x0)), BDDbounded (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) r x *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) r) (@None (prod BDDvar (prod ad ad))), BDDbounded (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) r x *)
(* Goal: BDD_OK (bs_of_cfg new_cfg) r *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDconfig ad BDDalloc)) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) *)
  elim y; clear y.  intro x0.  elim x0; clear x0.  intros xl y0.
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim y0; clear y0.  intros ll rl.  intro y.
(* Goal: BDDbounded (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) a (ad_S x1) *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) a) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x1 (@pair ad ad l1 r1))) *)
(* Goal: forall (_ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a) (@None (prod BDDvar (prod ad ad)))) (_ : @eq bool match MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) a with | Some a => true | None => false end true), BDD_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) a *)
  apply nodes_preserved_bounded with (bs := bs_of_cfg new_cfg).
(* Goal: nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) *)
  exact BDDalloc_preserves_nodes.  cut (BDDcompare (ad_S xl) x = Datatypes.Lt \/ ad_S xl = x).
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a0 then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))), @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  intro H0.  elim H0; intro H1.  apply increase_bound with (n := ad_S xl).
(* Goal: and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))) *)
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  cut (BDD_OK (bs_of_cfg new_cfg) l).  unfold BDD_OK in |- *.  rewrite y.
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  intro; assumption.  exact BDD_OK_l.  assumption.  rewrite <- H1.
(* Goal: and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))) *)
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  cut (BDD_OK (bs_of_cfg new_cfg) l).  unfold BDD_OK in |- *.  rewrite y.
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  intro; assumption.  exact BDD_OK_l.  apply BDDcompare_1.
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  apply (new_xl_lt_x xl ll rl).  assumption.  intro y.
(* Goal: and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))) *)
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  cut (BDD_OK (bs_of_cfg new_cfg) l).  unfold BDD_OK in |- *.  rewrite y.  intro H0.
(* Goal: @eq (option ad) (if andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0)) then @Some ad a else MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0) *)
(* Goal: @eq bool (andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0))) false *)
  elim H0; intro H1.  rewrite H1.  apply BDDbounded_0.  rewrite H1.
(* Goal: BDD_OK (bs_of_cfg new_cfg) l *)
(* Goal: BDDbounded (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) r x *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDconfig ad BDDalloc)) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) *)
  apply BDDbounded_1.  exact BDD_OK_l.  cut (BDD_OK (bs_of_cfg new_cfg) r).
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a0 then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))), @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  intro H0.  unfold BDD_OK in H0.  elim (option_sum _ (MapGet _ (bs_of_cfg new_cfg) r)).
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intro y.  elim y; clear y.  intro x0.  elim x0; clear x0.  intros xr y0.
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim y0; clear y0.  intros lr rr.  intro y.  apply nodes_preserved_bounded with (bs := bs_of_cfg new_cfg).
(* Goal: @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  exact BDDalloc_preserves_nodes.  rewrite y in H0.
(* Goal: BDDbounded (bs_of_cfg new_cfg) r x *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) r) (@None (prod BDDvar (prod ad ad))), BDDbounded (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) r x *)
(* Goal: BDD_OK (bs_of_cfg new_cfg) r *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDconfig ad BDDalloc)) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) *)
  cut (BDDcompare (ad_S xr) x = Datatypes.Lt \/ ad_S xr = x).  intro H1.  elim H1; intro H2.
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  apply increase_bound with (n := ad_S xr).  assumption.  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  rewrite <- H2; assumption.  apply BDDcompare_1.  apply (new_xr_lt_x xr lr rr).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  assumption.  intro y.  rewrite y in H0.  elim H0; intro.  rewrite H1.
(* Goal: @eq (option ad) (if andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0)) then @Some ad a else MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0) *)
(* Goal: @eq bool (andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0))) false *)
  apply BDDbounded_0.  rewrite H1.  apply BDDbounded_1.  exact BDD_OK_r.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) *)
  rewrite BDDalloc_lemma_1.  rewrite (Neqb_correct (snd BDDalloc)).  reflexivity.
Qed.

Lemma BDDalloc_keeps_state_OK : BDDstate_OK (fst (fst BDDalloc)).
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  split.  apply BDDalloc_zero.  split.  apply BDDalloc_one.  
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  unfold in_dom in |- *.  intro.  rewrite (BDDalloc_lemma_1 a).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  elim (sumbool_of_bool (Neqb a (snd BDDalloc))).  intro y.  rewrite y.  intro.
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  rewrite (Neqb_complete _ _ y).  apply BDDalloc_BDD_OK.  intro y.  rewrite y.
(* Goal: forall (_ : @eq bool (N.eqb a a0) true) (_ : @eq (option ad) (MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0)), @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a0 then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall (_ : @eq bool (N.eqb a a0) false) (_ : @eq (option ad) (MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0)), @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a0 then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))), @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  elim (option_sum _ (MapGet _ (bs_of_cfg new_cfg) a)).  intro y0.
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  elim y0; clear y0; intro.  elim x0; clear x0; intros x1 y0.
(* Goal: forall (_ : @eq bool (N.eqb a a0) true) (_ : @eq (option ad) (MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0)), @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a0 then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall (_ : @eq bool (N.eqb a a0) false) (_ : @eq (option ad) (MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0)), @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a0 then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))), @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  elim y0; clear y0; intros l1 r1.  intro y0.  intro H.  unfold BDD_OK in |- *.
  cut
   (MapGet (BDDvar * (ad * ad)) (fst (fst BDDalloc)) a =
    Some (x1, (l1, r1))).
(* Goal: BDDbounded (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) a (ad_S x1) *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) a) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x1 (@pair ad ad l1 r1))) *)
(* Goal: forall (_ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a) (@None (prod BDDvar (prod ad ad)))) (_ : @eq bool match MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) a with | Some a => true | None => false end true), BDD_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) a *)
  intro H0.  rewrite H0.  apply nodes_preserved_bounded with (bs := bs_of_cfg new_cfg).
(* Goal: nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) *)
  exact BDDalloc_preserves_nodes.  cut (BDD_OK (bs_of_cfg new_cfg) a).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  unfold BDD_OK in |- *.  rewrite y0.  intro; assumption.
(* Goal: @eq bool (in_dom (prod BDDvar (prod ad ad)) a (bs_of_cfg new_cfg)) true *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) a) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x1 (@pair ad ad l1 r1))) *)
(* Goal: forall (_ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a) (@None (prod BDDvar (prod ad ad)))) (_ : @eq bool match MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) a with | Some a => true | None => false end true), BDD_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) a *)
  apply (proj2 (proj2 (bs_of_cfg_OK _ new_cfg_OK))).  unfold in_dom in |- *.
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  rewrite y0.  reflexivity.  apply BDDalloc_preserves_nodes.  assumption.  
(* Goal: @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  intros y0 H.  unfold bs_of_cfg in y0.  rewrite y0 in H.  discriminate.
Qed.

Lemma BDDsharing_OK_1 :
 forall a : ad,
 MapGet _ (bs_of_cfg new_cfg) a = None ->
 BDDsharing_OK (MapPut _ (bs_of_cfg new_cfg) a (x, (l, r)))
   (MapPut3 _ (share_of_cfg new_cfg) l r x a).
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  split.  rewrite (MapPut3_semantics ad (share_of_cfg new_cfg) l r x l0 r0 x0 a).
(* Goal: forall _ : @eq (option ad) (if andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0)) then @Some ad a else MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))), @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  elim (sumbool_of_bool (Neqb l l0 && (Neqb r r0 && Neqb x x0))).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  intro y.  rewrite y.  intro H0.  injection H0; intro.  rewrite <- H1.
  rewrite
   (MapPut_semantics (BDDvar * (ad * ad)) (bs_of_cfg new_cfg) a (x, (l, r)) a)
   .
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall (_ : @eq bool (andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0))) false) (_ : @eq (option ad) (if andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0)) then @Some ad a else MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0)), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))), @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  rewrite (Neqb_correct a).  cut (Neqb l l0 = true /\ Neqb r r0 = true /\ Neqb x x0 = true).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  intro.  rewrite (Neqb_complete _ _ (proj1 H2)).
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l0 r))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: and (@eq bool (N.eqb l l0) true) (and (@eq bool (N.eqb r r0) true) (@eq bool (N.eqb x x0) true)) *)
(* Goal: forall (_ : @eq bool (andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0))) false) (_ : @eq (option ad) (if andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0)) then @Some ad a else MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0)), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))), @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  rewrite (Neqb_complete _ _ (proj1 (proj2 H2))).
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) *)
  rewrite (Neqb_complete _ _ (proj2 (proj2 H2))).  reflexivity.
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  apply andb3_lemma.  assumption.  intro y.  rewrite y.
  rewrite
   (MapPut_semantics (BDDvar * (ad * ad)) (bs_of_cfg new_cfg) a 
      (x, (l, r)) a0).
(* Goal: forall (_ : @eq bool (N.eqb a a0) true) (_ : @eq (option ad) (MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0)), @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a0 then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall (_ : @eq bool (N.eqb a a0) false) (_ : @eq (option ad) (MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0)), @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a0 then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))), @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  elim (sumbool_of_bool (Neqb a a0)).  intro y0.  intro H0.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a0 then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall (_ : @eq bool (N.eqb a a0) false) (_ : @eq (option ad) (MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0)), @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a0 then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))), @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  rewrite <- (Neqb_complete _ _ y0) in H0.  unfold share_of_cfg in H0.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a0 then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall (_ : @eq bool (N.eqb a a0) false) (_ : @eq (option ad) (MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0)), @eq (option (prod BDDvar (prod ad ad))) (if N.eqb a a0 then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))), @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  unfold bs_of_cfg in H.  rewrite (proj1 (proj1 (proj2 new_cfg_OK) x0 l0 r0 a) H0) in H.
(* Goal: @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  discriminate.  intros y0 H0.  rewrite y0.  unfold bs_of_cfg in |- *.  unfold share_of_cfg in H0.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
(* Goal: forall _ : @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))), @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  exact (proj1 (proj1 (proj2 new_cfg_OK) x0 l0 r0 a0) H0).  
  rewrite
   (MapPut_semantics (BDDvar * (ad * ad)) (bs_of_cfg new_cfg) a 
      (x, (l, r)) a0).
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intro H0.  elim (sumbool_of_bool (Neqb a a0)).  intro y.  rewrite y in H0.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  injection H0.  intros.  rewrite <- H1.  rewrite <- H2.  rewrite <- H3.
(* Goal: @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l r x) (@Some ad a0) *)
(* Goal: forall _ : @eq bool (N.eqb a a0) false, @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  rewrite (MapPut3_semantics ad (share_of_cfg new_cfg) l r x l r x a).
(* Goal: @eq (option ad) (if andb (N.eqb l l) (andb (N.eqb r r) (N.eqb x x)) then @Some ad a else MapGet3 ad (share_of_cfg new_cfg) l r x) (@Some ad a0) *)
(* Goal: forall _ : @eq bool (N.eqb a a0) false, @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  rewrite (Neqb_correct l).  rewrite (Neqb_correct r).  rewrite (Neqb_correct x).
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  simpl in |- *.  rewrite (Neqb_complete _ _ y).  reflexivity.  intro y.  rewrite y in H0.
(* Goal: @eq (option ad) (MapGet3 ad (MapPut3 ad (share_of_cfg new_cfg) l r x a) l0 r0 x0) (@Some ad a0) *)
  rewrite (MapPut3_semantics ad (share_of_cfg new_cfg) l r x l0 r0 x0 a).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  cut (Neqb l l0 && (Neqb r r0 && Neqb x x0) = false).  intro.
(* Goal: @eq (option ad) (MapGet3 ad (@fst BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg)) l0 r0 x0) (@Some ad a0) *)
(* Goal: @eq bool (andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0))) false *)
  rewrite H1.  unfold share_of_cfg in |- *.  unfold bs_of_cfg in H0.
(* Goal: @eq (option ad) (MapGet3 ad (@fst BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg)) l0 r0 x0) (@Some ad a0) *)
(* Goal: @eq bool (andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0))) false *)
  exact (proj2 (proj1 (proj2 new_cfg_OK) x0 l0 r0 a0) H0).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  apply andb3_lemma_1.  cut ((x, (l, r)) <> (x0, (l0, r0))).  intro.  unfold not in |- *; intro.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  apply H1.  injection H2; intros.  rewrite H3.  rewrite H4.  rewrite H5.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) *)
  reflexivity.  apply no_dup with (a := a0).
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg cfg) a0) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x0 (@pair ad ad l0 r0))) *)
  apply (proj2 (proj2 (gc_is_OK _ _ cfg_OK ul_OK))).  assumption.
Qed.

Lemma BDDalloc_keeps_sharing_OK :
 BDDsharing_OK (fst (fst BDDalloc)) (fst (snd (fst BDDalloc))).
Proof.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  rewrite BDDalloc_lemma_4.  rewrite BDDalloc_lemma_5.
(* Goal: BDDsharing_OK (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (@snd BDDconfig ad BDDalloc) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (MapPut3 ad (share_of_cfg new_cfg) l r x (@snd BDDconfig ad BDDalloc)) *)
  apply BDDsharing_OK_1.  apply BDDalloc_lemma_3.
Qed.

Lemma BDDalloc_keeps_cnt_OK :
 cnt_OK (fst (fst BDDalloc)) (fst (snd (snd (snd (fst BDDalloc))))).
Proof.
(* Goal: @eq BDDuniv_memo (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad (let (bs, p) := new_cfg in let (share, p0) := p in let (fl, p1) := p0 in let (cnt, p2) := p1 in let (negm, orm) := p2 in match fl with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) bs cnt (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad share l r x cnt) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S cnt) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) negm orm))))) cnt | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) bs a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad share l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) cnt (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) negm orm))))) a end)))))))) (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg)))))) *)
  unfold BDDalloc, cnt_OK in |- *.  rewrite (cfg_comp new_cfg).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  elim (list_sum _ (fl_of_cfg new_cfg)).  intro.  rewrite H.  simpl in |- *.  split.
(* Goal: @eq bool (Nleb (ad_S x0) (cnt_of_cfg new_cfg)) true *)
(* Goal: @eq bool (Nleb (cnt_of_cfg new_cfg) a) true *)
  apply Nleb_trans with (b := cnt_of_cfg new_cfg).  unfold cnt_of_cfg in |- *.
(* Goal: @eq bool (Nleb (Npos (xO xH)) (cnt_of_cfg new_cfg)) true *)
(* Goal: forall (a : ad) (_ : @eq bool (Nleb (cnt_of_cfg new_cfg) a) true), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) x0 (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a) (@None (prod BDDvar (prod ad ad))) *)
  exact (proj1 (proj1 (proj2 (proj2 (proj2 new_cfg_OK))))).
(* Goal: @eq bool (Nleb (ad_S node) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))))) true *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) node) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @ex ad (fun a : ad => @ex (list ad) (fun l' : list ad => @eq (list ad) (fl_of_cfg new_cfg) (@cons ad a l'))), BDDfree_list_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)) (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)))) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end))))) *)
  unfold Nleb in |- *.  apply leb_correct.  rewrite (ad_S_is_S (cnt_of_cfg new_cfg)).
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  apply le_S.  apply le_n.  intros.
  rewrite
   (MapPut_semantics (BDDvar * (ad * ad)) (bs_of_cfg new_cfg)
      (cnt_of_cfg new_cfg) (x, (l, r)) a).
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (if N.eqb (cnt_of_cfg new_cfg) a then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @ex ad (fun a : ad => @ex (list ad) (fun l' : list ad => @eq (list ad) (fl_of_cfg new_cfg) (@cons ad a l'))), and (@eq bool (Nleb (Npos (xO xH)) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)))))) true) (forall (a : ad) (_ : @eq bool (Nleb (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a0 fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0 (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a0) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a0 end))))) a) true), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a0 fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0 (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a0) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a0 end)) a) (@None (prod BDDvar (prod ad ad)))) *)
  replace (Neqb (cnt_of_cfg new_cfg) a) with false.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: @eq bool false (N.eqb (cnt_of_cfg new_cfg) a) *)
(* Goal: forall _ : @ex ad (fun a : ad => @ex (list ad) (fun l' : list ad => @eq (list ad) (fl_of_cfg new_cfg) (@cons ad a l'))), and (@eq bool (Nleb (Npos (xO xH)) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)))))) true) (forall (a : ad) (_ : @eq bool (Nleb (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a0 fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0 (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a0) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a0 end))))) a) true), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a0 fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0 (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a0) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a0 end)) a) (@None (prod BDDvar (prod ad ad)))) *)
  refine (proj2 (proj1 (proj2 (proj2 (proj2 new_cfg_OK)))) a _).
(* Goal: @eq bool (Nleb (ad_S node) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))))) true *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) node) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @ex ad (fun a : ad => @ex (list ad) (fun l' : list ad => @eq (list ad) (fl_of_cfg new_cfg) (@cons ad a l'))), BDDfree_list_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)) (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)))) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end))))) *)
  apply Nleb_trans with (b := ad_S (cnt_of_cfg new_cfg)).  unfold Nleb in |- *.
(* Goal: @eq bool (Nat.leb (N.to_nat (ad_S node)) (N.to_nat (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg)))))) true *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) node) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @ex ad (fun a : ad => @ex (list ad) (fun l' : list ad => @eq (list ad) (fl_of_cfg new_cfg) (@cons ad a l'))), BDDfree_list_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)) (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)))) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end))))) *)
  apply leb_correct.  rewrite (ad_S_is_S (cnt_of_cfg new_cfg)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  apply le_S.  apply le_n.  assumption.  symmetry  in |- *.  apply ad_S_le_then_neq.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  assumption.  intro.  elim H; clear H; intros.  elim H; clear H; intros.
(* Goal: forall _ : @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))), @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  rewrite H.  simpl in |- *.  split.
(* Goal: @eq bool (Nleb (Npos (xO xH)) (cnt_of_cfg new_cfg)) true *)
(* Goal: forall (a : ad) (_ : @eq bool (Nleb (cnt_of_cfg new_cfg) a) true), @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) x0 (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) a) (@None (prod BDDvar (prod ad ad))) *)
  exact (proj1 (proj1 (proj2 (proj2 (proj2 new_cfg_OK))))).
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  intros.  rewrite
   (MapPut_semantics (BDDvar * (ad * ad)) (bs_of_cfg new_cfg) x0 
      (x, (l, r)) a).
(* Goal: @eq (option ad) (if andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0)) then @Some ad a else MapGet3 ad (share_of_cfg new_cfg) l0 r0 x0) (@Some ad a0) *)
(* Goal: @eq bool (andb (N.eqb l l0) (andb (N.eqb r r0) (N.eqb x x0))) false *)
  cut (Neqb x0 a = false).  intro; rewrite H1.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: @eq bool (N.eqb x0 a) false *)
  apply (proj2 (proj1 (proj2 (proj2 (proj2 new_cfg_OK))))).
(* Goal: @eq bool (Nleb (ad_S x0) a) true *)
  exact H0.  apply ad_S_le_then_neq.  apply Nleb_trans with (b := cnt_of_cfg new_cfg).
(* Goal: @eq bool (Nleb (ad_S x0) (cnt_of_cfg new_cfg)) true *)
(* Goal: @eq bool (Nleb (cnt_of_cfg new_cfg) a) true *)
  unfold cnt_of_cfg in |- *.  refine
   (proj1 (proj2 (proj1 (proj2 (proj1 (proj2 (proj2 new_cfg_OK))) x0) _))).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  unfold fl_of_cfg in H.  rewrite H.  simpl in |- *.  left; reflexivity.  assumption.
Qed.

Lemma BDDalloc_keeps_free_list_OK :
 BDDfree_list_OK (fst (fst BDDalloc)) (fst (snd (snd (fst BDDalloc))))
   (fst (snd (snd (snd (fst BDDalloc))))).
Proof.
(* Goal: BDDfree_list_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)))) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc))))) *)
  unfold BDDalloc in |- *.  rewrite (cfg_comp new_cfg).  elim (list_sum _ (fl_of_cfg new_cfg)).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  intro.  rewrite H.  simpl in |- *.  unfold BDDfree_list_OK in |- *.  split.  apply no_dup_nil.
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  intro.  rewrite
   (MapPut_semantics (BDDvar * (ad * ad)) (bs_of_cfg new_cfg)
      (cnt_of_cfg new_cfg) (x, (l, r)) node).
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  split.  simpl in |- *.  tauto.  intro.  elim H0; clear H0; intros.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim H1; clear H1; intros.  elim (sumbool_of_bool (Neqb (cnt_of_cfg new_cfg) node)).
(* Goal: @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  intro y.  rewrite y in H2.  discriminate.  intro y.  rewrite y in H2.
(* Goal: forall _ : @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))), @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  absurd (In node (fl_of_cfg new_cfg)).  rewrite H.  simpl in |- *.  tauto.  
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  apply (proj2 (proj2 (proj1 (proj2 (proj2 new_cfg_OK))) node)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  split.  assumption.  split.  unfold Nleb in |- *.  apply leb_correct.
(* Goal: le (N.to_nat (ad_S node)) (N.to_nat (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))))) *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) node) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @ex ad (fun a : ad => @ex (list ad) (fun l' : list ad => @eq (list ad) (fl_of_cfg new_cfg) (@cons ad a l'))), BDDfree_list_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)) (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)))) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end))))) *)
  rewrite (ad_S_is_S node).  apply lt_le_S.
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  cut (nat_of_N node <= nat_of_N (cnt_of_cfg new_cfg)).  intro.
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  elim (le_lt_or_eq _ _ H3).  tauto.  intro.  unfold cnt_of_cfg in y.
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  cut (node = fst (snd (snd (snd new_cfg)))).  intro.  rewrite H5 in y.
(* Goal: @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  rewrite (Neqb_correct (fst (snd (snd (snd new_cfg))))) in y.  discriminate.
(* Goal: @eq ad (N.of_nat (N.to_nat node)) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg)))) *)
(* Goal: le (N.to_nat node) (N.to_nat (cnt_of_cfg new_cfg)) *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) node) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @ex ad (fun a : ad => @ex (list ad) (fun l' : list ad => @eq (list ad) (fl_of_cfg new_cfg) (@cons ad a l'))), BDDfree_list_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)) (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)))) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end))))) *)
  rewrite <- (N_of_nat_of_N node).  rewrite H4.  apply N_of_nat_of_N.  
(* Goal: le (N.to_nat node) (N.to_nat (cnt_of_cfg new_cfg)) *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) node) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @ex ad (fun a : ad => @ex (list ad) (fun l' : list ad => @eq (list ad) (fl_of_cfg new_cfg) (@cons ad a l'))), BDDfree_list_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)) (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)))) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end))))) *)
  apply le_S_n.  rewrite <- (ad_S_is_S node).
(* Goal: le (N.to_nat (ad_S node)) (S (N.to_nat (cnt_of_cfg new_cfg))) *)
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg) node) (@None (prod BDDvar (prod ad ad))) *)
(* Goal: forall _ : @ex ad (fun a : ad => @ex (list ad) (fun l' : list ad => @eq (list ad) (fl_of_cfg new_cfg) (@cons ad a l'))), BDDfree_list_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)) (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end)))) (@fst ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match fl_of_cfg new_cfg with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (fl_of_cfg new_cfg) (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a end))))) *)
  rewrite <- (ad_S_is_S (cnt_of_cfg new_cfg)).  unfold Nleb in H1.
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  apply leb_complete.  assumption.  assumption.  intro.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim H; clear H; intros.  elim H; clear H; intros.  rewrite H.  simpl in |- *.
(* Goal: and (BDDor_memo_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@fst BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)))))))) (BDDuniv_memo_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)))))))) *)
  unfold BDDfree_list_OK in |- *.  split.  apply no_dup_cons_no_dup with (a := x0).
(* Goal: no_dup_list ad (@cons ad x0 x1) *)
(* Goal: forall node : ad, iff (@In ad node x1) (and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) x0 (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) node) (@None (prod BDDvar (prod ad ad)))))) *)
  unfold ad in *.
(* Goal: no_dup_list ad (@cons ad x0 x1) *)
  rewrite <- H.  unfold fl_of_cfg in |- *.  exact (proj1 (proj1 (proj2 (proj2 new_cfg_OK)))).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  cut (~ In x0 x1).  intro.  intro.
  rewrite
   (MapPut_semantics (BDDvar * (ad * ad)) (bs_of_cfg new_cfg) x0 
      (x, (l, r)) node).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  split.  intro.  elim (sumbool_of_bool (Neqb x0 node)).  intro y.
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  absurd (In node x1).  rewrite <- (Neqb_complete _ _ y).  assumption.
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  assumption.  intro y.
(* Goal: and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))) *)
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  rewrite y.  apply (proj1 (proj2 (proj1 (proj2 (proj2 new_cfg_OK))) node)).
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  unfold fl_of_cfg in H.  rewrite H.  apply in_cons.  assumption.  intros.
(* Goal: forall _ : @eq bool (N.eqb x0 node) false, @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim (sumbool_of_bool (Neqb x0 node)).  intro y.  rewrite y in H1.
(* Goal: forall _ : and (@eq bool (Nleb (Npos (xO xH)) node) true) (and (@eq bool (Nleb (ad_S node) (cnt_of_cfg new_cfg)) true) (@eq (option (prod BDDvar (prod ad ad))) (if N.eqb x0 node then @Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r)) else MapGet (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) node) (@None (prod BDDvar (prod ad ad))))), @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  elim H1; intros.  elim H3; intros.  discriminate.  intro y.
(* Goal: @In ad node x1 *)
(* Goal: not (@In ad x0 x1) *)
  rewrite y in H1.  unfold bs_of_cfg in H1.  cut (In node (fst (snd (snd new_cfg)))).
(* Goal: forall _ : @eq ad x0 node, @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  unfold fl_of_cfg in H.  rewrite H.  intro.  elim (in_inv H2).  intro.
(* Goal: @In ad node x1 *)
(* Goal: forall _ : @In ad node x1, @In ad node x1 *)
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  rewrite H3 in y.  rewrite (Neqb_correct node) in y.  discriminate.  tauto.
(* Goal: @In ad node (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
(* Goal: not (@In ad x0 x1) *)
  apply (proj2 (proj2 (proj1 (proj2 (proj2 new_cfg_OK))) node)).
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  assumption.  apply no_dup_cons_no_in.  rewrite <- H.  unfold fl_of_cfg in |- *.
(* Goal: no_dup_list ad (@fst BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg))) *)
  exact (proj1 (proj1 (proj2 (proj2 new_cfg_OK)))).
Qed.

Lemma BDDalloc_orm_same : orm_of_cfg (fst BDDalloc) = orm_of_cfg new_cfg.
Proof.
(* Goal: @eq BDDuniv_memo (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad (let (bs, p) := new_cfg in let (share, p0) := p in let (fl, p1) := p0 in let (cnt, p2) := p1 in let (negm, orm) := p2 in match fl with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) bs cnt (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad share l r x cnt) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S cnt) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) negm orm))))) cnt | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) bs a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad share l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) cnt (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) negm orm))))) a end)))))))) (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg)))))) *)
  unfold orm_of_cfg, BDDalloc in |- *.  rewrite (cfg_comp new_cfg).  simpl in |- *.
(* Goal: forall (a : ad) (l0 : list ad) (_ : @eq BDDuniv_memo (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match l0 with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) l0 (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a0 fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0 (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a0) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a0 end))))))) (um_of_cfg new_cfg)), @eq BDDuniv_memo (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad (@pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) l0 (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a)))))))) (um_of_cfg new_cfg) *)
  elim (fl_of_cfg new_cfg).  simpl in |- *.  reflexivity.  simpl in |- *.  reflexivity.
Qed.

Lemma BDDalloc_negm_same : negm_of_cfg (fst BDDalloc) = negm_of_cfg new_cfg.
Proof.
(* Goal: @eq BDDuniv_memo (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad (let (bs, p) := new_cfg in let (share, p0) := p in let (fl, p1) := p0 in let (cnt, p2) := p1 in let (negm, orm) := p2 in match fl with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) bs cnt (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad share l r x cnt) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S cnt) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) negm orm))))) cnt | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) bs a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad share l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) cnt (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) negm orm))))) a end)))))))) (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg)))))) *)
  unfold negm_of_cfg, BDDalloc in |- *.  rewrite (cfg_comp new_cfg).  simpl in |- *.
(* Goal: forall (a : ad) (l0 : list ad) (_ : @eq BDDuniv_memo (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match l0 with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) l0 (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a0 fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0 (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a0) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a0 end))))))) (um_of_cfg new_cfg)), @eq BDDuniv_memo (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad (@pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) l0 (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a)))))))) (um_of_cfg new_cfg) *)
  elim (fl_of_cfg new_cfg).  simpl in |- *.  reflexivity.  simpl in |- *.  reflexivity.
Qed.

Lemma BDDalloc_um_same : um_of_cfg (fst BDDalloc) = um_of_cfg new_cfg.
Proof.
(* Goal: @eq BDDuniv_memo (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad (let (bs, p) := new_cfg in let (share, p0) := p in let (fl, p1) := p0 in let (cnt, p2) := p1 in let (negm, orm) := p2 in match fl with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) bs cnt (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad share l r x cnt) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S cnt) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) negm orm))))) cnt | cons a fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) bs a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad share l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) cnt (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) negm orm))))) a end)))))))) (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) new_cfg)))))) *)
  unfold um_of_cfg, BDDalloc in |- *.  rewrite (cfg_comp new_cfg).  simpl in |- *.
(* Goal: forall (a : ad) (l0 : list ad) (_ : @eq BDDuniv_memo (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad match l0 with | nil => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) (cnt_of_cfg new_cfg) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x (cnt_of_cfg new_cfg)) (@pair BDDfree_list (prod N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) l0 (@pair N (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (ad_S (cnt_of_cfg new_cfg)) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) (cnt_of_cfg new_cfg) | cons a0 fl' => @pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a0 (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a0) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) fl' (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a0 end))))))) (um_of_cfg new_cfg)), @eq BDDuniv_memo (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad (@pair (prod (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))))) ad (@pair (Map (prod BDDvar (prod ad ad))) (prod (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (MapPut (prod BDDvar (prod ad ad)) (bs_of_cfg new_cfg) a (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@pair (Map (Map (Map ad))) (prod (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (MapPut3 ad (share_of_cfg new_cfg) l r x a) (@pair (list ad) (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) l0 (@pair ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (cnt_of_cfg new_cfg) (@pair BDDneg_memo (prod BDDor_memo BDDuniv_memo) (negm_of_cfg new_cfg) (@pair BDDor_memo BDDuniv_memo (orm_of_cfg new_cfg) (um_of_cfg new_cfg))))))) a)))))))) (um_of_cfg new_cfg) *)
  elim (fl_of_cfg new_cfg).  simpl in |- *.  reflexivity.  simpl in |- *.  reflexivity.
Qed.

Lemma BDDalloc_keeps_neg_memo_OK :
 BDDneg_memo_OK (bs_of_cfg (fst BDDalloc)) (negm_of_cfg (fst BDDalloc)).
Proof.
(* Goal: BDDneg_memo_OK (bs_of_cfg (@fst BDDconfig ad BDDalloc)) (negm_of_cfg (@fst BDDconfig ad BDDalloc)) *)
  rewrite BDDalloc_negm_same.  apply nodes_preserved_neg_memo_OK with (bs := bs_of_cfg new_cfg).
(* Goal: nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) *)
  exact BDDalloc_preserves_nodes.  exact (bs_of_cfg_OK _ new_cfg_OK).
(* Goal: BDDstate_OK (bs_of_cfg (@fst BDDconfig ad BDDalloc)) *)
(* Goal: BDDuniv_memo_OK (bs_of_cfg new_cfg) (um_of_cfg new_cfg) *)
  exact BDDalloc_keeps_state_OK.  exact (negm_of_cfg_OK _ new_cfg_OK).
Qed.

Lemma BDDalloc_keeps_or_memo_OK :
 BDDor_memo_OK (bs_of_cfg (fst BDDalloc)) (orm_of_cfg (fst BDDalloc)).
Proof.
(* Goal: BDDor_memo_OK (bs_of_cfg (@fst BDDconfig ad BDDalloc)) (orm_of_cfg (@fst BDDconfig ad BDDalloc)) *)
  rewrite BDDalloc_orm_same.  apply nodes_preserved_or_memo_OK with (bs := bs_of_cfg new_cfg).
(* Goal: nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) *)
  exact BDDalloc_preserves_nodes.  exact (bs_of_cfg_OK _ new_cfg_OK).
(* Goal: BDDstate_OK (bs_of_cfg (@fst BDDconfig ad BDDalloc)) *)
(* Goal: BDDuniv_memo_OK (bs_of_cfg new_cfg) (um_of_cfg new_cfg) *)
  exact BDDalloc_keeps_state_OK.  exact (orm_of_cfg_OK _ new_cfg_OK).
Qed.

Lemma BDDalloc_keeps_univ_memo_OK :
 BDDuniv_memo_OK (bs_of_cfg (fst BDDalloc)) (um_of_cfg (fst BDDalloc)).
Proof.
(* Goal: BDDuniv_memo_OK (bs_of_cfg (@fst BDDconfig ad BDDalloc)) (um_of_cfg (@fst BDDconfig ad BDDalloc)) *)
  rewrite BDDalloc_um_same.  apply nodes_preserved_um_OK with (bs := bs_of_cfg new_cfg).
(* Goal: nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) *)
  exact BDDalloc_preserves_nodes.  exact (bs_of_cfg_OK _ new_cfg_OK).
(* Goal: BDDstate_OK (bs_of_cfg (@fst BDDconfig ad BDDalloc)) *)
(* Goal: BDDuniv_memo_OK (bs_of_cfg new_cfg) (um_of_cfg new_cfg) *)
  exact BDDalloc_keeps_state_OK.  exact (um_of_cfg_OK _ new_cfg_OK).
Qed.

(* The following results are used for BDDmake *)
Lemma BDDalloc_keeps_config_OK : BDDconfig_OK (fst BDDalloc).
Proof.
(* Goal: and (BDDor_memo_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@fst BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)))))))) (BDDuniv_memo_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)))))))) *)
  unfold BDDconfig_OK in |- *.  split.  apply BDDalloc_keeps_state_OK.  split.
(* Goal: and (BDDor_memo_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@fst BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)))))))) (BDDuniv_memo_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)))))))) *)
  exact BDDalloc_keeps_sharing_OK.  split.  exact BDDalloc_keeps_free_list_OK.  
(* Goal: and (BDDor_memo_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@fst BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)))))))) (BDDuniv_memo_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)))))))) *)
  split.  exact BDDalloc_keeps_cnt_OK.  split.
(* Goal: and (BDDor_memo_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@fst BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)))))))) (BDDuniv_memo_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)))))))) *)
  exact BDDalloc_keeps_neg_memo_OK.  split.  exact BDDalloc_keeps_or_memo_OK.
(* Goal: BDDuniv_memo_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDor_memo BDDuniv_memo (@snd BDDneg_memo (prod BDDor_memo BDDuniv_memo) (@snd ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)) (@snd BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))) (@snd BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo)))) (@snd BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc))))))) *)
  exact BDDalloc_keeps_univ_memo_OK.
Qed.
 
Lemma BDDalloc_preserves_used_nodes :
 used_nodes_preserved cfg (fst BDDalloc) ul.
Proof.
(* Goal: BDDconfig_OK cfg *)
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  apply used_nodes_preserved_trans with (cfg2 := new_cfg).  assumption.  
(* Goal: used_nodes_preserved cfg new_cfg ul *)
(* Goal: used_nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) ul *)
  exact new_cfg_nodes_preserved.  apply nodes_preserved_used_nodes_preserved.
(* Goal: nodes_preserved new_cfg (@fst BDDconfig ad BDDalloc) *)
  exact BDDalloc_preserves_nodes.
Qed.

Lemma BDDalloc_node_OK : config_node_OK (fst BDDalloc) (snd BDDalloc).
Proof.
(* Goal: BDD_OK (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDconfig ad BDDalloc) *)
  unfold config_node_OK in |- *.  apply BDD_OK_node_OK.  apply BDDalloc_BDD_OK.
Qed.

Lemma BDDallocGet :
 MapGet _ (fst (fst BDDalloc)) (snd BDDalloc) = Some (x, (l, r)).
Proof.
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (MapGet (prod BDDvar (prod ad ad)) (@fst BDDstate (prod BDDsharing_map (prod BDDfree_list (prod ad (prod BDDneg_memo (prod BDDor_memo BDDuniv_memo))))) (@fst BDDconfig ad BDDalloc)) (@snd BDDconfig ad BDDalloc)) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) *)
  rewrite (BDDalloc_lemma_1 (snd BDDalloc)).
(* Goal: @eq (option (prod BDDvar (prod ad ad))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) (@Some (prod BDDvar (prod ad ad)) (@pair BDDvar (prod ad ad) x (@pair ad ad l r))) *)
  rewrite (Neqb_correct (snd BDDalloc)).  reflexivity.
Qed.

End BDD_alloc.