• 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-and-faig-operations-commute
          • 4v-sexpr-to-faig-plain
          • 4v-sexpr-to-faig-opt
          • Sfaig
          • 4v->faig-const
          • 4v-sexpr-to-faig-list
          • Faig-const-fix
          • Faig-const->4v
            • Faig-const-alist->4v-alist
            • Faig-const-list->4v-list
          • 4v-sexpr-to-faig-alist
          • Faig-const-<=
          • Faig-const-p
        • 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-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

• Faig-const->4v

Faig-const-list->4v-list

Signature

(faig-const-list->4v-list x) → *

Definitions and Theorems

Function: faig-const-list->4v-list

(defun faig-const-list->4v-list (x)
  (declare (xargs :guard t))
  (let ((__function__ 'faig-const-list->4v-list))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (faig-const->4v (car x))
            (faig-const-list->4v-list (cdr x))))))

Theorem: nth-of-faig-const-list->4v-list

(defthm nth-of-faig-const-list->4v-list
  (4v-equiv (nth n (faig-const-list->4v-list args))
            (faig-const->4v (nth n args))))