proposition: Lemma BDDcompare_max_1_2 : forall x1 x2 y1 y2 : BDDvar, BDDcompare x1 x2 = Datatypes.Lt -> BDDcompare y1 y2 = Datatypes.Lt -> BDDcompare (BDDvar_max x1 y1) (BDDvar_max x2 y2) = Datatypes.Lt.
proof: Proof. unfold BDDvar_max in |- *. unfold BDDvar_le in |- *. unfold Nleb in |- *. intros x1 x2 y1 y2 H H0. elim (sumbool_of_bool (leb (nat_of_N x1) (nat_of_N y1))). intro y. rewrite y. elim (sumbool_of_bool (leb (nat_of_N x2) (nat_of_N y2))). intro y0. rewrite y0. assumption. intro y0. rewrite y0. apply BDDlt_compare. apply lt_trans with (m := nat_of_N y2). apply BDDcompare_lt. assumption. apply leb_complete_conv. assumption. intro y. rewrite y. elim (sumbool_of_bool (leb (nat_of_N x2) (nat_of_N y2))). intro y0. rewrite y0. apply BDDlt_compare. apply lt_le_trans with (m := nat_of_N x2). apply BDDcompare_lt. assumption. apply leb_complete. assumption. intro y0. rewrite y0. assumption. 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