• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
          • 4vs-not-list
          • 4vs-onehot
          • 4vs-ite*-list-dumb
          • 4vs-and-list-dumb
          • 4vs-not
          • 4vs-and-list
          • 4vs-and-dumb
          • 4vs-and
          • 4vs-zif-dumb
          • 4vs-z
          • 4vs-x
          • 4vs-t
          • 4vs-ite*-dumb
          • 4vs-f
          • 4vs-iff
          • 4vs-buf
          • 4vs-xor
          • 4vs-or
          • 4vs-implies-lists
          • 4vs-implies
          • 4vs-xor-lists
          • 4vs-or-lists
          • 4vs-or-list
          • 4vs-iff-lists
          • 4vs-and-lists
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 4vs-constructors
• Onehot-rewriting

4vs-ite*-list-dumb

(4vs-ite*-list-dumb c as bs) produces a list of sexprs, basically (4V-ITE* C Ai Bi) for the corresponding elements of AS and BS.

Definitions and Theorems

Function: 4vs-ite*-list-dumb

(defun 4vs-ite*-list-dumb (c as bs)
       (declare (xargs :guard (equal (len as) (len bs))))
       (if (atom as)
           nil
           (cons (4vs-ite*-dumb c (car as) (car bs))
                 (4vs-ite*-list-dumb c (cdr as)
                                     (cdr bs)))))

Theorem: 4vs-ite*-list-dumb-when-atom

(defthm 4vs-ite*-list-dumb-when-atom
        (implies (atom as)
                 (equal (4vs-ite*-list-dumb c as bs)
                        nil)))

Theorem: 4vs-ite*-list-dumb-of-cons

(defthm 4vs-ite*-list-dumb-of-cons
        (equal (4vs-ite*-list-dumb c (cons a as)
                                   (cons b bs))
               (cons (4vs-ite*-dumb c a b)
                     (4vs-ite*-list-dumb c as bs))))

Theorem: consp-of-4vs-ite*-list-dumb

(defthm consp-of-4vs-ite*-list-dumb
        (equal (consp (4vs-ite*-list-dumb c as bs))
               (consp as)))

Theorem: len-of-4vs-ite*-list-dumb

(defthm len-of-4vs-ite*-list-dumb
        (equal (len (4vs-ite*-list-dumb c as bs))
               (len as)))

Theorem: car-of-4vs-ite*-list-dumb

(defthm car-of-4vs-ite*-list-dumb
        (equal (car (4vs-ite*-list-dumb c as bs))
               (if (consp as)
                   (4vs-ite*-dumb c (car as) (car bs))
                   nil)))

Theorem: cdr-of-4vs-ite*-list-dumb

(defthm cdr-of-4vs-ite*-list-dumb
        (equal (cdr (4vs-ite*-list-dumb c as bs))
               (4vs-ite*-list-dumb c (cdr as)
                                   (cdr bs))))

Theorem: 4v-sexpr-vars-list-of-4vs-ite*-list-dumb

(defthm
 4v-sexpr-vars-list-of-4vs-ite*-list-dumb
 (implies
  (equal (len a) (len b))
  (set-equiv (4v-sexpr-vars-list (4vs-ite*-list-dumb c a b))
             (if (consp a)
                 (hons-alphorder-merge
                      (4v-sexpr-vars c)
                      (hons-alphorder-merge (4v-sexpr-vars-list a)
                                            (4v-sexpr-vars-list b)))
                 nil))))