		Search-engine friendly clone of the ACL2 documentation.

Fraig-output-map-entry

Fraig-output-map-entry-fix

Fixing function for fraig-output-map-entry structures.

Signature
(fraig-output-map-entry-fix x) → new-x
Arguments: x — Guard (fraig-output-map-entry-p x).
Returns: new-x — Type (fraig-output-map-entry-p new-x).

Definitions and Theorems

Function: fraig-output-map-entry-fix$inline

(defun fraig-output-map-entry-fix$inline (x)
  (declare (xargs :guard (fraig-output-map-entry-p x)))
  (let ((__function__ 'fraig-output-map-entry-fix))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((type (fraig-output-type-fix (cdr (std::da-nth 0 x))))
              (count (nfix (cdr (std::da-nth 1 x)))))
           (list (cons 'type type)
                 (cons 'count count)))
         :exec x)))

Theorem: fraig-output-map-entry-p-of-fraig-output-map-entry-fix

(defthm fraig-output-map-entry-p-of-fraig-output-map-entry-fix
  (b* ((new-x (fraig-output-map-entry-fix$inline x)))
    (fraig-output-map-entry-p new-x))
  :rule-classes :rewrite)

Theorem: fraig-output-map-entry-fix-when-fraig-output-map-entry-p

(defthm fraig-output-map-entry-fix-when-fraig-output-map-entry-p
  (implies (fraig-output-map-entry-p x)
           (equal (fraig-output-map-entry-fix x)
                  x)))

Function: fraig-output-map-entry-equiv$inline

(defun fraig-output-map-entry-equiv$inline (x acl2::y)
  (declare (xargs :guard (and (fraig-output-map-entry-p x)
                              (fraig-output-map-entry-p acl2::y))))
  (equal (fraig-output-map-entry-fix x)
         (fraig-output-map-entry-fix acl2::y)))

Theorem: fraig-output-map-entry-equiv-is-an-equivalence

(defthm fraig-output-map-entry-equiv-is-an-equivalence
  (and (booleanp (fraig-output-map-entry-equiv x y))
       (fraig-output-map-entry-equiv x x)
       (implies (fraig-output-map-entry-equiv x y)
                (fraig-output-map-entry-equiv y x))
       (implies (and (fraig-output-map-entry-equiv x y)
                     (fraig-output-map-entry-equiv y z))
                (fraig-output-map-entry-equiv x z)))
  :rule-classes (:equivalence))

Theorem: fraig-output-map-entry-equiv-implies-equal-fraig-output-map-entry-fix-1

(defthm
 fraig-output-map-entry-equiv-implies-equal-fraig-output-map-entry-fix-1
 (implies (fraig-output-map-entry-equiv x x-equiv)
          (equal (fraig-output-map-entry-fix x)
                 (fraig-output-map-entry-fix x-equiv)))
 :rule-classes (:congruence))

Theorem: fraig-output-map-entry-fix-under-fraig-output-map-entry-equiv

(defthm
      fraig-output-map-entry-fix-under-fraig-output-map-entry-equiv
  (fraig-output-map-entry-equiv (fraig-output-map-entry-fix x)
                                x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-fraig-output-map-entry-fix-1-forward-to-fraig-output-map-entry-equiv

(defthm
 equal-of-fraig-output-map-entry-fix-1-forward-to-fraig-output-map-entry-equiv
 (implies (equal (fraig-output-map-entry-fix x)
                 acl2::y)
          (fraig-output-map-entry-equiv x acl2::y))
 :rule-classes :forward-chaining)

Theorem: equal-of-fraig-output-map-entry-fix-2-forward-to-fraig-output-map-entry-equiv

(defthm
 equal-of-fraig-output-map-entry-fix-2-forward-to-fraig-output-map-entry-equiv
 (implies (equal x (fraig-output-map-entry-fix acl2::y))
          (fraig-output-map-entry-equiv x acl2::y))
 :rule-classes :forward-chaining)

Theorem: fraig-output-map-entry-equiv-of-fraig-output-map-entry-fix-1-forward

(defthm
 fraig-output-map-entry-equiv-of-fraig-output-map-entry-fix-1-forward
 (implies
      (fraig-output-map-entry-equiv (fraig-output-map-entry-fix x)
                                    acl2::y)
      (fraig-output-map-entry-equiv x acl2::y))
 :rule-classes :forward-chaining)

Theorem: fraig-output-map-entry-equiv-of-fraig-output-map-entry-fix-2-forward

(defthm
 fraig-output-map-entry-equiv-of-fraig-output-map-entry-fix-2-forward
 (implies (fraig-output-map-entry-equiv
               x (fraig-output-map-entry-fix acl2::y))
          (fraig-output-map-entry-equiv x acl2::y))
 :rule-classes :forward-chaining)