		Search-engine friendly clone of the ACL2 documentation.

Character-any-map

Character-any-mfix

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

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

Definitions and Theorems

Function: character-any-mfix

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

Theorem: character-any-mapp-of-character-any-mfix

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

Theorem: character-any-mfix-when-character-any-mapp

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

Theorem: emptyp-character-any-mfix

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

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

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

Function: character-any-mequiv$inline

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

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

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

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

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

Theorem: character-any-mfix-under-character-any-mequiv

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

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

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

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

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

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

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

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

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