• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
      • Equal-by-eval-bdds
      • Ubdd-constructors
        • Q-and
        • Q-ite
        • Q-or
        • Q-implies
        • Q-iff
        • Q-and-c2
        • Q-and-c1
        • Q-or-c2
        • Q-not
        • Q-ite-fn
        • Q-xor
        • Q-and-is-nil
        • Cheap-and-expensive-arguments
        • Q-compose-list
        • Q-compose
        • Qv
        • Q-and-is-nilc2
        • Q-nor
        • Q-nand
      • Eval-bdd
      • Ubddp
      • Ubdd-fix
      • Q-sat
      • Bdd-sat-dfs
      • Eval-bdd-list
      • Qcdr
      • Qcar
      • Q-sat-any
      • Canonicalize-to-q-ite
      • Ubdd-listp
      • Qcons
    • Bdd
    • Faig
    • Bed
    • 4v
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Ubdd-constructors

Q-compose-list

(q-compose-list xs l) composes each UBDD in xs with the list of UBDDs l, i.e., it maps q-compose across xs.

Definitions and Theorems

Function: q-compose-list

(defun q-compose-list (xs l)
       (declare (xargs :guard t))
       (if (atom xs)
           nil
           (cons (q-compose (car xs) l)
                 (q-compose-list (cdr xs) l))))

Theorem: q-compose-list-when-not-consp

(defthm q-compose-list-when-not-consp
        (implies (not (consp xs))
                 (equal (q-compose-list xs l) nil)))

Theorem: q-compose-list-of-cons

(defthm q-compose-list-of-cons
        (equal (q-compose-list (cons x xs) l)
               (cons (q-compose x l)
                     (q-compose-list xs l))))

Theorem: ubdd-listp-of-q-compose-list

(defthm ubdd-listp-of-q-compose-list
        (implies (and (force (ubdd-listp xs))
                      (force (ubdd-listp l)))
                 (equal (ubdd-listp (q-compose-list xs l))
                        t)))