		Search-engine friendly clone of the ACL2 documentation.

Any-nat-map

Any-nat-mfix

(any-nat-mfix x) is a usual fty omap fixing function.

Signature
(any-nat-mfix x) → *
Arguments: x — Guard (any-nat-mapp x).

Definitions and Theorems

Function: any-nat-mfix

(defun any-nat-mfix (x)
  (declare (xargs :guard (any-nat-mapp x)))
  (mbe :logic (if (any-nat-mapp x) x nil)
       :exec x))

Theorem: any-nat-mapp-of-any-nat-mfix

(defthm any-nat-mapp-of-any-nat-mfix
  (any-nat-mapp (any-nat-mfix x)))

Theorem: any-nat-mfix-when-any-nat-mapp

(defthm any-nat-mfix-when-any-nat-mapp
  (implies (any-nat-mapp x)
           (equal (any-nat-mfix x) x)))

Theorem: emptyp-any-nat-mfix

(defthm emptyp-any-nat-mfix
  (implies (or (omap::emptyp x)
               (not (any-nat-mapp x)))
           (omap::emptyp (any-nat-mfix x))))

Theorem: emptyp-of-any-nat-mfix-to-not-any-nat-map-or-emptyp

(defthm emptyp-of-any-nat-mfix-to-not-any-nat-map-or-emptyp
  (equal (omap::emptyp (any-nat-mfix x))
         (or (not (any-nat-mapp x))
             (omap::emptyp x))))

Function: any-nat-mequiv$inline

(defun any-nat-mequiv$inline (x y)
  (declare (xargs :guard (and (any-nat-mapp x)
                              (any-nat-mapp y))))
  (equal (any-nat-mfix x)
         (any-nat-mfix y)))

Theorem: any-nat-mequiv-is-an-equivalence

(defthm any-nat-mequiv-is-an-equivalence
  (and (booleanp (any-nat-mequiv x y))
       (any-nat-mequiv x x)
       (implies (any-nat-mequiv x y)
                (any-nat-mequiv y x))
       (implies (and (any-nat-mequiv x y)
                     (any-nat-mequiv y z))
                (any-nat-mequiv x z)))
  :rule-classes (:equivalence))

Theorem: any-nat-mequiv-implies-equal-any-nat-mfix-1

(defthm any-nat-mequiv-implies-equal-any-nat-mfix-1
  (implies (any-nat-mequiv x x-equiv)
           (equal (any-nat-mfix x)
                  (any-nat-mfix x-equiv)))
  :rule-classes (:congruence))

Theorem: any-nat-mfix-under-any-nat-mequiv

(defthm any-nat-mfix-under-any-nat-mequiv
  (any-nat-mequiv (any-nat-mfix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-any-nat-mfix-1-forward-to-any-nat-mequiv

(defthm equal-of-any-nat-mfix-1-forward-to-any-nat-mequiv
  (implies (equal (any-nat-mfix x) y)
           (any-nat-mequiv x y))
  :rule-classes :forward-chaining)

Theorem: equal-of-any-nat-mfix-2-forward-to-any-nat-mequiv

(defthm equal-of-any-nat-mfix-2-forward-to-any-nat-mequiv
  (implies (equal x (any-nat-mfix y))
           (any-nat-mequiv x y))
  :rule-classes :forward-chaining)

Theorem: any-nat-mequiv-of-any-nat-mfix-1-forward

(defthm any-nat-mequiv-of-any-nat-mfix-1-forward
  (implies (any-nat-mequiv (any-nat-mfix x) y)
           (any-nat-mequiv x y))
  :rule-classes :forward-chaining)

Theorem: any-nat-mequiv-of-any-nat-mfix-2-forward

(defthm any-nat-mequiv-of-any-nat-mfix-2-forward
  (implies (any-nat-mequiv x (any-nat-mfix y))
           (any-nat-mequiv x y))
  :rule-classes :forward-chaining)