proposition: Lemma BDDvar_ordered_high_3 : forall (cfg : BDDconfig) (node1 node2 : ad), BDDconfig_OK cfg -> is_internal_node cfg node1 -> is_internal_node cfg node2 -> BDDcompare (var cfg node2) (var cfg node1) = Datatypes.Lt -> BDDcompare (BDDvar_max (var cfg (high cfg node1)) (var cfg node2)) (var cfg node1) = Datatypes.Lt.
proof: Proof. intros cfg node1 node2 H H0 H1 H2. rewrite (BDDvar_max_comm (var cfg (high cfg node1)) (var cfg node2)). apply BDDvar_ordered_high_2. assumption. assumption. assumption. 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