(in-package "ACL2")

(include-book "bdd-mgr")

#|

    bdd-spec.lisp
    ~~~~~~~~~~~~~

In this book we will develop the theory of the function ite-spec,
a much simpler version of the function ite-bdd given in the bdd-mgr
book. This book consists of 5 main parts:

1. prove robdds are propositionally equivalent iff they are
structurally equivalent.

2. prove that ite-spec is semantically equivalent to
propositional if-then-else.

3. prove 4 reductions of ite-spec which are used in ite-bdd
to short-circuit the evaluation of 4 input cases.

4. prove that when ite-spec is given robdds, it returns an robdd.

5. prove several important congruences about structural-equivalence.

|#

;;;; this book only contains definitions used for proving theorems
;;;; about the "executable" functions in bdd-mr.lisp. Thus, we do not
;;;; expect to execute the functions in this book and as such, we will
;;;; not go through the overhead of verifying their guards. 

(set-verify-guards-eagerness 0)

;;;;; most of the recursive functions defined in this book will recur
;;;;; by traversing the the tree structure of bdds. so, we will recall
;;;;; a couple of simple theorems here and actually hide the definition
;;;;; of acl2-count.

(local 
(defthm consp-<-acl2-count-bdd-else
  (implies (consp x)
	   (< (acl2-count (b-else x))
	      (acl2-count x)))
  :rule-classes :linear))

(local 
(defthm consp-<-acl2-count-bdd-then
  (implies (consp x)
	   (< (acl2-count (b-then x))
	      (acl2-count x)))
  :rule-classes :linear))

(local 
(defthm acl2-count-consp->0
  (implies (consp x)
	   (< 0 (acl2-count x)))
  :rule-classes :linear))

(in-theory (disable acl2-count))

#|----------------------------------------------------------------------------|#

;;;;;;;;;;;;;;;;;;; BEGIN PART 1. ;;;;;;;;;;;;;;;;;;;;;;;;

;;;; we now define structural equivalence for bdds. This function
;;;; is essentially 'equal except that it ignores the (car) of each
;;;; node (this is where we store the unique identifiers in the
;;;; stobj implementation) and compares atoms using iff.

(defun bdd= (x y)
  (cond ((and (atom x) (atom y)) (iff x y))
        ((or (atom x) (atom y)) nil)
        (t (and (equal (b-test x) (b-test y))
                (bdd= (b-then x) (b-then y))
                (bdd= (b-else x) (b-else y))))))

(local
(defthm bdd=-is-reflexive (bdd= x x)))

(local
(defthm bdd=-is-symmetric
  (implies (bdd= x y) (bdd= y x))))

(local
(defthm bdd=-is-transitive
  (implies (and (bdd= x y) (bdd= y z))
           (bdd= x z))))

(defequiv bdd=)

;;;; we will use the following wrapper function for (if) in order to
;;;; use the function in theorems and rewrite rules without having
;;;; ACL2 reducing it propositionally.

(defun prop-if (x y z) (if x y z))

;;;; we prove a few useful theorems about prop-if (and in fact (if)).

(defcong iff iff (prop-if x y z) 1)

(defthm prop-if-reduction-t
  (equal (prop-if t x y) x))

(defthm prop-if-reduction-nil
  (equal (prop-if nil x y) y))

(defthm prop-if-reduction-equal
  (implies (equal x y)
           (equal (prop-if f x y) y)))

;;;; (prop-look v a) is essentially (cdr (assoc v a))

(defmacro bool (x) `(if ,x t nil))

(defun prop-look (v a)
  (if (atom a) nil
    (if (equal v (caar a))
        (bool (cdar a))
      (prop-look v (cdr a)))))

;;;; (bdd-ev x a) evaluates the bdd x under the propositional assignment a

(defun bdd-ev (x a)
  (if (atom x) (bool x)
    (prop-if (prop-look (b-test x) a)
             (bdd-ev (b-then x) a)
             (bdd-ev (b-else x) a))))

;;;; (1) the following simple congruence assures that two bdds x and y such that
;;;; (bdd= x y), satisfy the relation (forall (a) (equal (bdd-ev x a) (bdd-ev y a)))

(defcong bdd= equal (bdd-ev x a) 1)

;;;; we now show that converse holds in the case where x and y are robdds (reduced
;;;; ordered binary decision diagrams). Thus ACL2 will agree with [Bryant86]. Actually,
;;;; we need to extend the notion of bdd-ev (which we do later in this book) to allow
;;;; for tests which are non-variables. We essentially use if-normalizing to show that
;;;; any if expression can be reduced to one where all tests are variables identifiers.

(defun bdd-test> (x y) 
  (or (atom y)
      (> (b-test x) 
         (b-test y))))

(defun robdd (x)
  (or (atom x)
      (and (bdd-test> x (b-then x))      ;;;; ORDERED
           (bdd-test> x (b-else x))
           (not (bdd= (b-then x)         ;;;; REDUCED
                      (b-else x)))
           (pnatp (b-test x))
           (robdd (b-then x))
           (robdd (b-else x)))))

;;;; in order to show the converse to (1), we need to construct a witness which satisfies
;;;; (not (equal (bdd-ev x witness) (bdd-ev y witness))) when (not (bdd= x y)) and x and y
;;;; are robdds. the following function builds this witness as a function of x and y.

(defun robdd-witness (x y)
  (declare (xargs :measure 
                  (+ (acl2-count x) (acl2-count y))))
  (cond
   ((and (atom x) (atom y)) ())
   ((and (consp y)
         (or (atom x)
             (> (b-test y) (b-test x))))
    (if (bdd= x (b-then y))
        (cons (cons (b-test y) nil)
              (robdd-witness x (b-else y)))
      (cons (cons (b-test y) t)
            (robdd-witness x (b-then y)))))
   ((or (atom y)
        (> (b-test x) (b-test y)))
    (if (bdd= (b-then x) y)
        (cons (cons (b-test x) nil)
              (robdd-witness (b-else x) y))
      (cons (cons (b-test x) t)
            (robdd-witness (b-then x) y))))
   (t 
    (if (bdd= (b-then x) (b-then y))
        (cons (cons (b-test x) nil)
              (robdd-witness (b-else x) (b-else y)))
      (cons (cons (b-test x) t)
            (robdd-witness (b-then x) (b-then y)))))))

;;;; the following predicate (independent-of v x) is true when 
;;;; the bdd x is not dependent on the variable v

(defun independent-of (v x)
  (or (atom x)
      (and (not (equal (b-test x) v))
           (independent-of v (b-then x))
           (independent-of v (b-else x)))))

;;;; we now relate independence to robdd structures...

(local
(defthm robdd-natp-test-forward-chain
  (implies (and (robdd x) (consp x))
           (natp (b-test x)))
  :rule-classes :forward-chaining))


(local
(defthm robdd-independence-setup
  (implies (and (robdd x)
                (or (atom x)
                    (> v (b-test x))))
           (independent-of v x))
  :hints (("Goal" :induct (independent-of v x)))))

;;;; ...and wrap this notion into a decomposition at a given robdd node x

(local
(defthm robdd-independence
  (implies (and (robdd x) (consp x))
           (and (independent-of (b-test x) (b-then x))
                (independent-of (b-test x) (b-else x))))))

;;;; we also need to show that bdd-ev can "skip" over independent variables

(local
(defthm bdd-ev-independence
  (implies (independent-of v x)
           (equal (bdd-ev x (cons (cons v d) a))
                  (bdd-ev x a)))))

;;;; the above independence properties allow us to simplify bdd-ev's to not
;;;; only deconstruct the bdd x, but also drop the variable bound to the 
;;;; test position in x. NOTE, a more general theorem could be used here where
;;;; the binding to (b-test x) is forgotten from the assignment. The following
;;;; is sufficient for our purposes since our witness function will construct 
;;;; the assignment in a specific manner..

(local
(defthm bdd-ev-of-robdd
  (implies (and (robdd x) (consp x)
                (equal (b-test x) v))
           (equal (bdd-ev x (cons (cons v d) a))
                  (if d (bdd-ev (b-then x) a)
                    (bdd-ev (b-else x) a))))))

;;;; the following forward chaining is not necessary in order for our saturation
;;;; theorem to succeed, but it is useful in helping ACL2 avoid unnecessary forcing
;;;; induced by the implication:
;;;;      (implies (and (force (acl2-numberp x)) 
;;;;                    (force (acl2-numberp y))
;;;;                    (>= x y) (>= y x))
;;;;               (equal x y))


;;;; we now prove our saturation theorem. ACL2 does a wonderful job on this theorem
;;;; breaking it up into 18 subgoals and discharging each of them in an orderly fashion :)

(defthm robdd-bdd=-saturates-bdd-ev-=
  (implies (and (robdd x) (robdd y) 
                (not (bdd= x y)))
           (not (equal (bdd-ev x (robdd-witness x y))
                       (bdd-ev y (robdd-witness x y))))))

;;;; so, now we have that for robdds x and y, that (bdd= x y) is the same
;;;; relation as (forall (a) (equal (bdd-ev x a) (bdd-ev y a)))


;;;;;;;;;;;;;;;;;;;; END PART 1. ;;;;;;;;;;;;;;;;;;;;;;;;;

#|----------------------------------------------------------------------------|#

;;;;;;;;;;;;;;;;;;; BEGIN PART 2. ;;;;;;;;;;;;;;;;;;;;;;;;

;;;; WE now move to the definition of our specification of ite, namely the function ite-spec.
;;;; We will show that this function preserves bdd-ev and given robdds, it returns robdds.
;;;; We will later show that under the right invariant that our stobj implementation of bdd-ite
;;;; returns a bdd which is bdd= to the bdd returned by ite-spec.

;;;; top-var, else-node, then-node, b-node are defined in bdd-mgr.lisp

(in-theory (enable top-var then-node else-node b-node))

(defun ite-spec (f g h)
  (declare (xargs :measure (+ (acl2-count f) 
			      (acl2-count g) 
			      (acl2-count h))))
  (if (atom f) (if f g h)
    (let ((v (top-var f g h)))
      (let ((then (ite-spec (then-node f v) 
                            (then-node g v) 
                            (then-node h v)))
            (else (ite-spec (else-node f v)
                            (else-node g v)
                            (else-node h v))))
        (if (bdd= then else) then
          (b-node 'if v then else))))))

(local
(defthm top-var->=-f-test
  (>= (top-var f g h) (b-test f))
  :rule-classes :linear))

(local
(defthm top-var->=-g-test
  (implies (consp g) 
           (>= (top-var f g h) (b-test g)))
  :rule-classes :linear))

(local
(defthm top-var->=-h-test
  (implies (consp h)
           (>= (top-var f g h) (b-test h)))
  :rule-classes :linear))

(local
(defthm ite-main-lemma-setup
  (implies (and (>= v (b-test f))
                (or (>= v (b-test g))
                    (atom g))
                (or (>= v (b-test h))
                    (atom h)))
           (equal (prop-if (prop-look v a)
                           (prop-if (bdd-ev (then-node f v) a)
                                    (bdd-ev (then-node g v) a)
                                    (bdd-ev (then-node h v) a))
                           (prop-if (bdd-ev (else-node f v) a)
                                    (bdd-ev (else-node g v) a)
                                    (bdd-ev (else-node h v) a)))
                  (prop-if (bdd-ev f a) 
                           (bdd-ev g a)
                           (bdd-ev h a))))
  :rule-classes nil))

(local
(defthm ite-main-lemma
  (let ((v (top-var f g h)))
    (equal (prop-if (prop-look v a)
                    (prop-if (bdd-ev (then-node f v) a)
                             (bdd-ev (then-node g v) a)
                             (bdd-ev (then-node h v) a))
                    (prop-if (bdd-ev (else-node f v) a)
                             (bdd-ev (else-node g v) a)
                             (bdd-ev (else-node h v) a)))
           (prop-if (bdd-ev f a) 
                    (bdd-ev g a)
                    (bdd-ev h a))))
  :hints (("Goal" 
           :use (:instance ite-main-lemma-setup 
                           (v (top-var f g h)))
           :in-theory (disable top-var prop-if 
                               then-node else-node)))))

(local
(defthm prop-if-equal-with-ite-main
  (let ((v (top-var f g h)))
    (implies (equal (prop-if (bdd-ev (then-node f v) a)
                             (bdd-ev (then-node g v) a)
                             (bdd-ev (then-node h v) a))
                    (prop-if (bdd-ev (else-node f v) a)
                             (bdd-ev (else-node g v) a)
                             (bdd-ev (else-node h v) a)))
             (equal (prop-if (bdd-ev (else-node f v) a)
                             (bdd-ev (else-node g v) a)
                             (bdd-ev (else-node h v) a))
                    (prop-if (bdd-ev f a) 
                             (bdd-ev g a)
                             (bdd-ev h a)))))
  :hints (("Goal"
           :in-theory (disable ite-main-lemma
                               then-node else-node
                               prop-if top-var)
           :use (:instance ite-main-lemma)))))

(defthm ite-spec-preserves-bdd-ev
  (equal (bdd-ev (ite-spec f g h) a)
         (prop-if (bdd-ev f a) 
                  (bdd-ev g a) 
                  (bdd-ev h a)))
  :hints (("Goal" 
           :induct (ite-spec f g h)
           :in-theory (disable then-node else-node
                               prop-if top-var))))

;;;;;;;;;;;;;;;;;;;; END PART 2. ;;;;;;;;;;;;;;;;;;;;;;;;;

#|----------------------------------------------------------------------------|#

;;;;;;;;;;;;;;;;;;; BEGIN PART 3. ;;;;;;;;;;;;;;;;;;;;;;;;

;;;; we now prove a few reductions which we make use of in the implementation 
;;;; function ite-bdd in order to simplify ite calculations.

(local
(defthm ite-spec-reduction-1-free
  (implies (and (equal g (bdd-1))
                (equal h (bdd-0))
                (robdd f))
           (bdd= (ite-spec f g h) f))
  :hints (("Goal" :induct (ite-spec f g h)))
  :rule-classes nil))

(defthm ite-spec-reduction-1
  (implies (robdd f)
           (bdd= (ite-spec f (bdd-1) (bdd-0)) f))
  :hints (("Goal" :use (:instance  
                        ite-spec-reduction-1-free
                        (g (bdd-1)) (h (bdd-0))))))
(local 
(defthm then-node-atom
  (implies (atom x) (equal (then-node x v) x))))

(local
(defthm else-node-atom
  (implies (atom x) (equal (else-node x v) x))))

(defcong bdd= bdd= (then-node x v) 1)

(defcong bdd= bdd= (else-node x v) 1)

(local
(defthm bdd=-forward-chain-b-test
  (implies (bdd= x y) (equal (b-test x) (b-test y)))
  :rule-classes :forward-chaining))

(defthm robdd-then-node
  (implies (robdd x) (robdd (then-node x u))))

(defthm robdd-else-node
  (implies (robdd x) (robdd (else-node x u))))

(local
(defthm bdd=-back-chain
  (implies (and (consp x) (consp y)
                (bdd= (b-then x) (b-then y))
                (bdd= (b-else x) (b-else y)))
           (equal (bdd= x y)
                  (equal (b-test x) (b-test y))))))

(local
(defthm bdd=top-var-equal-1
  (implies (and (robdd f) (robdd g) (bdd= f g))
           (equal (top-var f g h)
                  (top-var f t h)))))

(defthm ite-spec-reduction-2
  (implies (and (robdd f) (robdd g) (robdd h)
                (bdd= f g))
           (bdd= (ite-spec f g h)
                 (ite-spec f (bdd-1) h)))
  :hints (("Goal" :induct (ite-spec f g h)
           :in-theory (disable top-var then-node else-node bdd=))
          ("Subgoal *1/1" :in-theory (enable bdd=)))
  :rule-classes nil)

(local
(defthm bdd=top-var-equal-2
  (implies (and (robdd f) (robdd h) (bdd= f h))
           (equal (top-var f g h)
                  (top-var f g nil)))))

(defthm ite-spec-reduction-3
  (implies (and (robdd f) (robdd h)
                (bdd= f h))
           (bdd= (ite-spec f g h)
                 (ite-spec f g (bdd-0))))
  :hints (("Goal" 
           :induct (ite-spec f g h)
           :in-theory (disable top-var then-node else-node bdd=))
          ("Subgoal *1/1"
           :in-theory (enable bdd=))))

(local
(defthm then-node-match
  (implies (consp g)
           (equal (then-node g (b-test g)) (b-then g)))))

(local
(defthm else-node-match
  (implies (consp g)
           (equal (else-node g (b-test g)) (b-else g)))))

(local
(defthm then-node-mismatch-non-atom
  (implies (and (consp g) (not (equal v (b-test g))))
           (equal (then-node g v) g))))

(local
(defthm else-node-mismatch-non-atom
  (implies (and (consp g) (not (equal v (b-test g))))
           (equal (else-node g v) g))))

(defthm ite-spec-reduction-4
  (implies (and (robdd g) (robdd h) (bdd= g h))
           (bdd= (ite-spec f g h) g))
  :hints (("Goal"
           :induct (ite-spec f g h)
           :in-theory (disable top-var then-node else-node bdd=))
          ("Subgoal *1/4"
           :cases ((atom g) 
                   (and (consp g) 
                        (equal (top-var f g h) (b-test g)))))
          ("Subgoal *1/3"
           :cases ((atom g) 
                   (and (consp g)
                        (equal (top-var f g h) (b-test g)))))))

;;;;;;;;;;;;;;;;;;;; END PART 3. ;;;;;;;;;;;;;;;;;;;;;;;;;

#|----------------------------------------------------------------------------|#

;;;;;;;;;;;;;;;;;;; BEGIN PART 4. ;;;;;;;;;;;;;;;;;;;;;;;;

;;;; we now want to (finally) show that if ite-spec is given robdds then it will return
;;;; robdds. this is important since we want to ensure that the relation bdd=
;;;; is always equivalent to propositional equivalence.

(local
(defthm top-var-is-pnatp
  (implies (and (robdd f) (robdd g) (robdd h)
                (consp f))
           (pnatp (top-var f g h)))
  :rule-classes ((:forward-chaining
                  :trigger-terms ((top-var f g h)))
                 :rewrite)))

(local
(defthm top-var-is-bounded
  (implies (and (> v (b-test f))
                (> v (b-test g))
                (> v (b-test h)))
           (> v (top-var f g h)))
  :rule-classes :linear))

(local
(defthm robdd-bounded-then-node
  (implies (and (robdd f) (pnatp v)
                (>= v (b-test f)))
           (> v (b-test (then-node f v))))
  :rule-classes ((:forward-chaining
                  :trigger-terms ((then-node f v)))
                 :linear)))

(local
(defthm robdd-bounded-else-node
  (implies (and (robdd f) (pnatp v)
                (>= v (b-test f)))
           (> v (b-test (else-node f v))))
  :rule-classes ((:forward-chaining
                  :trigger-terms ((else-node f v)))
                 :linear)))

(local
(defthm robdd-constrained-then-node
  (implies (robdd f)
           (>= (b-test f)
               (b-test (then-node f v))))
  :rule-classes :linear))

(local
(defthm robdd-constrained-else-node
  (implies (robdd f)
           (>= (b-test f)
               (b-test (else-node f v))))
  :rule-classes :linear))

(local
(defthm ite-spec-is-bounded-then
  (implies (and (> v (b-test f))
                (> v (b-test g))
                (> v (b-test h))
                (pnatp v)
                (robdd f) (robdd g) (robdd h))
           (> v (b-test (ite-spec f g h))))
  :hints (("Goal" 
           :induct (ite-spec f g h)
           :in-theory (disable then-node else-node top-var)))
  :rule-classes ((:forward-chaining
                  :trigger-terms ((ite-spec f g h)))
                 :linear)))

(local
(defthm top-var-bounds-b-test-f
  (implies (and (consp f) (robdd f))
           (and (>= (top-var f g h)
                    (b-test f))
                (>= (top-var f g h)
                    (b-test g))
                (>= (top-var f g h)
                    (b-test h))))
  :rule-classes ((:forward-chaining
                  :trigger-terms ((top-var f g h)))
                 :linear)))

(local
(defthm ite-spec-then-node
  (let ((v (top-var f g h)))
    (implies (and (consp f) (robdd f)
                  (robdd g) (robdd h))
             (> v (b-test (ite-spec (then-node f v)
                                    (then-node g v)
                                    (then-node h v))))))))

(local
(defthm ite-spec-else-node
  (let ((v (top-var f g h)))
    (implies (and (consp f) (robdd f)
                  (robdd g) (robdd h))
             (> v (b-test (ite-spec (else-node f v)
                                    (else-node g v)
                                    (else-node h v))))))))

(defthm ite-spec-returns-robdds
  (implies (and (robdd f) (robdd g) (robdd h))
           (robdd (ite-spec f g h)))
  :hints (("Goal" :in-theory (disable top-var then-node else-node))))


;;;;;;;;;;;;;;;;;;;; END PART 4. ;;;;;;;;;;;;;;;;;;;;;;;;;

#|----------------------------------------------------------------------------|#

;;;;;;;;;;;;;;;;;;; BEGIN PART 5. ;;;;;;;;;;;;;;;;;;;;;;;;

;;;; we finish this book with some congruence relations which let us
;;;; replace bdd= items in answering the question if something
;;;; is an robdd, in the context of ite-spec, etc..

(local 
(defthm bdd=-bdd-test>-rewrite
  (implies (bdd= x y)
           (equal (bdd-test> z x)
                  (bdd-test> z y)))))

(local
(defthm bdd=-atom-implies
  (implies (and (bdd= x y) (atom x))
           (atom y))))

(local
(defthm bdd=-implies-equal-b-test
  (implies (bdd= x y)
           (equal (b-test x) (b-test y)))))

(local
(defthm bdd=-implies-bdd=-b-then
  (implies (bdd= x y)
           (bdd= (b-then x) (b-then y)))))

(local
(defthm bdd=-implies-bdd=-b-else
  (implies (bdd= x y)
           (bdd= (b-else x) (b-else y)))))

(local
(defthm bdd=-robdd-cong-implies
  (implies (and (bdd= x y) (robdd x))
           (robdd y))
  :hints (("Goal" :induct (bdd= x y)))
  :rule-classes nil))

(defcong bdd= equal (robdd x) 1
  :hints (("Goal" 
           :in-theory (disable robdd bdd=)
           :use ((:instance bdd=-robdd-cong-implies
                            (x x) (y x-equiv))
                 (:instance bdd=-robdd-cong-implies
                            (x x-equiv) (y x))))))

(defcong bdd= equal (top-var f g h) 1)

(defcong bdd= equal (top-var f g h) 2)

(defcong bdd= equal (top-var f g h) 3)

(local (defcong bdd= equal (consp x) 1))

(defun ite-f-induct (f fe g h)
  (declare (xargs :measure (+ (acl2-count f) 
			      (acl2-count g) 
			      (acl2-count h))))
  (if (atom f) fe
    (let ((v (top-var f g h)))
      (+ (ite-f-induct (then-node f v) 
                       (then-node fe v)
                       (then-node g v) 
                       (then-node h v))
         (ite-f-induct (else-node f v)
                       (else-node fe v)
                       (else-node g v)
                       (else-node h v))))))

(defun ite-g-induct (f g ge h)
  (declare (xargs :measure (+ (acl2-count f) 
			      (acl2-count g) 
			      (acl2-count h))))
  (if (atom f) ge
    (let ((v (top-var f g h)))
      (+ (ite-g-induct (then-node f v) 
                       (then-node g v)
                       (then-node ge v) 
                       (then-node h v))
         (ite-g-induct (else-node f v)
                       (else-node g v)
                       (else-node ge v)
                       (else-node h v))))))

(defun ite-h-induct (f g h he)
  (declare (xargs :measure (+ (acl2-count f) 
			      (acl2-count g) 
			      (acl2-count h))))
  (if (atom f) he
    (let ((v (top-var f g h)))
      (+ (ite-h-induct (then-node f v) 
                       (then-node g v)
                       (then-node h v) 
                       (then-node he v))
         (ite-h-induct (else-node f v)
                       (else-node g v)
                       (else-node h v)
                       (else-node he v))))))

(in-theory (disable top-var then-node else-node 
                    bdd= b-node))

(local (in-theory (disable bdd=-is-symmetric 
                           bdd=-is-transitive 
                           bdd=-is-reflexive)))

(defcong bdd= bdd= (ite-spec f g h) 1
  :hints (("Goal" :induct (ite-f-induct f f-equiv g h)
           :in-theory (enable b-node))
          ("Subgoal *1/1" :in-theory (enable bdd=))))

(defcong bdd= bdd= (ite-spec f g h) 2
  :hints (("Goal" :induct (ite-g-induct f g g-equiv h)
           :in-theory (enable b-node))
          ("Subgoal *1/1" :in-theory (enable bdd=))))

(defcong bdd= bdd= (ite-spec f g h) 3
  :hints (("Goal" :induct (ite-h-induct f g h h-equiv)
           :in-theory (enable b-node))
          ("Subgoal *1/1" :in-theory (enable bdd=))))

(in-theory (disable ite-spec robdd bdd-ev prop-if))

(in-theory (enable acl2-count))

;;;;;;;;;;;;;;;;;;;; END PART 5. ;;;;;;;;;;;;;;;;;;;;;;;;;

#|----------------------------------------------------------------------------|#