• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
          • Svtv-data
          • Defsvtv$
          • Svtv-run
          • Defsvtv-phasewise
          • Svtv
          • Svtv-spec
          • Defsvtv
          • Process.lisp
          • Svtv-doc
          • Svtv-chase$
          • Svtv-versus-stv
          • Svtv-debug-fsm
          • Structure.lisp
            • Svtv-baseentry-p
            • Svtv-entry-p
            • Svtv-outentry-p
            • Svtv-outentry-fix
            • Svtv-baseentry-fix
            • Svtv-entry-fix
            • Svtv-overrideline
            • Svtv-outputline
            • Svtv-condoverride
            • Svtv-line
            • Svtv-inputmap
            • Svtv-outentrylist
              • Svtv-outentrylist-fix
                • Svtv-outentrylist-equiv
                • Svtv-outentrylist-p
              • Svtv-lines
              • Svtv-entrylist
              • Svtv-overridelines
              • Svtv-outputs
              • Svtv-inputtype-p
              • Svtv-dontcare-p
            • Svtv-debug
            • Def-pipeline-thm
            • Expand.lisp
            • Def-cycle-thm
            • Svtv-utilities
            • Svtv-debug$
            • Defsvtv$-phasewise
          • Svex-decomposition-methodology
          • Sv-versus-esim
          • Svex-decomp
          • Svex-compose-dfs
          • Svex-compilation
          • Moddb
          • Svmods
          • Svstmt
          • Sv-tutorial
          • Expressions
          • Symbolic-test-vector
          • Vl-to-svex
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Svtv-outentrylist

    Svtv-outentrylist-fix

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

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

    In the logic, we apply svtv-outentry-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: svtv-outentrylist-fix$inline

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

    Theorem: svtv-outentrylist-p-of-svtv-outentrylist-fix

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

    Theorem: svtv-outentrylist-fix-when-svtv-outentrylist-p

    (defthm svtv-outentrylist-fix-when-svtv-outentrylist-p
      (implies (svtv-outentrylist-p x)
               (equal (svtv-outentrylist-fix x) x)))

    Function: svtv-outentrylist-equiv$inline

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

    Theorem: svtv-outentrylist-equiv-is-an-equivalence

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

    Theorem: svtv-outentrylist-equiv-implies-equal-svtv-outentrylist-fix-1

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

    Theorem: svtv-outentrylist-fix-under-svtv-outentrylist-equiv

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

    Theorem: equal-of-svtv-outentrylist-fix-1-forward-to-svtv-outentrylist-equiv

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

    Theorem: equal-of-svtv-outentrylist-fix-2-forward-to-svtv-outentrylist-equiv

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

    Theorem: svtv-outentrylist-equiv-of-svtv-outentrylist-fix-1-forward

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

    Theorem: svtv-outentrylist-equiv-of-svtv-outentrylist-fix-2-forward

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

    Theorem: car-of-svtv-outentrylist-fix-x-under-svtv-outentry-equiv

    (defthm car-of-svtv-outentrylist-fix-x-under-svtv-outentry-equiv
      (svtv-outentry-equiv (car (svtv-outentrylist-fix x))
                           (car x)))

    Theorem: car-svtv-outentrylist-equiv-congruence-on-x-under-svtv-outentry-equiv

    (defthm
     car-svtv-outentrylist-equiv-congruence-on-x-under-svtv-outentry-equiv
     (implies (svtv-outentrylist-equiv x x-equiv)
              (svtv-outentry-equiv (car x)
                                   (car x-equiv)))
     :rule-classes :congruence)

    Theorem: cdr-of-svtv-outentrylist-fix-x-under-svtv-outentrylist-equiv

    (defthm cdr-of-svtv-outentrylist-fix-x-under-svtv-outentrylist-equiv
      (svtv-outentrylist-equiv (cdr (svtv-outentrylist-fix x))
                               (cdr x)))

    Theorem: cdr-svtv-outentrylist-equiv-congruence-on-x-under-svtv-outentrylist-equiv

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

    Theorem: cons-of-svtv-outentry-fix-x-under-svtv-outentrylist-equiv

    (defthm cons-of-svtv-outentry-fix-x-under-svtv-outentrylist-equiv
      (svtv-outentrylist-equiv (cons (svtv-outentry-fix x) y)
                               (cons x y)))

    Theorem: cons-svtv-outentry-equiv-congruence-on-x-under-svtv-outentrylist-equiv

    (defthm
     cons-svtv-outentry-equiv-congruence-on-x-under-svtv-outentrylist-equiv
     (implies (svtv-outentry-equiv x x-equiv)
              (svtv-outentrylist-equiv (cons x y)
                                       (cons x-equiv y)))
     :rule-classes :congruence)

    Theorem: cons-of-svtv-outentrylist-fix-y-under-svtv-outentrylist-equiv

    (defthm
          cons-of-svtv-outentrylist-fix-y-under-svtv-outentrylist-equiv
      (svtv-outentrylist-equiv (cons x (svtv-outentrylist-fix y))
                               (cons x y)))

    Theorem: cons-svtv-outentrylist-equiv-congruence-on-y-under-svtv-outentrylist-equiv

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

    Theorem: consp-of-svtv-outentrylist-fix

    (defthm consp-of-svtv-outentrylist-fix
      (equal (consp (svtv-outentrylist-fix x))
             (consp x)))

    Theorem: svtv-outentrylist-fix-under-iff

    (defthm svtv-outentrylist-fix-under-iff
      (iff (svtv-outentrylist-fix x)
           (consp x)))

    Theorem: svtv-outentrylist-fix-of-cons

    (defthm svtv-outentrylist-fix-of-cons
      (equal (svtv-outentrylist-fix (cons a x))
             (cons (svtv-outentry-fix a)
                   (svtv-outentrylist-fix x))))

    Theorem: len-of-svtv-outentrylist-fix

    (defthm len-of-svtv-outentrylist-fix
      (equal (len (svtv-outentrylist-fix x))
             (len x)))

    Theorem: svtv-outentrylist-fix-of-append

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

    Theorem: svtv-outentrylist-fix-of-repeat

    (defthm svtv-outentrylist-fix-of-repeat
      (equal (svtv-outentrylist-fix (repeat acl2::n x))
             (repeat acl2::n (svtv-outentry-fix x))))

    Theorem: list-equiv-refines-svtv-outentrylist-equiv

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

    Theorem: nth-of-svtv-outentrylist-fix

    (defthm nth-of-svtv-outentrylist-fix
      (equal (nth acl2::n (svtv-outentrylist-fix x))
             (if (< (nfix acl2::n) (len x))
                 (svtv-outentry-fix (nth acl2::n x))
               nil)))

    Theorem: svtv-outentrylist-equiv-implies-svtv-outentrylist-equiv-append-1

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

    Theorem: svtv-outentrylist-equiv-implies-svtv-outentrylist-equiv-append-2

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

    Theorem: svtv-outentrylist-equiv-implies-svtv-outentrylist-equiv-nthcdr-2

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

    Theorem: svtv-outentrylist-equiv-implies-svtv-outentrylist-equiv-take-2

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