proposition: Lemma BDDshare_put_puts : forall (share : BDDsharing_map) (x : BDDvar) (l r counter : ad), BDDshare_lookup (BDDshare_put share x l r counter) x l r = Some counter.
proof: Proof. intros share x l r counter. unfold BDDshare_put in |- *. elim (option_sum _ (MapGet (Map (Map ad)) share l)). intro y. elim y. clear y. intros x0 y. rewrite y. elim (option_sum _ (MapGet (Map ad) x0 r)). intros y0. elim y0. clear y0. intros x1 y0. rewrite y0. unfold BDDshare_lookup in |- *. rewrite (MapPut_semantics _ share l (MapPut (Map ad) x0 r (MapPut ad x1 x counter)) l) . cut (N.eqb l l = true). intros H. rewrite H. rewrite (MapPut_semantics _ x0 r (MapPut ad x1 x counter) r). cut (N.eqb r r = true). intros H0. rewrite H0. rewrite (MapPut_semantics _ x1 x counter x). cut (N.eqb x x = true). intros H1. rewrite H1. trivial. apply Neqb_correct. apply Neqb_correct. apply Neqb_correct. intros y0. rewrite y0. unfold BDDshare_lookup in |- *. rewrite (MapPut_semantics (Map (Map ad)) share l (MapPut (Map ad) x0 r (MapPut ad (newMap ad) x counter)) l) . rewrite (Neqb_correct l). rewrite (MapPut_semantics (Map ad) x0 r (MapPut ad (newMap ad) x counter) r) . rewrite (Neqb_correct r). rewrite (MapPut_semantics ad (newMap ad) x counter x). rewrite (Neqb_correct x). trivial. intros y. rewrite y. unfold BDDshare_lookup in |- *. simpl in |- *. rewrite (MapPut_semantics (Map (Map ad)) share l (M1 (Map ad) r (M1 ad x counter)) l). rewrite (Neqb_correct l). simpl in |- *. rewrite (Neqb_correct r). simpl in |- *. rewrite (Neqb_correct x). trivial. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat