proposition: Lemma BDDvar_ordered_high_2 : forall (cfg : BDDconfig) (node1 node2 : ad), BDDconfig_OK cfg -> is_internal_node cfg node1 -> is_internal_node cfg node2 -> BDDcompare (var cfg node1) (var cfg node2) = Datatypes.Lt -> BDDcompare (BDDvar_max (var cfg node1) (var cfg (high cfg node2))) (var cfg node2) = Datatypes.Lt.
proof: Proof. intros cfg node1 node2 H H0 H1 H2. cut (var cfg node2 = BDDvar_max (var cfg node2) (var cfg node2)). intro H3. rewrite H3. apply BDDcompare_max_1_2. assumption. cut (config_node_OK cfg (high cfg node2)). intro H4. elim H4; intro. rewrite H5. unfold var at 1 in |- *. rewrite (config_OK_zero cfg H). unfold BDDzero in |- *. apply BDDcompare_z_nz. apply INFERIEUR_neq_O with (x := var cfg node1). assumption. elim H5; intro. rewrite H6. unfold var at 1 in |- *. rewrite (config_OK_one cfg H). unfold BDDzero in |- *. apply BDDcompare_z_nz. apply INFERIEUR_neq_O with (x := var cfg node1). assumption. apply BDDvar_ordered_high. assumption. assumption. apply in_dom_is_internal. assumption. apply high_OK. assumption. assumption. rewrite (BDDvar_max_x_x (var cfg node2)). 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