• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
          • Vl-module
          • Vl-vardecl
          • Expressions
          • Vl-fundecl
          • Vl-assign
          • Vl-gateinst
          • Vl-modinst
          • Vl-commentmap
          • Vl-portdecl
          • Vl-taskdecl
          • Vl-design
          • Vl-interface
          • Vl-plainarglist->exprs
          • Vl-taskdecllist->names
          • Vl-fundecllist->names
          • Vl-package
          • Vl-port
          • Vl-udp
          • Vl-paramdecl
          • Vl-genelement
          • Vl-cycledelayrange
          • Vl-namedarg
          • Vl-sort-blockitems-aux
          • Vl-distitem
          • Vl-gatedelay
          • Vl-repetition
          • Vl-typedef
          • Vl-range
          • Vl-gatestrength
          • Vl-program
          • Vl-config
          • Vl-always
          • Vl-datatype-update-dims
          • Vl-import
          • Vl-enumbasetype
          • Vl-repeateventcontrol
          • Vl-paramargs
          • Vl-initial
          • Vl-eventcontrol
          • Vl-udpsymbol-p
          • Vl-maybe-range
          • Vl-maybe-nettypename
          • Vl-maybe-gatestrength
          • Vl-maybe-gatedelay
          • Vl-maybe-delayoreventcontrol
          • Vl-alias
          • Maybe-string-fix
          • Vl-maybe-packeddimension
          • Vl-fwdtypedef
          • Vl-evatom
          • Vl-packeddimension-p
          • Vl-maybe-udpsymbol
          • Vl-maybe-module
          • Vl-maybe-direction
          • Vl-maybe-datatype
          • Vl-maybe-cstrength
          • Vl-direction-p
          • Vl-arguments
          • Vl-maybe-design
          • Vl-udpline
          • Vl-exprdist
          • Vl-context1
          • Vl-genvar
          • Vl-enumitem
          • Vl-datatype-update-udims
          • Vl-datatype-update-pdims
          • Vl-modelement
          • Vl-udpedge
          • Vl-delaycontrol
          • Vl-context
            • Vl-context-p
            • Ctxexprs
              • Vl-make-exprctxalist
              • Vl-paramdecllist-ctxexprs
              • Vl-taskdecllist-ctxexprs
              • Vl-portdecllist-ctxexprs
              • Vl-gateinstlist-ctxexprs
              • Vl-vardecllist-ctxexprs
              • Vl-modinstlist-ctxexprs
              • Vl-initiallist-ctxexprs
              • Vl-fundecllist-ctxexprs
              • Vl-assignlist-ctxexprs
              • Vl-alwayslist-ctxexprs
              • Vl-portlist-ctxexprs
              • Vl-taskdecl-ctxexprs
              • Vl-portdecl-ctxexprs
              • Vl-paramdecl-ctxexprs
              • Vl-gateinst-ctxexprs
              • Vl-vardecl-ctxexprs
              • Vl-modinst-ctxexprs
              • Vl-initial-ctxexprs
              • Vl-fundecl-ctxexprs
              • Vl-assign-ctxexprs
              • Vl-always-ctxexprs
              • Vl-port-ctxexprs
              • Vl-exprctxalist
                • Vl-exprctxalist-p
                  • Vl-exprctxalist-fix
                  • Vl-exprctxalist-equiv
              • Vl-pp-ctxelement-summary
              • Vl-pp-ctxelement-full
              • Vl-context-fix
              • Vl-ctxelement-summary
              • Vl-context-summary
              • Vl-pp-context-summary
              • Vl-pp-context-full
            • Vl-sort-blockitems
            • Vl-distweighttype-p
            • Vl-ctxelement->loc
            • Vl-blockitem
            • Vl-vardecllist
            • Vl-module->ifports
            • Vl-modelement->loc
            • Vl-ctxelement
            • Vl-coretypename-p
            • Vl-packeddimensionlist
            • Vl-modelementlist->genelements
            • Vl-gatetype-p
            • Vl-paramdecllist
            • Vl-lifetime-p
            • Vl-datatype->udims
            • Vl-datatype->pdims
            • Vl-timeunit-p
            • Vl-repetitiontype-p
            • Vl-port->name
            • Vl-importlist
            • Vl-genelement->loc
            • Vl-delayoreventcontrol
            • Vl-cstrength-p
            • Statements
            • Vl-udpentry-p
            • Vl-packeddimension-fix
            • Vl-nettypename-p
            • Vl-portdecllist
            • Vl-port->loc
            • Vl-enumbasekind-fix
            • Vl-arguments->args
            • Vl-taskdecllist
            • Vl-portlist
            • Vl-importpart-p
            • Vl-importpart-fix
            • Vl-fundecllist
            • Vl-blockstmt-p
            • Vl-assignlist
            • Vl-alwaystype-p
            • Vl-typedeflist
            • Vl-syntaxversion-p
            • Vl-randomqualifier-p
            • Vl-modinstlist
            • Vl-gateinstlist
            • Vl-blockitemlist
            • Vl-udptable
            • Vl-udplist
            • Vl-udpentrylist
            • Vl-programlist
            • Vl-paramvaluelist
            • Vl-packagelist
            • Vl-namedparamvaluelist
            • Vl-namedarglist
            • Vl-modulelist
            • Vl-modportlist
            • Vl-modport-portlist
            • Vl-interfacelist
            • Vl-initiallist
            • Vl-genvarlist
            • Vl-fwdtypedeflist
            • Vl-evatomlist
            • Vl-enumitemlist
            • Vl-distlist
            • Vl-configlist
            • Vl-alwayslist
            • Vl-aliaslist
            • Vl-regularportlist
            • Vl-rangelist-list
            • Vl-rangelist
            • Vl-paramdecllist-list
            • Vl-modelementlist
            • Vl-maybe-range-list
            • Vl-interfaceportlist
            • Vl-argumentlist
            • Data-types
          • Getting-started
          • Utilities
          • Loader
          • Transforms
          • Lint
          • Mlib
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-exprctxalist

    Vl-exprctxalist-p

    Recognizer for vl-exprctxalist.

    Signature
    (vl-exprctxalist-p x) → *

    Definitions and Theorems

    Function: vl-exprctxalist-p

    (defun vl-exprctxalist-p (x)
      (declare (xargs :guard t))
      (let ((__function__ 'vl-exprctxalist-p))
        (declare (ignorable __function__))
        (if (atom x)
            t
          (and (consp (car x))
               (vl-expr-p (caar x))
               (vl-context1-p (cdar x))
               (vl-exprctxalist-p (cdr x))))))

    Theorem: vl-exprctxalist-p-of-revappend

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

    Theorem: vl-exprctxalist-p-of-remove

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

    Theorem: vl-exprctxalist-p-of-last

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

    Theorem: vl-exprctxalist-p-of-nthcdr

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

    Theorem: vl-exprctxalist-p-of-butlast

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

    Theorem: vl-exprctxalist-p-of-update-nth

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

    Theorem: vl-exprctxalist-p-of-repeat

    (defthm vl-exprctxalist-p-of-repeat
      (iff (vl-exprctxalist-p (repeat acl2::n acl2::x))
           (or (and (consp acl2::x)
                    (vl-expr-p (car acl2::x))
                    (vl-context1-p (cdr acl2::x)))
               (zp acl2::n)))
      :rule-classes ((:rewrite)))

    Theorem: vl-exprctxalist-p-of-take

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

    Theorem: vl-exprctxalist-p-of-union-equal

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

    Theorem: vl-exprctxalist-p-of-intersection-equal-2

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

    Theorem: vl-exprctxalist-p-of-intersection-equal-1

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

    Theorem: vl-exprctxalist-p-of-set-difference-equal

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

    Theorem: vl-exprctxalist-p-set-equiv-congruence

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

    Theorem: vl-exprctxalist-p-when-subsetp-equal

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

    Theorem: vl-exprctxalist-p-of-rcons

    (defthm vl-exprctxalist-p-of-rcons
      (iff (vl-exprctxalist-p (acl2::rcons acl2::a acl2::x))
           (and (and (consp acl2::a)
                     (vl-expr-p (car acl2::a))
                     (vl-context1-p (cdr acl2::a)))
                (vl-exprctxalist-p (list-fix acl2::x))))
      :rule-classes ((:rewrite)))

    Theorem: vl-exprctxalist-p-of-rev

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

    Theorem: vl-exprctxalist-p-of-duplicated-members

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

    Theorem: vl-exprctxalist-p-of-difference

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

    Theorem: vl-exprctxalist-p-of-intersect-2

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

    Theorem: vl-exprctxalist-p-of-intersect-1

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

    Theorem: vl-exprctxalist-p-of-union

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

    Theorem: vl-exprctxalist-p-of-mergesort

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

    Theorem: vl-exprctxalist-p-of-delete

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

    Theorem: vl-exprctxalist-p-of-insert

    (defthm vl-exprctxalist-p-of-insert
      (iff (vl-exprctxalist-p (insert acl2::a acl2::x))
           (and (vl-exprctxalist-p (sfix acl2::x))
                (and (consp acl2::a)
                     (vl-expr-p (car acl2::a))
                     (vl-context1-p (cdr acl2::a)))))
      :rule-classes ((:rewrite)))

    Theorem: vl-exprctxalist-p-of-sfix

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

    Theorem: vl-exprctxalist-p-of-list-fix

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

    Theorem: vl-exprctxalist-p-of-append

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

    Theorem: vl-exprctxalist-p-when-not-consp

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

    Theorem: vl-exprctxalist-p-of-cdr-when-vl-exprctxalist-p

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

    Theorem: vl-exprctxalist-p-of-cons

    (defthm vl-exprctxalist-p-of-cons
      (equal (vl-exprctxalist-p (cons acl2::a acl2::x))
             (and (and (consp acl2::a)
                       (vl-expr-p (car acl2::a))
                       (vl-context1-p (cdr acl2::a)))
                  (vl-exprctxalist-p acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-exprctxalist-p-of-make-fal

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

    Theorem: vl-context1-p-of-cdr-when-member-equal-of-vl-exprctxalist-p

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

    Theorem: vl-expr-p-of-car-when-member-equal-of-vl-exprctxalist-p

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

    Theorem: consp-when-member-equal-of-vl-exprctxalist-p

    (defthm consp-when-member-equal-of-vl-exprctxalist-p
      (implies (and (vl-exprctxalist-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-exprctxalist-p acl2::x)
                                       'nil)
                                     (consp acl2::a)))))

    Theorem: vl-exprctxalist-p-of-fast-alist-clean

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

    Theorem: vl-exprctxalist-p-of-hons-shrink-alist

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

    Theorem: vl-exprctxalist-p-of-hons-acons

    (defthm vl-exprctxalist-p-of-hons-acons
      (equal (vl-exprctxalist-p (hons-acons acl2::a acl2::n acl2::x))
             (and (vl-expr-p acl2::a)
                  (vl-context1-p acl2::n)
                  (vl-exprctxalist-p acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: vl-context1-p-of-cdr-of-hons-assoc-equal-when-vl-exprctxalist-p

    (defthm
        vl-context1-p-of-cdr-of-hons-assoc-equal-when-vl-exprctxalist-p
      (implies
           (vl-exprctxalist-p acl2::x)
           (iff (vl-context1-p (cdr (hons-assoc-equal acl2::k acl2::x)))
                (or (hons-assoc-equal acl2::k acl2::x)
                    (vl-context1-p nil))))
      :rule-classes ((:rewrite)))

    Theorem: vl-context1-p-of-cdar-when-vl-exprctxalist-p

    (defthm vl-context1-p-of-cdar-when-vl-exprctxalist-p
      (implies (vl-exprctxalist-p acl2::x)
               (iff (vl-context1-p (cdar acl2::x))
                    (or (consp acl2::x)
                        (vl-context1-p nil))))
      :rule-classes ((:rewrite)))

    Theorem: vl-expr-p-of-caar-when-vl-exprctxalist-p

    (defthm vl-expr-p-of-caar-when-vl-exprctxalist-p
      (implies (vl-exprctxalist-p acl2::x)
               (iff (vl-expr-p (caar acl2::x))
                    (or (consp acl2::x) (vl-expr-p nil))))
      :rule-classes ((:rewrite)))