		Search-engine friendly clone of the ACL2 documentation.

Valid-externals

Valid-externals-fix

(valid-externals-fix x) is a usual ACL2::fty omap fixing function.

Signature
(valid-externals-fix x) → *
Arguments: x — Guard (valid-externalsp x).

Definitions and Theorems

Function: valid-externals-fix

(defun valid-externals-fix (x)
  (declare (xargs :guard (valid-externalsp x)))
  (mbe :logic (if (valid-externalsp x) x nil)
       :exec x))

Theorem: valid-externalsp-of-valid-externals-fix

(defthm valid-externalsp-of-valid-externals-fix
  (valid-externalsp (valid-externals-fix x)))

Theorem: valid-externals-fix-when-valid-externalsp

(defthm valid-externals-fix-when-valid-externalsp
  (implies (valid-externalsp x)
           (equal (valid-externals-fix x) x)))

Theorem: emptyp-valid-externals-fix

(defthm emptyp-valid-externals-fix
  (implies (or (omap::emptyp x)
               (not (valid-externalsp x)))
           (omap::emptyp (valid-externals-fix x))))

Theorem: emptyp-of-valid-externals-fix-to-not-valid-externals-or-emptyp

(defthm
     emptyp-of-valid-externals-fix-to-not-valid-externals-or-emptyp
  (equal (omap::emptyp (valid-externals-fix x))
         (or (not (valid-externalsp x))
             (omap::emptyp x))))

Function: valid-externals-equiv$inline

(defun valid-externals-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (valid-externalsp acl2::x)
                              (valid-externalsp acl2::y))))
  (equal (valid-externals-fix acl2::x)
         (valid-externals-fix acl2::y)))

Theorem: valid-externals-equiv-is-an-equivalence

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

Theorem: valid-externals-equiv-implies-equal-valid-externals-fix-1

(defthm valid-externals-equiv-implies-equal-valid-externals-fix-1
  (implies (valid-externals-equiv acl2::x x-equiv)
           (equal (valid-externals-fix acl2::x)
                  (valid-externals-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: valid-externals-fix-under-valid-externals-equiv

(defthm valid-externals-fix-under-valid-externals-equiv
  (valid-externals-equiv (valid-externals-fix acl2::x)
                         acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-valid-externals-fix-1-forward-to-valid-externals-equiv

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

Theorem: equal-of-valid-externals-fix-2-forward-to-valid-externals-equiv

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

Theorem: valid-externals-equiv-of-valid-externals-fix-1-forward

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

Theorem: valid-externals-equiv-of-valid-externals-fix-2-forward

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

Theorem: valid-externals-fix-of-valid-externals-fix-x

(defthm valid-externals-fix-of-valid-externals-fix-x
  (equal (valid-externals-fix (valid-externals-fix x))
         (valid-externals-fix x)))

Theorem: valid-externals-fix-valid-externals-equiv-congruence-on-x

(defthm valid-externals-fix-valid-externals-equiv-congruence-on-x
  (implies (valid-externals-equiv x x-equiv)
           (equal (valid-externals-fix x)
                  (valid-externals-fix x-equiv)))
  :rule-classes :congruence)