		Search-engine friendly clone of the ACL2 documentation.

Balance-config

Balance-config-fix

Fixing function for balance-config structures.

Signature
(balance-config-fix x) → new-x
Arguments: x — Guard (balance-config-p x).
Returns: new-x — Type (balance-config-p new-x).

Definitions and Theorems

Function: balance-config-fix$inline

(defun balance-config-fix$inline (x)
 (declare (xargs :guard (balance-config-p x)))
 (let ((__function__ 'balance-config-fix))
  (declare (ignorable __function__))
  (mbe
   :logic
   (b* ((search-higher-levels
             (acl2::bool-fix (cdr (std::da-nth 0 (cdr x)))))
        (search-second-lit
             (acl2::bool-fix (cdr (std::da-nth 1 (cdr x)))))
        (search-limit (nfix (cdr (std::da-nth 2 (cdr x)))))
        (supergate-limit (pos-fix (cdr (std::da-nth 3 (cdr x)))))
        (verbosity-level (nfix (cdr (std::da-nth 4 (cdr x)))))
        (gatesimp (gatesimp-fix (cdr (std::da-nth 5 (cdr x))))))
    (cons
       :balance-config (list (cons 'search-higher-levels
                                   search-higher-levels)
                             (cons 'search-second-lit
                                   search-second-lit)
                             (cons 'search-limit search-limit)
                             (cons 'supergate-limit supergate-limit)
                             (cons 'verbosity-level verbosity-level)
                             (cons 'gatesimp gatesimp))))
   :exec x)))

Theorem: balance-config-p-of-balance-config-fix

(defthm balance-config-p-of-balance-config-fix
  (b* ((new-x (balance-config-fix$inline x)))
    (balance-config-p new-x))
  :rule-classes :rewrite)

Theorem: balance-config-fix-when-balance-config-p

(defthm balance-config-fix-when-balance-config-p
  (implies (balance-config-p x)
           (equal (balance-config-fix x) x)))

Function: balance-config-equiv$inline

(defun balance-config-equiv$inline (x acl2::y)
  (declare (xargs :guard (and (balance-config-p x)
                              (balance-config-p acl2::y))))
  (equal (balance-config-fix x)
         (balance-config-fix acl2::y)))

Theorem: balance-config-equiv-is-an-equivalence

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

Theorem: balance-config-equiv-implies-equal-balance-config-fix-1

(defthm balance-config-equiv-implies-equal-balance-config-fix-1
  (implies (balance-config-equiv x x-equiv)
           (equal (balance-config-fix x)
                  (balance-config-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: balance-config-fix-under-balance-config-equiv

(defthm balance-config-fix-under-balance-config-equiv
  (balance-config-equiv (balance-config-fix x)
                        x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-balance-config-fix-1-forward-to-balance-config-equiv

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

Theorem: equal-of-balance-config-fix-2-forward-to-balance-config-equiv

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

Theorem: balance-config-equiv-of-balance-config-fix-1-forward

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

Theorem: balance-config-equiv-of-balance-config-fix-2-forward

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