• 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
        • Svstmt
        • Sv-tutorial
        • Expressions
          • Rewriting
          • Svex
          • Bit-blasting
          • Functions
          • 4vmask
            • Svex-argmasks
            • 4vmask-p
            • 4vmask-subsumes
            • 4veclist-mask
            • 4vec-mask-to-zero
            • 4vec-mask
            • 4vmasklist-subsumes
            • 4vmask-union
            • 4vec-mask?
            • 4vmask-equiv
            • 4vmask-fix
            • 4vmask-alist
              • 4vmask-alist-p
              • 4vmask-alist-fix
                • 4vmask-acons
                • 4vmask-assoc
                • 4vmask-alist-equiv
              • 4veclist-mask?
              • 4vmasklist
              • 4vmask-empty
            • Why-infinite-width
            • Svex-vars
            • Evaluation
            • Values
          • Symbolic-test-vector
          • Vl-to-svex
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • 4vmask-alist

    4vmask-alist-fix

    (4vmask-alist-fix x) is an fty alist fixing function that follows the fix-keys strategy.

    Signature
    (4vmask-alist-fix x) → fty::newx
    Arguments
    x — Guard (4vmask-alist-p x).
    Returns
    fty::newx — Type (4vmask-alist-p fty::newx).

    Note that in the execution this is just an inline identity function.

    Definitions and Theorems

    Function: 4vmask-alist-fix$inline

    (defun 4vmask-alist-fix$inline (x)
      (declare (xargs :guard (4vmask-alist-p x)))
      (let ((__function__ '4vmask-alist-fix))
        (declare (ignorable __function__))
        (mbe :logic
             (if (atom x)
                 nil
               (if (consp (car x))
                   (cons (cons (svar-fix (caar x))
                               (4vmask-fix (cdar x)))
                         (4vmask-alist-fix (cdr x)))
                 (4vmask-alist-fix (cdr x))))
             :exec x)))

    Theorem: 4vmask-alist-p-of-4vmask-alist-fix

    (defthm 4vmask-alist-p-of-4vmask-alist-fix
      (b* ((fty::newx (4vmask-alist-fix$inline x)))
        (4vmask-alist-p fty::newx))
      :rule-classes :rewrite)

    Theorem: 4vmask-alist-fix-when-4vmask-alist-p

    (defthm 4vmask-alist-fix-when-4vmask-alist-p
      (implies (4vmask-alist-p x)
               (equal (4vmask-alist-fix x) x)))

    Function: 4vmask-alist-equiv$inline

    (defun 4vmask-alist-equiv$inline (x y)
      (declare (xargs :guard (and (4vmask-alist-p x)
                                  (4vmask-alist-p y))))
      (equal (4vmask-alist-fix x)
             (4vmask-alist-fix y)))

    Theorem: 4vmask-alist-equiv-is-an-equivalence

    (defthm 4vmask-alist-equiv-is-an-equivalence
      (and (booleanp (4vmask-alist-equiv x y))
           (4vmask-alist-equiv x x)
           (implies (4vmask-alist-equiv x y)
                    (4vmask-alist-equiv y x))
           (implies (and (4vmask-alist-equiv x y)
                         (4vmask-alist-equiv y z))
                    (4vmask-alist-equiv x z)))
      :rule-classes (:equivalence))

    Theorem: 4vmask-alist-equiv-implies-equal-4vmask-alist-fix-1

    (defthm 4vmask-alist-equiv-implies-equal-4vmask-alist-fix-1
      (implies (4vmask-alist-equiv x x-equiv)
               (equal (4vmask-alist-fix x)
                      (4vmask-alist-fix x-equiv)))
      :rule-classes (:congruence))

    Theorem: 4vmask-alist-fix-under-4vmask-alist-equiv

    (defthm 4vmask-alist-fix-under-4vmask-alist-equiv
      (4vmask-alist-equiv (4vmask-alist-fix x)
                          x)
      :rule-classes (:rewrite :rewrite-quoted-constant))

    Theorem: equal-of-4vmask-alist-fix-1-forward-to-4vmask-alist-equiv

    (defthm equal-of-4vmask-alist-fix-1-forward-to-4vmask-alist-equiv
      (implies (equal (4vmask-alist-fix x) y)
               (4vmask-alist-equiv x y))
      :rule-classes :forward-chaining)

    Theorem: equal-of-4vmask-alist-fix-2-forward-to-4vmask-alist-equiv

    (defthm equal-of-4vmask-alist-fix-2-forward-to-4vmask-alist-equiv
      (implies (equal x (4vmask-alist-fix y))
               (4vmask-alist-equiv x y))
      :rule-classes :forward-chaining)

    Theorem: 4vmask-alist-equiv-of-4vmask-alist-fix-1-forward

    (defthm 4vmask-alist-equiv-of-4vmask-alist-fix-1-forward
      (implies (4vmask-alist-equiv (4vmask-alist-fix x)
                                   y)
               (4vmask-alist-equiv x y))
      :rule-classes :forward-chaining)

    Theorem: 4vmask-alist-equiv-of-4vmask-alist-fix-2-forward

    (defthm 4vmask-alist-equiv-of-4vmask-alist-fix-2-forward
      (implies (4vmask-alist-equiv x (4vmask-alist-fix y))
               (4vmask-alist-equiv x y))
      :rule-classes :forward-chaining)

    Theorem: cons-of-svar-fix-k-under-4vmask-alist-equiv

    (defthm cons-of-svar-fix-k-under-4vmask-alist-equiv
      (4vmask-alist-equiv (cons (cons (svar-fix acl2::k) acl2::v)
                                x)
                          (cons (cons acl2::k acl2::v) x)))

    Theorem: cons-svar-equiv-congruence-on-k-under-4vmask-alist-equiv

    (defthm cons-svar-equiv-congruence-on-k-under-4vmask-alist-equiv
      (implies (svar-equiv acl2::k k-equiv)
               (4vmask-alist-equiv (cons (cons acl2::k acl2::v) x)
                                   (cons (cons k-equiv acl2::v) x)))
      :rule-classes :congruence)

    Theorem: cons-of-4vmask-fix-v-under-4vmask-alist-equiv

    (defthm cons-of-4vmask-fix-v-under-4vmask-alist-equiv
      (4vmask-alist-equiv (cons (cons acl2::k (4vmask-fix acl2::v))
                                x)
                          (cons (cons acl2::k acl2::v) x)))

    Theorem: cons-4vmask-equiv-congruence-on-v-under-4vmask-alist-equiv

    (defthm cons-4vmask-equiv-congruence-on-v-under-4vmask-alist-equiv
      (implies (4vmask-equiv acl2::v v-equiv)
               (4vmask-alist-equiv (cons (cons acl2::k acl2::v) x)
                                   (cons (cons acl2::k v-equiv) x)))
      :rule-classes :congruence)

    Theorem: cons-of-4vmask-alist-fix-y-under-4vmask-alist-equiv

    (defthm cons-of-4vmask-alist-fix-y-under-4vmask-alist-equiv
      (4vmask-alist-equiv (cons x (4vmask-alist-fix y))
                          (cons x y)))

    Theorem: cons-4vmask-alist-equiv-congruence-on-y-under-4vmask-alist-equiv

    (defthm
       cons-4vmask-alist-equiv-congruence-on-y-under-4vmask-alist-equiv
      (implies (4vmask-alist-equiv y y-equiv)
               (4vmask-alist-equiv (cons x y)
                                   (cons x y-equiv)))
      :rule-classes :congruence)

    Theorem: 4vmask-alist-fix-of-acons

    (defthm 4vmask-alist-fix-of-acons
      (equal (4vmask-alist-fix (cons (cons acl2::a acl2::b) x))
             (cons (cons (svar-fix acl2::a)
                         (4vmask-fix acl2::b))
                   (4vmask-alist-fix x))))

    Theorem: 4vmask-alist-fix-of-append

    (defthm 4vmask-alist-fix-of-append
      (equal (4vmask-alist-fix (append std::a std::b))
             (append (4vmask-alist-fix std::a)
                     (4vmask-alist-fix std::b))))

    Theorem: consp-car-of-4vmask-alist-fix

    (defthm consp-car-of-4vmask-alist-fix
      (equal (consp (car (4vmask-alist-fix x)))
             (consp (4vmask-alist-fix x))))