proposition: Lemma BDDvar_independent_low : forall (cfg : BDDconfig) (node : ad), BDDconfig_OK cfg -> is_internal_node cfg node -> bool_fun_independent (bool_fun_of_BDD cfg (low cfg node)) (var cfg node).
proof: Proof. intros cfg node H H0. cut (config_node_OK cfg (low cfg node)). intros H1. elim H1. intro H2. rewrite H2. apply bool_fun_independent_zero. assumption. intro H2. elim H2; intro. rewrite H3; apply bool_fun_independent_one; assumption. cut (is_internal_node cfg (low cfg node)). intro H4. apply BDDvar_independent_1 with (n := nat_of_N (var cfg (low cfg node))). assumption. apply in_dom_is_internal. assumption. reflexivity. apply BDDvar_ordered_low. assumption. assumption. assumption. apply in_dom_is_internal. assumption. apply low_OK. assumption. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2