proposition: Lemma bool_fun_of_BDD_semantics : forall cfg : BDDconfig, BDDconfig_OK cfg -> bool_fun_of_BDD cfg BDDzero = bool_fun_zero /\ bool_fun_of_BDD cfg BDDone = bool_fun_one /\ (forall node : ad, is_internal_node cfg node -> bool_fun_of_BDD cfg node = (fun vb : var_binding => if vb (var cfg node) then bool_fun_of_BDD cfg (high cfg node) vb else bool_fun_of_BDD cfg (low cfg node) vb)).
proof: Proof. intros cfg H. unfold bool_fun_of_BDD in |- *. split. apply (proj1 (bool_fun_of_BDD_1_semantics_1 cfg H (S (nat_of_N (var cfg BDDzero))))). split. apply (proj1 (proj2 (bool_fun_of_BDD_1_semantics_1 cfg H (S (nat_of_N (var cfg BDDone)))))). intros node H0. cut (nat_of_N (var cfg node) < S (nat_of_N (var cfg node))). intro H1. rewrite (proj2 (proj2 (bool_fun_of_BDD_1_semantics_1 cfg H (S (nat_of_N (var cfg node))))) node H0 H1). cut (bool_fun_of_BDD_1 cfg (high cfg node) (pred (S (nat_of_N (var cfg node)))) = bool_fun_of_BDD_1 cfg (high cfg node) (S (nat_of_N (var cfg (high cfg node))))). intro H2. cut (bool_fun_of_BDD_1 cfg (low cfg node) (pred (S (nat_of_N (var cfg node)))) = bool_fun_of_BDD_1 cfg (low cfg node) (S (nat_of_N (var cfg (low cfg node))))). intro H3. rewrite H2. rewrite H3. trivial. unfold pred in |- *. elim (option_sum _ (MapGet _ (fst cfg) (low cfg node))). intros y. elim y. clear y. intro x. elim x. clear x. intros x y. elim y. clear y. intros l r. intro y. cut (nat_of_N (var cfg (low cfg node)) < nat_of_N (var cfg node)). intro H3. rewrite (bool_fun_of_BDD_1_change_bound cfg H (nat_of_N (var cfg node)) (low cfg node) H3). trivial. apply BDDcompare_lt. apply BDDvar_ordered_low. assumption. assumption. unfold is_internal_node in |- *. split with x. split with l. split with r. assumption. intros y. apply bool_fun_of_BDD_1_semantics_2. assumption. unfold pred in |- *. elim (option_sum _ (MapGet _ (fst cfg) (high cfg node))). intros y. elim y. clear y. intro x. elim x. clear x. intros x y. elim y. clear y. intros l r. intro y. cut (nat_of_N (var cfg (high cfg node)) < nat_of_N (var cfg node)). intro H2. rewrite (bool_fun_of_BDD_1_change_bound cfg H (nat_of_N (var cfg node)) (high cfg node) H2). trivial. apply BDDcompare_lt. apply BDDvar_ordered_high. assumption. assumption. unfold is_internal_node in |- *. split with x. split with l. split with r. assumption. intros y. apply bool_fun_of_BDD_1_semantics_2. assumption. unfold lt in |- *. auto. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1