proposition: Lemma BDDor_memo_lookup_semantics : forall (memo : BDDor_memo) (node1 node2 node node1' node2' : ad), BDDor_memo_lookup (BDDor_memo_put memo node1 node2 node) node1' node2' = (if N.eqb node1 node1' && N.eqb node2 node2' then Some node else BDDor_memo_lookup memo node1' node2').
proof: Proof. intros memo node1 node2 node node1' node2'. unfold BDDor_memo_lookup, BDDor_memo_put in |- *. rewrite (MapPut_semantics (Map ad) memo node1 (MapPut ad match MapGet (Map ad) memo node1 with | None => newMap ad | Some y => y end node2 node) node1'). elim (sumbool_of_bool (N.eqb node1 node1')); intro y. rewrite y. rewrite (MapPut_semantics ad match MapGet (Map ad) memo node1 with | None => newMap ad | Some y => y end node2 node node2'). elim (sumbool_of_bool (N.eqb node2 node2')). intro y0. rewrite y0. simpl in |- *. reflexivity. intro y0. rewrite y0. simpl in |- *. elim (option_sum _ (MapGet (Map ad) memo node1)). intro y1. inversion y1. rewrite H. cut (node1 = node1'). intro H0. rewrite <- H0. rewrite H. reflexivity. apply Neqb_complete; assumption. intro y1. rewrite y1. cut (node1 = node1'). intro H. rewrite <- H. rewrite y1. simpl in |- *. reflexivity. apply Neqb_complete; assumption. rewrite y. simpl in |- *. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1 bdd5_2