		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svjumpstates-compatible

Signature
(svjumpstates-compatible x y) → *
Arguments: x — Guard (svjumpstate-p x).; y — Guard (svjumpstate-p y).

Definitions and Theorems

Function: svjumpstates-compatible

(defun svjumpstates-compatible (x y)
  (declare (xargs :guard (and (svjumpstate-p x)
                              (svjumpstate-p y))))
  (let ((__function__ 'svjumpstates-compatible))
    (declare (ignorable __function__))
    (b* (((svjumpstate x)) ((svjumpstate y)))
      (and (svstates-compatible x.breakst y.breakst)
           (svstates-compatible x.continuest y.continuest)
           (svstates-compatible x.returnst y.returnst)))))

Theorem: svjumpstates-compatible-is-an-equivalence

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

Theorem: svjumpstates-compatible-implies-svstates-compatible-svjumpstate->breakst-1

(defthm
 svjumpstates-compatible-implies-svstates-compatible-svjumpstate->breakst-1
 (implies (svjumpstates-compatible x x-equiv)
          (svstates-compatible (svjumpstate->breakst x)
                               (svjumpstate->breakst x-equiv)))
 :rule-classes (:congruence))

Theorem: svstates-compatible-implies-svjumpstates-compatible-svjumpstate-2

(defthm
  svstates-compatible-implies-svjumpstates-compatible-svjumpstate-2
  (implies (svstates-compatible breakcond breakcond-equiv)
           (svjumpstates-compatible
                (svjumpstate constraints
                             breakcond breakst continuecond
                             continuest returncond returnst)
                (svjumpstate constraints
                             breakcond-equiv breakst continuecond
                             continuest returncond returnst)))
  :rule-classes (:congruence))

Theorem: svjumpstates-compatible-implies-svstates-compatible-svjumpstate->continuest-1

(defthm
 svjumpstates-compatible-implies-svstates-compatible-svjumpstate->continuest-1
 (implies (svjumpstates-compatible x x-equiv)
          (svstates-compatible (svjumpstate->continuest x)
                               (svjumpstate->continuest x-equiv)))
 :rule-classes (:congruence))

Theorem: svstates-compatible-implies-svjumpstates-compatible-svjumpstate-4

(defthm
  svstates-compatible-implies-svjumpstates-compatible-svjumpstate-4
  (implies (svstates-compatible continuecond continuecond-equiv)
           (svjumpstates-compatible
                (svjumpstate constraints
                             breakcond breakst continuecond
                             continuest returncond returnst)
                (svjumpstate constraints
                             breakcond breakst continuecond-equiv
                             continuest returncond returnst)))
  :rule-classes (:congruence))

Theorem: svjumpstates-compatible-implies-svstates-compatible-svjumpstate->returnst-1

(defthm
 svjumpstates-compatible-implies-svstates-compatible-svjumpstate->returnst-1
 (implies (svjumpstates-compatible x x-equiv)
          (svstates-compatible (svjumpstate->returnst x)
                               (svjumpstate->returnst x-equiv)))
 :rule-classes (:congruence))

Theorem: svstates-compatible-implies-svjumpstates-compatible-svjumpstate-6

(defthm
  svstates-compatible-implies-svjumpstates-compatible-svjumpstate-6
  (implies (svstates-compatible returncond returncond-equiv)
           (svjumpstates-compatible
                (svjumpstate constraints
                             breakcond breakst continuecond
                             continuest returncond returnst)
                (svjumpstate constraints
                             breakcond breakst continuecond
                             continuest returncond-equiv returnst)))
  :rule-classes (:congruence))

Theorem: svjumpstates-compatible-of-svjumpstate-fix-x

(defthm svjumpstates-compatible-of-svjumpstate-fix-x
  (equal (svjumpstates-compatible (svjumpstate-fix x)
                                  y)
         (svjumpstates-compatible x y)))

Theorem: svjumpstates-compatible-svjumpstate-equiv-congruence-on-x

(defthm svjumpstates-compatible-svjumpstate-equiv-congruence-on-x
  (implies (svjumpstate-equiv x x-equiv)
           (equal (svjumpstates-compatible x y)
                  (svjumpstates-compatible x-equiv y)))
  :rule-classes :congruence)

Theorem: svjumpstates-compatible-of-svjumpstate-fix-y

(defthm svjumpstates-compatible-of-svjumpstate-fix-y
  (equal (svjumpstates-compatible x (svjumpstate-fix y))
         (svjumpstates-compatible x y)))

Theorem: svjumpstates-compatible-svjumpstate-equiv-congruence-on-y

(defthm svjumpstates-compatible-svjumpstate-equiv-congruence-on-y
  (implies (svjumpstate-equiv y y-equiv)
           (equal (svjumpstates-compatible x y)
                  (svjumpstates-compatible x y-equiv)))
  :rule-classes :congruence)