		Search-engine friendly clone of the ACL2 documentation.

Dead-code-eliminator-execution

Soutcome-result-okeq

Equality of statement outcome results modulo errors.

Signature
(soutcome-result-okeq x y) → yes/no
Arguments: x — Guard (soutcome-resultp x).; y — Guard (soutcome-resultp y).
Returns: yes/no — Type (booleanp yes/no).

This is the equivalence relation on statement outcomes discussed in dead-code-eliminator-execution.

Definitions and Theorems

Function: soutcome-result-okeq

(defun soutcome-result-okeq (x y)
  (declare (xargs :guard (and (soutcome-resultp x)
                              (soutcome-resultp y))))
  (let ((__function__ 'soutcome-result-okeq))
    (declare (ignorable __function__))
    (b* ((x (soutcome-result-fix x))
         (y (soutcome-result-fix y)))
      (cond ((reserrp x) (reserrp y))
            ((reserrp y) (reserrp x))
            (t (equal x y))))))

Theorem: booleanp-of-soutcome-result-okeq

(defthm booleanp-of-soutcome-result-okeq
  (b* ((yes/no (soutcome-result-okeq x y)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: soutcome-result-okeq-is-an-equivalence

(defthm soutcome-result-okeq-is-an-equivalence
  (and (booleanp (soutcome-result-okeq x y))
       (soutcome-result-okeq x x)
       (implies (soutcome-result-okeq x y)
                (soutcome-result-okeq y x))
       (implies (and (soutcome-result-okeq x y)
                     (soutcome-result-okeq y z))
                (soutcome-result-okeq x z)))
  :rule-classes (:equivalence))

Theorem: soutcome-result-okeq-of-soutcome-result-fix-x

(defthm soutcome-result-okeq-of-soutcome-result-fix-x
  (equal (soutcome-result-okeq (soutcome-result-fix x)
                               y)
         (soutcome-result-okeq x y)))

Theorem: soutcome-result-okeq-soutcome-result-equiv-congruence-on-x

(defthm soutcome-result-okeq-soutcome-result-equiv-congruence-on-x
  (implies (soutcome-result-equiv x x-equiv)
           (equal (soutcome-result-okeq x y)
                  (soutcome-result-okeq x-equiv y)))
  :rule-classes :congruence)

Theorem: soutcome-result-okeq-of-soutcome-result-fix-y

(defthm soutcome-result-okeq-of-soutcome-result-fix-y
  (equal (soutcome-result-okeq x (soutcome-result-fix y))
         (soutcome-result-okeq x y)))

Theorem: soutcome-result-okeq-soutcome-result-equiv-congruence-on-y

(defthm soutcome-result-okeq-soutcome-result-equiv-congruence-on-y
  (implies (soutcome-result-equiv y y-equiv)
           (equal (soutcome-result-okeq x y)
                  (soutcome-result-okeq x y-equiv)))
  :rule-classes :congruence)