		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Wellformed

Fixtype of the well-formedness indicator.

This is returned by the ACL2 static semantic checking functions when an abstract syntactic entity passes the static semantic checks and there is no additional information to return. When the static semantic checks fail, those functions return errors instead; see wellformed-result.

Definitions and Theorems

Function: wellformed-equiv$inline

(defun wellformed-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (wellformedp acl2::x)
                              (wellformedp acl2::y))))
  (equal (wellformed-fix acl2::x)
         (wellformed-fix acl2::y)))

Theorem: wellformed-equiv-is-an-equivalence

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

Theorem: wellformed-equiv-implies-equal-wellformed-fix-1

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

Theorem: wellformed-fix-under-wellformed-equiv

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

Theorem: equal-of-wellformed-fix-1-forward-to-wellformed-equiv

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

Theorem: equal-of-wellformed-fix-2-forward-to-wellformed-equiv

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

Theorem: wellformed-equiv-of-wellformed-fix-1-forward

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

Theorem: wellformed-equiv-of-wellformed-fix-2-forward

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

Subtopics

Wellformed-fix: Fixer for wellformed.
Wellformedp: Recognizer for wellformed.