proposition: Lemma no_duplicate_node : forall (cfg : BDDconfig) (node1 node2 : ad), BDDconfig_OK cfg -> is_internal_node cfg node1 -> is_internal_node cfg node2 -> var cfg node1 = var cfg node2 -> high cfg node1 = high cfg node2 -> low cfg node1 = low cfg node2 -> node1 = node2.
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y. elim y; clear y; intros share counter. intros node1 node2 H H0 H1 H2 H3 H4. inversion H0. inversion H5. inversion H6. inversion H1. inversion H8. inversion H9. unfold var in H2; rewrite H7 in H2; rewrite H10 in H2. unfold high in H3; rewrite H7 in H3; rewrite H10 in H3. unfold low in H4; rewrite H7 in H4; rewrite H10 in H4. cut (BDDshare_lookup share x x0 x1 = Some node1). cut (BDDshare_lookup share x2 x3 x4 = Some node2). intros H11 H12. rewrite H2 in H12. rewrite H3 in H12. rewrite H4 in H12. rewrite H11 in H12. injection H12. intro H13. rewrite H13; reflexivity. elim H. intros H11 H12. apply (proj2 (proj1 H12 x2 x3 x4 node2)). assumption. elim H; intros. apply (proj2 (proj1 H12 x x0 x1 node1)). assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2