proposition: Lemma bool_fun_of_BDD_1_semantics_1 : forall cfg : BDDconfig, BDDconfig_OK cfg -> forall bound : nat, bool_fun_of_BDD_1 cfg BDDzero bound = bool_fun_zero /\ bool_fun_of_BDD_1 cfg BDDone bound = bool_fun_one /\ (forall node : ad, is_internal_node cfg node -> nat_of_N (var cfg node) < bound -> bool_fun_of_BDD_1 cfg node bound = (fun vb : var_binding => if vb (var cfg node) then bool_fun_of_BDD_1 cfg (high cfg node) (pred bound) vb else bool_fun_of_BDD_1 cfg (low cfg node) (pred bound) vb)).
proof: Proof. intro cfg. elim cfg. clear cfg. intros bs y. elim y. clear y. intros share counter. intro H. simple induction bound. split. unfold bool_fun_of_BDD_1 in |- *. elim H. intros H0 H1. elim H0. intros H2 H3. simpl in |- *. rewrite H2. trivial. split. elim H. intros H0 H1. elim H0. intros H2 H3. unfold bool_fun_of_BDD_1 in |- *. simpl in |- *. rewrite (proj1 H3). trivial. unfold is_internal_node in |- *. intro node. intro H0. unfold var in |- *. elim H0. clear H0. intros x H0. elim H0. clear H0. intros l H0. elim H0. clear H0. intros r H0. rewrite H0. intro H1. cut (~ nat_of_N x < 0). unfold not in |- *. tauto. apply lt_n_O. intros n H0. elim H. intros H1 H2. elim H1. intros H3 H4. elim H4. intros H5 H6. split. unfold bool_fun_of_BDD_1 in |- *. simpl in |- *. rewrite H3. trivial. split. unfold bool_fun_of_BDD_1 in |- *. simpl in |- *. rewrite H5. trivial. intro node. intro H7. unfold is_internal_node in H7. elim H7. clear H7. intro x. intro H7. elim H7. clear H7. intro x0. intro H7. elim H7. clear H7. intro x1. intro H7. unfold var in |- *. rewrite H7. intro H8. unfold pred in |- *. unfold bool_fun_of_BDD_1 at 1 in |- *. rewrite H7. unfold high in |- *. rewrite H7. unfold low in |- *. rewrite H7. trivial. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1