		Search-engine friendly clone of the ACL2 documentation.

Run-snippet-info

Run-snippet-info-fix

Fixing function for run-snippet-info structures.

Signature
(run-snippet-info-fix x) → new-x
Arguments: x — Guard (run-snippet-info-p x).
Returns: new-x — Type (run-snippet-info-p new-x).

Definitions and Theorems

Function: run-snippet-info-fix$inline

(defun run-snippet-info-fix$inline (x)
 (declare (xargs :guard (run-snippet-info-p x)))
 (let ((__function__ 'run-snippet-info-fix))
  (declare (ignorable __function__))
  (mbe
    :logic
    (b* ((input-size (nfix (cdr (std::da-nth 0 x))))
         (output-size (pos-fix (cdr (std::da-nth 1 x))))
         (snip-addr (canonical-address-fix (cdr (std::da-nth 2 x))))
         (ret-addr (canonical-address-fix (cdr (std::da-nth 3 x))))
         (step-count (nfix (cdr (std::da-nth 4 x)))))
      (list (cons 'input-size input-size)
            (cons 'output-size output-size)
            (cons 'snip-addr snip-addr)
            (cons 'ret-addr ret-addr)
            (cons 'step-count step-count)))
    :exec x)))

Theorem: run-snippet-info-p-of-run-snippet-info-fix

(defthm run-snippet-info-p-of-run-snippet-info-fix
  (b* ((new-x (run-snippet-info-fix$inline x)))
    (run-snippet-info-p new-x))
  :rule-classes :rewrite)

Theorem: run-snippet-info-fix-when-run-snippet-info-p

(defthm run-snippet-info-fix-when-run-snippet-info-p
  (implies (run-snippet-info-p x)
           (equal (run-snippet-info-fix x) x)))

Function: run-snippet-info-equiv$inline

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

Theorem: run-snippet-info-equiv-is-an-equivalence

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

Theorem: run-snippet-info-equiv-implies-equal-run-snippet-info-fix-1

(defthm run-snippet-info-equiv-implies-equal-run-snippet-info-fix-1
  (implies (run-snippet-info-equiv x x-equiv)
           (equal (run-snippet-info-fix x)
                  (run-snippet-info-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: run-snippet-info-fix-under-run-snippet-info-equiv

(defthm run-snippet-info-fix-under-run-snippet-info-equiv
  (run-snippet-info-equiv (run-snippet-info-fix x)
                          x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-run-snippet-info-fix-1-forward-to-run-snippet-info-equiv

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

Theorem: equal-of-run-snippet-info-fix-2-forward-to-run-snippet-info-equiv

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

Theorem: run-snippet-info-equiv-of-run-snippet-info-fix-1-forward

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

Theorem: run-snippet-info-equiv-of-run-snippet-info-fix-2-forward

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