• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
          • Name-database
            • Vl-namedb
            • Vl-namedb-plain-name
            • Vl-namedb-pset-fix
            • Vl-namedb-plain-names
            • Vl-namedb-indexed-name
            • Vl-namedb-pmap-fix
            • Vl-unlike-any-prefix-p
            • Vl-namedb-pmap-okp
            • Vl-namedb-allnames
            • Vl-starting-namedb
            • Vl-pgenstr-highest
            • Vl-namedb-pset-okp
            • Vl-pgenstr-p
            • Vl-pgenstr->val
            • Vl-free-namedb
            • Vl-namedb-plain-name-quiet
            • Vl-pgenstr-highest-of-alist-keys
            • Vl-pgenstr
            • Vl-empty-namedb
            • Vl-namedb-nameset
              • Vl-namedb-nameset-p
                • Vl-namedb-nameset-fix
                • Vl-namedb-nameset-equiv
              • Vl-unlike-any-prefix-p-of-alist-keys
              • Vl-namedb-prefixmap
            • Vl-gc
            • Symbol-list-names
            • Ints-from
            • Nats-from
            • Make-lookup-alist
            • Redundant-mergesort
            • Longest-common-prefix
            • Vl-plural-p
            • Vl-remove-keys
            • Vl-merge-contiguous-indices
            • Vl-edition-p
            • Sum-nats
            • Vl-maybe-integer-listp
            • Fast-memberp
            • Nat-listp
            • Max-nats
            • Longest-common-prefix-list
            • Character-list-listp
            • Vl-character-list-list-values-p
            • Remove-from-alist
            • Prefix-of-eachp
            • Vl-string-keys-p
            • Vl-maybe-nat-listp
            • Vl-string-list-values-p
            • String-list-listp
            • Vl-string-values-p
            • True-list-listp
            • Symbol-list-listp
            • Explode-list
            • All-have-len
            • Pos-listp
            • Min-nats
            • Debuggable-and
            • Vl-starname
            • Remove-equal-without-guard
            • Vl-maybe-string-list
            • String-fix
            • Longer-than-p
            • Anyp
            • Fast-alist-free-each-alist-val
            • Not*
            • Free-list-of-fast-alists
            • *nls*
          • Printer
          • Kit
          • Mlib
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-namedb-nameset

    Vl-namedb-nameset-p

    Recognizer for vl-namedb-nameset.

    Signature
    (vl-namedb-nameset-p x) → *

    Definitions and Theorems

    Function: vl-namedb-nameset-p

    (defun vl-namedb-nameset-p (x)
      (declare (xargs :guard t))
      (let ((__function__ 'vl-namedb-nameset-p))
        (declare (ignorable __function__))
        (if (atom x)
            t
          (and (consp (car x))
               (stringp (caar x))
               (true-p (cdar x))
               (vl-namedb-nameset-p (cdr x))))))

    Theorem: vl-namedb-nameset-p-of-revappend

    (defthm vl-namedb-nameset-p-of-revappend
      (equal (vl-namedb-nameset-p (revappend acl2::x acl2::y))
             (and (vl-namedb-nameset-p (list-fix acl2::x))
                  (vl-namedb-nameset-p acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-remove

    (defthm vl-namedb-nameset-p-of-remove
      (implies (vl-namedb-nameset-p acl2::x)
               (vl-namedb-nameset-p (remove acl2::a acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-last

    (defthm vl-namedb-nameset-p-of-last
      (implies (vl-namedb-nameset-p (double-rewrite acl2::x))
               (vl-namedb-nameset-p (last acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-nthcdr

    (defthm vl-namedb-nameset-p-of-nthcdr
      (implies (vl-namedb-nameset-p (double-rewrite acl2::x))
               (vl-namedb-nameset-p (nthcdr acl2::n acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-butlast

    (defthm vl-namedb-nameset-p-of-butlast
      (implies (vl-namedb-nameset-p (double-rewrite acl2::x))
               (vl-namedb-nameset-p (butlast acl2::x acl2::n)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-update-nth

    (defthm vl-namedb-nameset-p-of-update-nth
     (implies
         (vl-namedb-nameset-p (double-rewrite acl2::x))
         (iff (vl-namedb-nameset-p (update-nth acl2::n acl2::y acl2::x))
              (and (and (consp acl2::y)
                        (stringp (car acl2::y))
                        (true-p (cdr acl2::y)))
                   (or (<= (nfix acl2::n) (len acl2::x))
                       (and (consp nil)
                            (stringp (car nil))
                            (true-p (cdr nil)))))))
     :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-repeat

    (defthm vl-namedb-nameset-p-of-repeat
      (iff (vl-namedb-nameset-p (repeat acl2::n acl2::x))
           (or (and (consp acl2::x)
                    (stringp (car acl2::x))
                    (true-p (cdr acl2::x)))
               (zp acl2::n)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-take

    (defthm vl-namedb-nameset-p-of-take
      (implies (vl-namedb-nameset-p (double-rewrite acl2::x))
               (iff (vl-namedb-nameset-p (take acl2::n acl2::x))
                    (or (and (consp nil)
                             (stringp (car nil))
                             (true-p (cdr nil)))
                        (<= (nfix acl2::n) (len acl2::x)))))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-union-equal

    (defthm vl-namedb-nameset-p-of-union-equal
      (equal (vl-namedb-nameset-p (union-equal acl2::x acl2::y))
             (and (vl-namedb-nameset-p (list-fix acl2::x))
                  (vl-namedb-nameset-p (double-rewrite acl2::y))))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-intersection-equal-2

    (defthm vl-namedb-nameset-p-of-intersection-equal-2
      (implies
           (vl-namedb-nameset-p (double-rewrite acl2::y))
           (vl-namedb-nameset-p (intersection-equal acl2::x acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-intersection-equal-1

    (defthm vl-namedb-nameset-p-of-intersection-equal-1
      (implies
           (vl-namedb-nameset-p (double-rewrite acl2::x))
           (vl-namedb-nameset-p (intersection-equal acl2::x acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-set-difference-equal

    (defthm vl-namedb-nameset-p-of-set-difference-equal
      (implies
           (vl-namedb-nameset-p acl2::x)
           (vl-namedb-nameset-p (set-difference-equal acl2::x acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-set-equiv-congruence

    (defthm vl-namedb-nameset-p-set-equiv-congruence
      (implies (set-equiv acl2::x acl2::y)
               (equal (vl-namedb-nameset-p acl2::x)
                      (vl-namedb-nameset-p acl2::y)))
      :rule-classes :congruence)

    Theorem: vl-namedb-nameset-p-when-subsetp-equal

    (defthm vl-namedb-nameset-p-when-subsetp-equal
      (and (implies (and (subsetp-equal acl2::x acl2::y)
                         (vl-namedb-nameset-p acl2::y))
                    (vl-namedb-nameset-p acl2::x))
           (implies (and (vl-namedb-nameset-p acl2::y)
                         (subsetp-equal acl2::x acl2::y))
                    (vl-namedb-nameset-p acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-rcons

    (defthm vl-namedb-nameset-p-of-rcons
      (iff (vl-namedb-nameset-p (acl2::rcons acl2::a acl2::x))
           (and (and (consp acl2::a)
                     (stringp (car acl2::a))
                     (true-p (cdr acl2::a)))
                (vl-namedb-nameset-p (list-fix acl2::x))))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-rev

    (defthm vl-namedb-nameset-p-of-rev
      (equal (vl-namedb-nameset-p (rev acl2::x))
             (vl-namedb-nameset-p (list-fix acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-duplicated-members

    (defthm vl-namedb-nameset-p-of-duplicated-members
      (implies (vl-namedb-nameset-p acl2::x)
               (vl-namedb-nameset-p (duplicated-members acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-difference

    (defthm vl-namedb-nameset-p-of-difference
      (implies (vl-namedb-nameset-p acl2::x)
               (vl-namedb-nameset-p (difference acl2::x acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-intersect-2

    (defthm vl-namedb-nameset-p-of-intersect-2
      (implies (vl-namedb-nameset-p acl2::y)
               (vl-namedb-nameset-p (intersect acl2::x acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-intersect-1

    (defthm vl-namedb-nameset-p-of-intersect-1
      (implies (vl-namedb-nameset-p acl2::x)
               (vl-namedb-nameset-p (intersect acl2::x acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-union

    (defthm vl-namedb-nameset-p-of-union
      (iff (vl-namedb-nameset-p (union acl2::x acl2::y))
           (and (vl-namedb-nameset-p (sfix acl2::x))
                (vl-namedb-nameset-p (sfix acl2::y))))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-mergesort

    (defthm vl-namedb-nameset-p-of-mergesort
      (iff (vl-namedb-nameset-p (mergesort acl2::x))
           (vl-namedb-nameset-p (list-fix acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-delete

    (defthm vl-namedb-nameset-p-of-delete
      (implies (vl-namedb-nameset-p acl2::x)
               (vl-namedb-nameset-p (delete acl2::k acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-insert

    (defthm vl-namedb-nameset-p-of-insert
      (iff (vl-namedb-nameset-p (insert acl2::a acl2::x))
           (and (vl-namedb-nameset-p (sfix acl2::x))
                (and (consp acl2::a)
                     (stringp (car acl2::a))
                     (true-p (cdr acl2::a)))))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-sfix

    (defthm vl-namedb-nameset-p-of-sfix
      (iff (vl-namedb-nameset-p (sfix acl2::x))
           (or (vl-namedb-nameset-p acl2::x)
               (not (setp acl2::x))))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-list-fix

    (defthm vl-namedb-nameset-p-of-list-fix
      (equal (vl-namedb-nameset-p (list-fix acl2::x))
             (vl-namedb-nameset-p acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-append

    (defthm vl-namedb-nameset-p-of-append
      (equal (vl-namedb-nameset-p (append acl2::a acl2::b))
             (and (vl-namedb-nameset-p acl2::a)
                  (vl-namedb-nameset-p acl2::b)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-when-not-consp

    (defthm vl-namedb-nameset-p-when-not-consp
      (implies (not (consp acl2::x))
               (vl-namedb-nameset-p acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-cdr-when-vl-namedb-nameset-p

    (defthm vl-namedb-nameset-p-of-cdr-when-vl-namedb-nameset-p
      (implies (vl-namedb-nameset-p (double-rewrite acl2::x))
               (vl-namedb-nameset-p (cdr acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-cons

    (defthm vl-namedb-nameset-p-of-cons
      (equal (vl-namedb-nameset-p (cons acl2::a acl2::x))
             (and (and (consp acl2::a)
                       (stringp (car acl2::a))
                       (true-p (cdr acl2::a)))
                  (vl-namedb-nameset-p acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-make-fal

    (defthm vl-namedb-nameset-p-of-make-fal
      (implies (and (vl-namedb-nameset-p acl2::x)
                    (vl-namedb-nameset-p acl2::y))
               (vl-namedb-nameset-p (make-fal acl2::x acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: true-p-of-cdr-when-member-equal-of-vl-namedb-nameset-p

    (defthm true-p-of-cdr-when-member-equal-of-vl-namedb-nameset-p
      (and (implies (and (vl-namedb-nameset-p acl2::x)
                         (member-equal acl2::a acl2::x))
                    (true-p (cdr acl2::a)))
           (implies (and (member-equal acl2::a acl2::x)
                         (vl-namedb-nameset-p acl2::x))
                    (true-p (cdr acl2::a))))
      :rule-classes ((:rewrite)))

    Theorem: stringp-of-car-when-member-equal-of-vl-namedb-nameset-p

    (defthm stringp-of-car-when-member-equal-of-vl-namedb-nameset-p
      (and (implies (and (vl-namedb-nameset-p acl2::x)
                         (member-equal acl2::a acl2::x))
                    (stringp (car acl2::a)))
           (implies (and (member-equal acl2::a acl2::x)
                         (vl-namedb-nameset-p acl2::x))
                    (stringp (car acl2::a))))
      :rule-classes ((:rewrite)))

    Theorem: consp-when-member-equal-of-vl-namedb-nameset-p

    (defthm consp-when-member-equal-of-vl-namedb-nameset-p
      (implies (and (vl-namedb-nameset-p acl2::x)
                    (member-equal acl2::a acl2::x))
               (consp acl2::a))
      :rule-classes
      ((:rewrite :backchain-limit-lst (0 0))
       (:rewrite :backchain-limit-lst (0 0)
                 :corollary (implies (if (member-equal acl2::a acl2::x)
                                         (vl-namedb-nameset-p acl2::x)
                                       'nil)
                                     (consp acl2::a)))))

    Theorem: vl-namedb-nameset-p-of-fast-alist-clean

    (defthm vl-namedb-nameset-p-of-fast-alist-clean
      (implies (vl-namedb-nameset-p acl2::x)
               (vl-namedb-nameset-p (fast-alist-clean acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-hons-shrink-alist

    (defthm vl-namedb-nameset-p-of-hons-shrink-alist
     (implies (and (vl-namedb-nameset-p acl2::x)
                   (vl-namedb-nameset-p acl2::y))
              (vl-namedb-nameset-p (hons-shrink-alist acl2::x acl2::y)))
     :rule-classes ((:rewrite)))

    Theorem: vl-namedb-nameset-p-of-hons-acons

    (defthm vl-namedb-nameset-p-of-hons-acons
      (equal (vl-namedb-nameset-p (hons-acons acl2::a acl2::n acl2::x))
             (and (stringp acl2::a)
                  (true-p acl2::n)
                  (vl-namedb-nameset-p acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: true-p-of-cdr-of-hons-assoc-equal-when-vl-namedb-nameset-p

    (defthm true-p-of-cdr-of-hons-assoc-equal-when-vl-namedb-nameset-p
      (implies (vl-namedb-nameset-p acl2::x)
               (iff (true-p (cdr (hons-assoc-equal acl2::k acl2::x)))
                    (hons-assoc-equal acl2::k acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: true-p-of-cdar-when-vl-namedb-nameset-p

    (defthm true-p-of-cdar-when-vl-namedb-nameset-p
      (implies (vl-namedb-nameset-p acl2::x)
               (iff (true-p (cdar acl2::x))
                    (consp acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: stringp-of-caar-when-vl-namedb-nameset-p

    (defthm stringp-of-caar-when-vl-namedb-nameset-p
      (implies (vl-namedb-nameset-p acl2::x)
               (iff (stringp (caar acl2::x))
                    (consp acl2::x)))
      :rule-classes ((:rewrite)))