• Top
  • Documentation
  • Books
  • 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
        • 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-shannon-expansion
          • Onehot-rewriting
            • 4v-onehot-sexpr-list-prime
            • 4v-onehot-sexpr-prime
            • 4v-onehot-rw-sexpr-alist-aux
            • 4v-onehot-rw-sexpr-alist
            • 4v-onehot-rw-sexpr
            • 4vs-onehot
            • 4vs-ite*-list-dumb
            • 4v-onehot-filter
            • 4v-onehot-list-p
          • 4v-sexpr-restrict-with-rw
          • 4v-sexpr-compose-with-rw
          • Sexpr-rewrite
          • Sexpr-rewrite-default
          • Sexpr-rewriting-internals
          • *sexpr-rewrites*
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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))))