• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Error-checking
      • Apt
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Prime-field-constraint-systems
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
        • Primitive-functions
        • Translated-terms
          • Tterm-constant-list->value-list
          • Tterm-free-vars
          • Tterm-option
          • Tterm-constant-list
          • Tterm-case-constant-listp
            • Tterm-case-constant-listp-basics
          • Lift-term
          • Tterms
        • Values
        • Evaluation
        • Program-equivalence
        • Functions
        • Packages
        • Programs
        • Interpreter
        • Evaluation-states
      • Prime-fields
      • Java
      • C
      • Syntheto
      • Number-theory
      • Cryptography
      • Lists-light
      • File-io-light
      • Json
      • Built-ins
      • Solidity
      • Axe
      • Std-extensions
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• Tterm-case-constant-listp

Tterm-case-constant-listp-basics

Basic theorems about tterm-case-constant-listp, generated by std::deflist.

Definitions and Theorems

Theorem: tterm-case-constant-listp-of-cons

(defthm tterm-case-constant-listp-of-cons
        (equal (tterm-case-constant-listp (cons acl2::a acl2::x))
               (and (tterm-case acl2::a :constant)
                    (tterm-case-constant-listp acl2::x)))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-cdr-when-tterm-case-constant-listp

(defthm
     tterm-case-constant-listp-of-cdr-when-tterm-case-constant-listp
     (implies (tterm-case-constant-listp (double-rewrite acl2::x))
              (tterm-case-constant-listp (cdr acl2::x)))
     :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-when-not-consp

(defthm tterm-case-constant-listp-when-not-consp
        (implies (not (consp acl2::x))
                 (equal (tterm-case-constant-listp acl2::x)
                        (not acl2::x)))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-of-car-when-tterm-case-constant-listp

(defthm tterm-case-of-car-when-tterm-case-constant-listp
        (implies (tterm-case-constant-listp acl2::x)
                 (iff (tterm-case (car acl2::x) :constant)
                      (consp acl2::x)))
        :rule-classes ((:rewrite)))

Theorem: true-listp-when-tterm-case-constant-listp

(defthm true-listp-when-tterm-case-constant-listp
        (implies (tterm-case-constant-listp acl2::x)
                 (true-listp acl2::x))
        :rule-classes :compound-recognizer)

Theorem: tterm-case-constant-listp-of-list-fix

(defthm tterm-case-constant-listp-of-list-fix
        (implies (tterm-case-constant-listp acl2::x)
                 (tterm-case-constant-listp (list-fix acl2::x)))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-sfix

(defthm tterm-case-constant-listp-of-sfix
        (iff (tterm-case-constant-listp (sfix acl2::x))
             (or (tterm-case-constant-listp acl2::x)
                 (not (setp acl2::x))))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-insert

(defthm tterm-case-constant-listp-of-insert
        (iff (tterm-case-constant-listp (insert acl2::a acl2::x))
             (and (tterm-case-constant-listp (sfix acl2::x))
                  (tterm-case acl2::a :constant)))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-delete

(defthm
     tterm-case-constant-listp-of-delete
     (implies (tterm-case-constant-listp acl2::x)
              (tterm-case-constant-listp (delete acl2::k acl2::x)))
     :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-mergesort

(defthm tterm-case-constant-listp-of-mergesort
        (iff (tterm-case-constant-listp (mergesort acl2::x))
             (tterm-case-constant-listp (list-fix acl2::x)))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-union

(defthm tterm-case-constant-listp-of-union
        (iff (tterm-case-constant-listp (union acl2::x acl2::y))
             (and (tterm-case-constant-listp (sfix acl2::x))
                  (tterm-case-constant-listp (sfix acl2::y))))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-intersect-1

(defthm
   tterm-case-constant-listp-of-intersect-1
   (implies (tterm-case-constant-listp acl2::x)
            (tterm-case-constant-listp (intersect acl2::x acl2::y)))
   :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-intersect-2

(defthm
   tterm-case-constant-listp-of-intersect-2
   (implies (tterm-case-constant-listp acl2::y)
            (tterm-case-constant-listp (intersect acl2::x acl2::y)))
   :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-difference

(defthm
  tterm-case-constant-listp-of-difference
  (implies (tterm-case-constant-listp acl2::x)
           (tterm-case-constant-listp (difference acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-duplicated-members

(defthm
  tterm-case-constant-listp-of-duplicated-members
  (implies (tterm-case-constant-listp acl2::x)
           (tterm-case-constant-listp (duplicated-members acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-rev

(defthm tterm-case-constant-listp-of-rev
        (equal (tterm-case-constant-listp (rev acl2::x))
               (tterm-case-constant-listp (list-fix acl2::x)))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-append

(defthm tterm-case-constant-listp-of-append
        (equal (tterm-case-constant-listp (append acl2::a acl2::b))
               (and (tterm-case-constant-listp (list-fix acl2::a))
                    (tterm-case-constant-listp acl2::b)))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-rcons

(defthm tterm-case-constant-listp-of-rcons
        (iff (tterm-case-constant-listp (rcons acl2::a acl2::x))
             (and (tterm-case acl2::a :constant)
                  (tterm-case-constant-listp (list-fix acl2::x))))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-when-member-equal-of-tterm-case-constant-listp

(defthm tterm-case-when-member-equal-of-tterm-case-constant-listp
        (and (implies (and (member-equal acl2::a acl2::x)
                           (tterm-case-constant-listp acl2::x))
                      (tterm-case acl2::a :constant))
             (implies (and (tterm-case-constant-listp acl2::x)
                           (member-equal acl2::a acl2::x))
                      (tterm-case acl2::a :constant)))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-when-subsetp-equal

(defthm tterm-case-constant-listp-when-subsetp-equal
        (and (implies (and (subsetp-equal acl2::x acl2::y)
                           (tterm-case-constant-listp acl2::y))
                      (equal (tterm-case-constant-listp acl2::x)
                             (true-listp acl2::x)))
             (implies (and (tterm-case-constant-listp acl2::y)
                           (subsetp-equal acl2::x acl2::y))
                      (equal (tterm-case-constant-listp acl2::x)
                             (true-listp acl2::x))))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-set-difference-equal

(defthm tterm-case-constant-listp-of-set-difference-equal
        (implies (tterm-case-constant-listp acl2::x)
                 (tterm-case-constant-listp
                      (set-difference-equal acl2::x acl2::y)))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-intersection-equal-1

(defthm
 tterm-case-constant-listp-of-intersection-equal-1
 (implies
   (tterm-case-constant-listp (double-rewrite acl2::x))
   (tterm-case-constant-listp (intersection-equal acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-intersection-equal-2

(defthm
 tterm-case-constant-listp-of-intersection-equal-2
 (implies
   (tterm-case-constant-listp (double-rewrite acl2::y))
   (tterm-case-constant-listp (intersection-equal acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-union-equal

(defthm
  tterm-case-constant-listp-of-union-equal
  (equal (tterm-case-constant-listp (union-equal acl2::x acl2::y))
         (and (tterm-case-constant-listp (list-fix acl2::x))
              (tterm-case-constant-listp (double-rewrite acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-take

(defthm
    tterm-case-constant-listp-of-take
    (implies (tterm-case-constant-listp (double-rewrite acl2::x))
             (iff (tterm-case-constant-listp (take acl2::n acl2::x))
                  (or (tterm-case nil :constant)
                      (<= (nfix acl2::n) (len acl2::x)))))
    :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-repeat

(defthm tterm-case-constant-listp-of-repeat
        (iff (tterm-case-constant-listp (repeat acl2::n acl2::x))
             (or (tterm-case acl2::x :constant)
                 (zp acl2::n)))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-of-nth-when-tterm-case-constant-listp

(defthm tterm-case-of-nth-when-tterm-case-constant-listp
        (implies (tterm-case-constant-listp acl2::x)
                 (iff (tterm-case (nth acl2::n acl2::x)
                                  :constant)
                      (< (nfix acl2::n) (len acl2::x))))
        :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-update-nth

(defthm
 tterm-case-constant-listp-of-update-nth
 (implies
  (tterm-case-constant-listp (double-rewrite acl2::x))
  (iff
    (tterm-case-constant-listp (update-nth acl2::n acl2::y acl2::x))
    (and (tterm-case acl2::y :constant)
         (or (<= (nfix acl2::n) (len acl2::x))
             (tterm-case nil :constant)))))
 :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-butlast

(defthm
     tterm-case-constant-listp-of-butlast
     (implies (tterm-case-constant-listp (double-rewrite acl2::x))
              (tterm-case-constant-listp (butlast acl2::x acl2::n)))
     :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-nthcdr

(defthm
     tterm-case-constant-listp-of-nthcdr
     (implies (tterm-case-constant-listp (double-rewrite acl2::x))
              (tterm-case-constant-listp (nthcdr acl2::n acl2::x)))
     :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-last

(defthm
     tterm-case-constant-listp-of-last
     (implies (tterm-case-constant-listp (double-rewrite acl2::x))
              (tterm-case-constant-listp (last acl2::x)))
     :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-remove

(defthm
     tterm-case-constant-listp-of-remove
     (implies (tterm-case-constant-listp acl2::x)
              (tterm-case-constant-listp (remove acl2::a acl2::x)))
     :rule-classes ((:rewrite)))

Theorem: tterm-case-constant-listp-of-revappend

(defthm
     tterm-case-constant-listp-of-revappend
     (equal (tterm-case-constant-listp (revappend acl2::x acl2::y))
            (and (tterm-case-constant-listp (list-fix acl2::x))
                 (tterm-case-constant-listp acl2::y)))
     :rule-classes ((:rewrite)))