• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
          • Language
          • Representation
          • Transformation-tools
            • Simpadd0
            • Splitgso
            • Constant-propagation
            • Split-fn
            • Specialize
            • Split-all-gso
            • Copy-fn
            • Rename
              • Abstract-syntax-rename
              • Ident-ident-subst
              • Ident-ident-alist
                • Ident-ident-alistp
                  • Ident-ident-alist-fix
                  • Ident-ident-alist-equiv
              • Utilities
            • Insertion-sort
            • Pack
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Ident-ident-alist

    Ident-ident-alistp

    Recognizer for ident-ident-alist.

    Signature
    (ident-ident-alistp x) → *

    Definitions and Theorems

    Function: ident-ident-alistp

    (defun ident-ident-alistp (x)
      (declare (xargs :guard t))
      (let ((__function__ 'ident-ident-alistp))
        (declare (ignorable __function__))
        (if (atom x)
            (eq x nil)
          (and (consp (car x))
               (identp (caar x))
               (identp (cdar x))
               (ident-ident-alistp (cdr x))))))

    Theorem: ident-ident-alistp-of-revappend

    (defthm ident-ident-alistp-of-revappend
      (equal (ident-ident-alistp (revappend acl2::x acl2::y))
             (and (ident-ident-alistp (list-fix acl2::x))
                  (ident-ident-alistp acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-remove

    (defthm ident-ident-alistp-of-remove
      (implies (ident-ident-alistp acl2::x)
               (ident-ident-alistp (remove acl2::a acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-last

    (defthm ident-ident-alistp-of-last
      (implies (ident-ident-alistp (double-rewrite acl2::x))
               (ident-ident-alistp (last acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-nthcdr

    (defthm ident-ident-alistp-of-nthcdr
      (implies (ident-ident-alistp (double-rewrite acl2::x))
               (ident-ident-alistp (nthcdr acl2::n acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-butlast

    (defthm ident-ident-alistp-of-butlast
      (implies (ident-ident-alistp (double-rewrite acl2::x))
               (ident-ident-alistp (butlast acl2::x acl2::n)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-update-nth

    (defthm ident-ident-alistp-of-update-nth
     (implies
          (ident-ident-alistp (double-rewrite acl2::x))
          (iff (ident-ident-alistp (update-nth acl2::n acl2::y acl2::x))
               (and (and (consp acl2::y)
                         (identp (car acl2::y))
                         (identp (cdr acl2::y)))
                    (or (<= (nfix acl2::n) (len acl2::x))
                        (and (consp nil)
                             (identp (car nil))
                             (identp (cdr nil)))))))
     :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-repeat

    (defthm ident-ident-alistp-of-repeat
      (iff (ident-ident-alistp (repeat acl2::n acl2::x))
           (or (and (consp acl2::x)
                    (identp (car acl2::x))
                    (identp (cdr acl2::x)))
               (zp acl2::n)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-take

    (defthm ident-ident-alistp-of-take
      (implies (ident-ident-alistp (double-rewrite acl2::x))
               (iff (ident-ident-alistp (take acl2::n acl2::x))
                    (or (and (consp nil)
                             (identp (car nil))
                             (identp (cdr nil)))
                        (<= (nfix acl2::n) (len acl2::x)))))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-union-equal

    (defthm ident-ident-alistp-of-union-equal
      (equal (ident-ident-alistp (union-equal acl2::x acl2::y))
             (and (ident-ident-alistp (list-fix acl2::x))
                  (ident-ident-alistp (double-rewrite acl2::y))))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-intersection-equal-2

    (defthm ident-ident-alistp-of-intersection-equal-2
     (implies (ident-ident-alistp (double-rewrite acl2::y))
              (ident-ident-alistp (intersection-equal acl2::x acl2::y)))
     :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-intersection-equal-1

    (defthm ident-ident-alistp-of-intersection-equal-1
     (implies (ident-ident-alistp (double-rewrite acl2::x))
              (ident-ident-alistp (intersection-equal acl2::x acl2::y)))
     :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-set-difference-equal

    (defthm ident-ident-alistp-of-set-difference-equal
      (implies
           (ident-ident-alistp acl2::x)
           (ident-ident-alistp (set-difference-equal acl2::x acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-when-subsetp-equal

    (defthm ident-ident-alistp-when-subsetp-equal
      (and (implies (and (subsetp-equal acl2::x acl2::y)
                         (ident-ident-alistp acl2::y))
                    (equal (ident-ident-alistp acl2::x)
                           (true-listp acl2::x)))
           (implies (and (ident-ident-alistp acl2::y)
                         (subsetp-equal acl2::x acl2::y))
                    (equal (ident-ident-alistp acl2::x)
                           (true-listp acl2::x))))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-rcons

    (defthm ident-ident-alistp-of-rcons
      (iff (ident-ident-alistp (rcons acl2::a acl2::x))
           (and (and (consp acl2::a)
                     (identp (car acl2::a))
                     (identp (cdr acl2::a)))
                (ident-ident-alistp (list-fix acl2::x))))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-append

    (defthm ident-ident-alistp-of-append
      (equal (ident-ident-alistp (append acl2::a acl2::b))
             (and (ident-ident-alistp (list-fix acl2::a))
                  (ident-ident-alistp acl2::b)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-rev

    (defthm ident-ident-alistp-of-rev
      (equal (ident-ident-alistp (rev acl2::x))
             (ident-ident-alistp (list-fix acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-duplicated-members

    (defthm ident-ident-alistp-of-duplicated-members
      (implies (ident-ident-alistp acl2::x)
               (ident-ident-alistp (duplicated-members acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-difference

    (defthm ident-ident-alistp-of-difference
      (implies (ident-ident-alistp acl2::x)
               (ident-ident-alistp (difference acl2::x acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-intersect-2

    (defthm ident-ident-alistp-of-intersect-2
      (implies (ident-ident-alistp acl2::y)
               (ident-ident-alistp (intersect acl2::x acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-intersect-1

    (defthm ident-ident-alistp-of-intersect-1
      (implies (ident-ident-alistp acl2::x)
               (ident-ident-alistp (intersect acl2::x acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-union

    (defthm ident-ident-alistp-of-union
      (iff (ident-ident-alistp (union acl2::x acl2::y))
           (and (ident-ident-alistp (sfix acl2::x))
                (ident-ident-alistp (sfix acl2::y))))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-mergesort

    (defthm ident-ident-alistp-of-mergesort
      (iff (ident-ident-alistp (mergesort acl2::x))
           (ident-ident-alistp (list-fix acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-delete

    (defthm ident-ident-alistp-of-delete
      (implies (ident-ident-alistp acl2::x)
               (ident-ident-alistp (delete acl2::k acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-insert

    (defthm ident-ident-alistp-of-insert
      (iff (ident-ident-alistp (insert acl2::a acl2::x))
           (and (ident-ident-alistp (sfix acl2::x))
                (and (consp acl2::a)
                     (identp (car acl2::a))
                     (identp (cdr acl2::a)))))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-sfix

    (defthm ident-ident-alistp-of-sfix
      (iff (ident-ident-alistp (sfix acl2::x))
           (or (ident-ident-alistp acl2::x)
               (not (setp acl2::x))))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-list-fix

    (defthm ident-ident-alistp-of-list-fix
      (implies (ident-ident-alistp acl2::x)
               (ident-ident-alistp (list-fix acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: true-listp-when-ident-ident-alistp-compound-recognizer

    (defthm true-listp-when-ident-ident-alistp-compound-recognizer
      (implies (ident-ident-alistp acl2::x)
               (true-listp acl2::x))
      :rule-classes :compound-recognizer)

    Theorem: ident-ident-alistp-when-not-consp

    (defthm ident-ident-alistp-when-not-consp
      (implies (not (consp acl2::x))
               (equal (ident-ident-alistp acl2::x)
                      (not acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-cdr-when-ident-ident-alistp

    (defthm ident-ident-alistp-of-cdr-when-ident-ident-alistp
      (implies (ident-ident-alistp (double-rewrite acl2::x))
               (ident-ident-alistp (cdr acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-cons

    (defthm ident-ident-alistp-of-cons
      (equal (ident-ident-alistp (cons acl2::a acl2::x))
             (and (and (consp acl2::a)
                       (identp (car acl2::a))
                       (identp (cdr acl2::a)))
                  (ident-ident-alistp acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-remove-assoc

    (defthm ident-ident-alistp-of-remove-assoc
      (implies
           (ident-ident-alistp acl2::x)
           (ident-ident-alistp (remove-assoc-equal acl2::name acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-put-assoc

    (defthm ident-ident-alistp-of-put-assoc
      (implies (and (ident-ident-alistp acl2::x))
               (iff (ident-ident-alistp
                         (put-assoc-equal acl2::name acl2::val acl2::x))
                    (and (identp acl2::name)
                         (identp acl2::val))))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-fast-alist-clean

    (defthm ident-ident-alistp-of-fast-alist-clean
      (implies (ident-ident-alistp acl2::x)
               (ident-ident-alistp (fast-alist-clean acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-hons-shrink-alist

    (defthm ident-ident-alistp-of-hons-shrink-alist
      (implies (and (ident-ident-alistp acl2::x)
                    (ident-ident-alistp acl2::y))
               (ident-ident-alistp (hons-shrink-alist acl2::x acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: ident-ident-alistp-of-hons-acons

    (defthm ident-ident-alistp-of-hons-acons
      (equal (ident-ident-alistp (hons-acons acl2::a acl2::n acl2::x))
             (and (identp acl2::a)
                  (identp acl2::n)
                  (ident-ident-alistp acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: identp-of-cdr-of-hons-assoc-equal-when-ident-ident-alistp

    (defthm identp-of-cdr-of-hons-assoc-equal-when-ident-ident-alistp
      (implies (ident-ident-alistp acl2::x)
               (iff (identp (cdr (hons-assoc-equal acl2::k acl2::x)))
                    (or (hons-assoc-equal acl2::k acl2::x)
                        (identp nil))))
      :rule-classes ((:rewrite)))

    Theorem: alistp-when-ident-ident-alistp-rewrite

    (defthm alistp-when-ident-ident-alistp-rewrite
      (implies (ident-ident-alistp acl2::x)
               (alistp acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: alistp-when-ident-ident-alistp

    (defthm alistp-when-ident-ident-alistp
      (implies (ident-ident-alistp acl2::x)
               (alistp acl2::x))
      :rule-classes :tau-system)

    Theorem: identp-of-cdar-when-ident-ident-alistp

    (defthm identp-of-cdar-when-ident-ident-alistp
      (implies (ident-ident-alistp acl2::x)
               (iff (identp (cdar acl2::x))
                    (or (consp acl2::x) (identp nil))))
      :rule-classes ((:rewrite)))

    Theorem: identp-of-caar-when-ident-ident-alistp

    (defthm identp-of-caar-when-ident-ident-alistp
      (implies (ident-ident-alistp acl2::x)
               (iff (identp (caar acl2::x))
                    (or (consp acl2::x) (identp nil))))
      :rule-classes ((:rewrite)))