		Search-engine friendly clone of the ACL2 documentation.

Character-any-map

Character-any-mequiv

Basic equivalence relation for character-any-map structures.

Definitions and Theorems

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)