proposition: Lemma BDDvar_ordered_high_1 : forall (cfg : BDDconfig) (node1 node2 : ad), BDDconfig_OK cfg -> is_internal_node cfg node1 -> is_internal_node cfg node2 -> is_internal_node cfg (high cfg node1) \/ is_internal_node cfg (high cfg node2) -> BDDcompare (BDDvar_max (var cfg (high cfg node1)) (var cfg (high cfg node2))) (BDDvar_max (var cfg node1) (var cfg node2)) = Datatypes.Lt.
proof: Proof. intros cfg node1 node2 H H0 H1 H2. cut (config_node_OK cfg (high cfg node1)). cut (config_node_OK cfg (high cfg node2)). intros H3 H4. elim H2; intro. cut (BDDcompare (var cfg (high cfg node1)) (var cfg node1) = Datatypes.Lt). intro H6. elim H3; intro. rewrite H7. unfold var at 2 in |- *. rewrite (config_OK_zero cfg H). unfold BDDzero in |- *. apply BDDvar_max_lemma_1. assumption. elim H7; intro. rewrite H8. unfold var at 2 in |- *. rewrite (config_OK_one cfg H). unfold BDDzero in |- *. apply BDDvar_max_lemma_1. assumption. apply BDDcompare_max_1_2. assumption. apply BDDvar_ordered_high. assumption. assumption. apply in_dom_is_internal. assumption. apply BDDvar_ordered_high. assumption. assumption. assumption. elim H4; intro. rewrite H6. unfold var at 1 in |- *. rewrite (config_OK_zero cfg H). unfold BDDzero in |- *. rewrite (BDDvar_max_comm N0 (var cfg (high cfg node2))). rewrite (BDDvar_max_comm (var cfg node1) (var cfg node2)). apply BDDvar_max_lemma_1. apply BDDvar_ordered_high. assumption. assumption. assumption. elim H6; intro. rewrite H7. unfold var at 1 in |- *. rewrite (config_OK_one cfg H). unfold BDDzero in |- *. rewrite (BDDvar_max_comm N0 (var cfg (high cfg node2))). rewrite (BDDvar_max_comm (var cfg node1) (var cfg node2)). apply BDDvar_max_lemma_1. apply BDDvar_ordered_high. assumption. assumption. assumption. apply BDDcompare_max_1_2. apply BDDvar_ordered_high. assumption. assumption. apply in_dom_is_internal; assumption. apply BDDvar_ordered_high. assumption. assumption. assumption. apply high_OK. assumption. assumption. apply high_OK. 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