		Search-engine friendly clone of the ACL2 documentation.

Syndef::acid4

Syndef::acid4-FIX

Fixing function for syndef::acid4 structures.

Signature
(syndef::|acid4-FIX| syndef::x) → syndef::new-x
Arguments: syndef::x — Guard (syndef::|acid4-P| syndef::x).
Returns: syndef::new-x — Type (syndef::|acid4-P| syndef::new-x).

Definitions and Theorems

Function: acid4-fix$inline

(defun syndef::|acid4-FIX$INLINE| (syndef::x)
 (declare (xargs :guard (syndef::|acid4-P| syndef::x)))
 (let ((__function__ 'syndef::|acid4-FIX|))
  (declare (ignorable __function__))
  (mbe
   :logic
   (b* ((syndef::|id| (ifix (cdr (std::da-nth 0 (cdr syndef::x))))))
     (cons :|acid4| (list (cons 'syndef::|id| syndef::|id|))))
   :exec syndef::x)))

Theorem: acid4-p-of-acid4-fix

(defthm syndef::|acid4-P-OF-acid4-FIX|
  (b* ((syndef::new-x (syndef::|acid4-FIX$INLINE| syndef::x)))
    (syndef::|acid4-P| syndef::new-x))
  :rule-classes :rewrite)

Theorem: acid4-fix-when-acid4-p

(defthm syndef::|acid4-FIX-WHEN-acid4-P|
  (implies (syndef::|acid4-P| syndef::x)
           (equal (syndef::|acid4-FIX| syndef::x)
                  syndef::x)))

Function: acid4-equiv$inline

(defun syndef::|acid4-EQUIV$INLINE| (acl2::x acl2::y)
  (declare (xargs :guard (and (syndef::|acid4-P| acl2::x)
                              (syndef::|acid4-P| acl2::y))))
  (equal (syndef::|acid4-FIX| acl2::x)
         (syndef::|acid4-FIX| acl2::y)))

Theorem: acid4-equiv-is-an-equivalence

(defthm syndef::|acid4-EQUIV-IS-AN-EQUIVALENCE|
  (and (booleanp (syndef::|acid4-EQUIV| syndef::x syndef::y))
       (syndef::|acid4-EQUIV| syndef::x syndef::x)
       (implies (syndef::|acid4-EQUIV| syndef::x syndef::y)
                (syndef::|acid4-EQUIV| syndef::y syndef::x))
       (implies (and (syndef::|acid4-EQUIV| syndef::x syndef::y)
                     (syndef::|acid4-EQUIV| syndef::y syndef::z))
                (syndef::|acid4-EQUIV| syndef::x syndef::z)))
  :rule-classes (:equivalence))

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

(defthm syndef::|acid4-EQUIV-IMPLIES-EQUAL-acid4-FIX-1|
  (implies (syndef::|acid4-EQUIV| acl2::x syndef::x-equiv)
           (equal (syndef::|acid4-FIX| acl2::x)
                  (syndef::|acid4-FIX| syndef::x-equiv)))
  :rule-classes (:congruence))

Theorem: acid4-fix-under-acid4-equiv

(defthm syndef::|acid4-FIX-UNDER-acid4-EQUIV|
  (syndef::|acid4-EQUIV| (syndef::|acid4-FIX| acl2::x)
                         acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

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

(defthm syndef::|EQUAL-OF-acid4-FIX-1-FORWARD-TO-acid4-EQUIV|
  (implies (equal (syndef::|acid4-FIX| acl2::x)
                  acl2::y)
           (syndef::|acid4-EQUIV| acl2::x acl2::y))
  :rule-classes :forward-chaining)

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

(defthm syndef::|EQUAL-OF-acid4-FIX-2-FORWARD-TO-acid4-EQUIV|
  (implies (equal acl2::x (syndef::|acid4-FIX| acl2::y))
           (syndef::|acid4-EQUIV| acl2::x acl2::y))
  :rule-classes :forward-chaining)

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

(defthm syndef::|acid4-EQUIV-OF-acid4-FIX-1-FORWARD|
  (implies (syndef::|acid4-EQUIV| (syndef::|acid4-FIX| acl2::x)
                                  acl2::y)
           (syndef::|acid4-EQUIV| acl2::x acl2::y))
  :rule-classes :forward-chaining)

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

(defthm syndef::|acid4-EQUIV-OF-acid4-FIX-2-FORWARD|
  (implies
       (syndef::|acid4-EQUIV| acl2::x (syndef::|acid4-FIX| acl2::y))
       (syndef::|acid4-EQUIV| acl2::x acl2::y))
  :rule-classes :forward-chaining)