• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-fixpoint-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Moddb
        • Svex-compilation
        • Svmods
        • Svstmt
        • Sv-tutorial
        • Expressions
          • Rewriting
          • Svex
            • Svar
              • Svar-p
              • Svar-fix
              • Make-svar
              • Svar-equiv
              • Svar->override-test
              • Svar->override-val
              • Svar->nonblocking
              • Change-svar
              • Svar->delay
              • Svarlist
                • Svarlist-p
                • Svarlist-fix
                  • Svarlist-equiv
                • Svar->name
                • Svar-map
                • Svar-alist
              • Least-fixpoint
              • Svex-p
              • Svex-select
              • Svex-alist
              • Svex-equiv
              • Svexlist
              • Svex-call
              • Fnsym
              • Svex-quote
              • Svex-var
              • Svcall-rw
              • Svcall
              • Svex-kind
              • Svcall*
              • Svex-fix
              • Svex-count
              • Svex-1z
              • Svex-1x
              • Svex-z
              • Svex-x
            • Bit-blasting
            • Functions
            • 4vmask
            • Why-infinite-width
            • Svex-vars
            • Evaluation
            • Values
          • Symbolic-test-vector
          • Vl-to-svex
        • Fgl
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Testing-utilities
      • Math
    • Svarlist

    Svarlist-fix

    (svarlist-fix x) is a usual fty list fixing function.

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

    In the logic, we apply svar-fix to each member of the x. In the execution, none of that is actually necessary and this is just an inlined identity function.

    Definitions and Theorems

    Function: svarlist-fix$inline

    (defun svarlist-fix$inline (x)
           (declare (xargs :guard (svarlist-p x)))
           (let ((__function__ 'svarlist-fix))
                (declare (ignorable __function__))
                (mbe :logic (if (atom x)
                                nil
                                (cons (svar-fix (car x))
                                      (svarlist-fix (cdr x))))
                     :exec x)))

    Theorem: svarlist-p-of-svarlist-fix

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

    Theorem: svarlist-fix-when-svarlist-p

    (defthm svarlist-fix-when-svarlist-p
            (implies (svarlist-p x)
                     (equal (svarlist-fix x) x)))

    Function: svarlist-equiv$inline

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

    Theorem: svarlist-equiv-is-an-equivalence

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

    Theorem: svarlist-equiv-implies-equal-svarlist-fix-1

    (defthm svarlist-equiv-implies-equal-svarlist-fix-1
            (implies (svarlist-equiv x x-equiv)
                     (equal (svarlist-fix x)
                            (svarlist-fix x-equiv)))
            :rule-classes (:congruence))

    Theorem: svarlist-fix-under-svarlist-equiv

    (defthm svarlist-fix-under-svarlist-equiv
            (svarlist-equiv (svarlist-fix x) x)
            :rule-classes (:rewrite :rewrite-quoted-constant))

    Theorem: equal-of-svarlist-fix-1-forward-to-svarlist-equiv

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

    Theorem: equal-of-svarlist-fix-2-forward-to-svarlist-equiv

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

    Theorem: svarlist-equiv-of-svarlist-fix-1-forward

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

    Theorem: svarlist-equiv-of-svarlist-fix-2-forward

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

    Theorem: car-of-svarlist-fix-x-under-svar-equiv

    (defthm car-of-svarlist-fix-x-under-svar-equiv
            (svar-equiv (car (svarlist-fix x))
                        (car x)))

    Theorem: car-svarlist-equiv-congruence-on-x-under-svar-equiv

    (defthm car-svarlist-equiv-congruence-on-x-under-svar-equiv
            (implies (svarlist-equiv x x-equiv)
                     (svar-equiv (car x) (car x-equiv)))
            :rule-classes :congruence)

    Theorem: cdr-of-svarlist-fix-x-under-svarlist-equiv

    (defthm cdr-of-svarlist-fix-x-under-svarlist-equiv
            (svarlist-equiv (cdr (svarlist-fix x))
                            (cdr x)))

    Theorem: cdr-svarlist-equiv-congruence-on-x-under-svarlist-equiv

    (defthm cdr-svarlist-equiv-congruence-on-x-under-svarlist-equiv
            (implies (svarlist-equiv x x-equiv)
                     (svarlist-equiv (cdr x) (cdr x-equiv)))
            :rule-classes :congruence)

    Theorem: cons-of-svar-fix-x-under-svarlist-equiv

    (defthm cons-of-svar-fix-x-under-svarlist-equiv
            (svarlist-equiv (cons (svar-fix x) y)
                            (cons x y)))

    Theorem: cons-svar-equiv-congruence-on-x-under-svarlist-equiv

    (defthm cons-svar-equiv-congruence-on-x-under-svarlist-equiv
            (implies (svar-equiv x x-equiv)
                     (svarlist-equiv (cons x y)
                                     (cons x-equiv y)))
            :rule-classes :congruence)

    Theorem: cons-of-svarlist-fix-y-under-svarlist-equiv

    (defthm cons-of-svarlist-fix-y-under-svarlist-equiv
            (svarlist-equiv (cons x (svarlist-fix y))
                            (cons x y)))

    Theorem: cons-svarlist-equiv-congruence-on-y-under-svarlist-equiv

    (defthm cons-svarlist-equiv-congruence-on-y-under-svarlist-equiv
            (implies (svarlist-equiv y y-equiv)
                     (svarlist-equiv (cons x y)
                                     (cons x y-equiv)))
            :rule-classes :congruence)

    Theorem: consp-of-svarlist-fix

    (defthm consp-of-svarlist-fix
            (equal (consp (svarlist-fix x))
                   (consp x)))

    Theorem: svarlist-fix-under-iff

    (defthm svarlist-fix-under-iff
            (iff (svarlist-fix x) (consp x)))

    Theorem: svarlist-fix-of-cons

    (defthm svarlist-fix-of-cons
            (equal (svarlist-fix (cons a x))
                   (cons (svar-fix a) (svarlist-fix x))))

    Theorem: len-of-svarlist-fix

    (defthm len-of-svarlist-fix
            (equal (len (svarlist-fix x)) (len x)))

    Theorem: svarlist-fix-of-append

    (defthm svarlist-fix-of-append
            (equal (svarlist-fix (append std::a std::b))
                   (append (svarlist-fix std::a)
                           (svarlist-fix std::b))))

    Theorem: svarlist-fix-of-repeat

    (defthm svarlist-fix-of-repeat
            (equal (svarlist-fix (repeat acl2::n x))
                   (repeat acl2::n (svar-fix x))))

    Theorem: list-equiv-refines-svarlist-equiv

    (defthm list-equiv-refines-svarlist-equiv
            (implies (list-equiv x y)
                     (svarlist-equiv x y))
            :rule-classes :refinement)

    Theorem: nth-of-svarlist-fix

    (defthm nth-of-svarlist-fix
            (equal (nth acl2::n (svarlist-fix x))
                   (if (< (nfix acl2::n) (len x))
                       (svar-fix (nth acl2::n x))
                       nil)))

    Theorem: svarlist-equiv-implies-svarlist-equiv-append-1

    (defthm svarlist-equiv-implies-svarlist-equiv-append-1
            (implies (svarlist-equiv x fty::x-equiv)
                     (svarlist-equiv (append x y)
                                     (append fty::x-equiv y)))
            :rule-classes (:congruence))

    Theorem: svarlist-equiv-implies-svarlist-equiv-append-2

    (defthm svarlist-equiv-implies-svarlist-equiv-append-2
            (implies (svarlist-equiv y fty::y-equiv)
                     (svarlist-equiv (append x y)
                                     (append x fty::y-equiv)))
            :rule-classes (:congruence))

    Theorem: svarlist-equiv-implies-svarlist-equiv-nthcdr-2

    (defthm svarlist-equiv-implies-svarlist-equiv-nthcdr-2
            (implies (svarlist-equiv acl2::l l-equiv)
                     (svarlist-equiv (nthcdr acl2::n acl2::l)
                                     (nthcdr acl2::n l-equiv)))
            :rule-classes (:congruence))

    Theorem: svarlist-equiv-implies-svarlist-equiv-take-2

    (defthm svarlist-equiv-implies-svarlist-equiv-take-2
            (implies (svarlist-equiv acl2::l l-equiv)
                     (svarlist-equiv (take acl2::n acl2::l)
                                     (take acl2::n l-equiv)))
            :rule-classes (:congruence))