• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Svex-compilation
        • Moddb
        • Svmods
          • Address
            • Svarlist-add-delay
            • Svarlist-addr-p
              • Svarlist-addr-p-basics
            • Address-fix
            • Svex-alist-add-delay
            • Svarlist-addr-p-badguy
            • Svar-add-delay
            • Make-scoped-svar
            • Address-p
            • Address-equiv
            • Make-address
            • Svar-addr-p
            • Svar-addr-fix
            • Change-address
            • Address->scope
            • Address->path
            • Address->index
            • Svar->address
            • Make-simple-svar
            • Address->svar
            • Svex-add-delay-top
            • Addr-scope
          • Wire
          • Module
          • Lhs
          • Path
          • Svar-add-namespace
          • Design
          • Modinst
          • Lhs-add-namespace
          • Modalist
          • Path-add-namespace
          • Modname->submodnames
          • Name
          • Constraintlist-addr-p
          • Svex-alist-addr-p
          • Svar-map-addr-p
          • Lhspairs-addr-p
          • Modname
          • Assigns-addr-p
          • Lhs-addr-p
          • Lhatom-addr-p
          • Modhier-list-measure
          • Attributes
          • Modhier-measure
          • Modhier-list-measure-aux
          • Modhier-loopfreelist-p
          • Modhier-loopfree-p
        • Svstmt
        • Sv-tutorial
        • Expressions
        • Symbolic-test-vector
        • Vl-to-svex
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Address

Svarlist-addr-p

(svarlist-addr-p x) recognizes lists where every element satisfies svar-addr-p.

Signature
(svarlist-addr-p x) → std::bool

This is an ordinary std::deflist. It is "loose" in that it does not care whether x is nil-terminated.

Definitions and Theorems

Function: svarlist-addr-p

(defun svarlist-addr-p (x)
  (declare (xargs :guard (svarlist-p x)))
  (let ((__function__ 'svarlist-addr-p))
    (declare (ignorable __function__))
    (if (consp x)
        (and (svar-addr-p (car x))
             (svarlist-addr-p (cdr x)))
      t)))

Theorem: svarlist-addr-p-of-svarlist-fix-x

(defthm svarlist-addr-p-of-svarlist-fix-x
  (equal (svarlist-addr-p (svarlist-fix x))
         (svarlist-addr-p x)))

Theorem: svarlist-addr-p-svarlist-equiv-congruence-on-x

(defthm svarlist-addr-p-svarlist-equiv-congruence-on-x
  (implies (svarlist-equiv x x-equiv)
           (equal (svarlist-addr-p x)
                  (svarlist-addr-p x-equiv)))
  :rule-classes :congruence)

Subtopics

Svarlist-addr-p-basics
Basic theorems about svarlist-addr-p, generated by std::deflist.