		Search-engine friendly clone of the ACL2 documentation.

Defsvtv-args

Defsvtv-args-fix

Fixing function for defsvtv-args structures.

Signature
(defsvtv-args-fix x) → new-x
Arguments: x — Guard (defsvtv-args-p x).
Returns: new-x — Type (defsvtv-args-p new-x).

Definitions and Theorems

Function: defsvtv-args-fix$inline

(defun defsvtv-args-fix$inline (x)
 (declare (xargs :guard (defsvtv-args-p x)))
 (let ((__function__ 'defsvtv-args-fix))
  (declare (ignorable __function__))
  (mbe
    :logic
    (b* ((name (acl2::symbol-fix (std::da-nth 0 x)))
         (stages (true-list-list-fix (std::da-nth 1 x)))
         (inputs (true-list-list-fix (std::da-nth 2 x)))
         (overrides (true-list-list-fix (std::da-nth 3 x)))
         (outputs (true-list-list-fix (std::da-nth 4 x)))
         (internals (true-list-list-fix (std::da-nth 5 x)))
         (design (design-fix (std::da-nth 6 x)))
         (design-const (acl2::symbol-fix (std::da-nth 7 x)))
         (labels (acl2::symbol-list-fix (std::da-nth 8 x)))
         (phase-config (phase-fsm-config-fix (std::da-nth 9 x)))
         (clocks (svarlist-fix (std::da-nth 10 x)))
         (phase-scc-limit (acl2::maybe-natp-fix (std::da-nth 11 x)))
         (monotonify (bool-fix (std::da-nth 12 x)))
         (simplify (bool-fix (std::da-nth 13 x)))
         (pre-simplify (bool-fix (std::da-nth 14 x)))
         (pipe-simp (svex-simpconfig-fix (std::da-nth 15 x)))
         (cycle-phases (svtv-cyclephaselist-fix (std::da-nth 16 x)))
         (cycle-phases-p (std::da-nth 17 x))
         (cycle-simp (svex-simpconfig-fix (std::da-nth 18 x)))
         (initial-state-vars (bool-fix (std::da-nth 19 x)))
         (define-macros (std::da-nth 20 x))
         (define-mod (std::da-nth 21 x))
         (parents (std::da-nth 22 x))
         (short (std::da-nth 23 x))
         (long (std::da-nth 24 x))
         (form (std::da-nth 25 x)))
      (list name stages
            inputs overrides outputs internals
            design design-const labels phase-config
            clocks phase-scc-limit monotonify
            simplify pre-simplify pipe-simp
            cycle-phases cycle-phases-p cycle-simp
            initial-state-vars define-macros
            define-mod parents short long form))
    :exec x)))

Theorem: defsvtv-args-p-of-defsvtv-args-fix

(defthm defsvtv-args-p-of-defsvtv-args-fix
  (b* ((new-x (defsvtv-args-fix$inline x)))
    (defsvtv-args-p new-x))
  :rule-classes :rewrite)

Theorem: defsvtv-args-fix-when-defsvtv-args-p

(defthm defsvtv-args-fix-when-defsvtv-args-p
  (implies (defsvtv-args-p x)
           (equal (defsvtv-args-fix x) x)))

Function: defsvtv-args-equiv$inline

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

Theorem: defsvtv-args-equiv-is-an-equivalence

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

Theorem: defsvtv-args-equiv-implies-equal-defsvtv-args-fix-1

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

Theorem: defsvtv-args-fix-under-defsvtv-args-equiv

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

Theorem: equal-of-defsvtv-args-fix-1-forward-to-defsvtv-args-equiv

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

Theorem: equal-of-defsvtv-args-fix-2-forward-to-defsvtv-args-equiv

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

Theorem: defsvtv-args-equiv-of-defsvtv-args-fix-1-forward

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

Theorem: defsvtv-args-equiv-of-defsvtv-args-fix-2-forward

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