		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svjumpstate-svstate-compatible

Signature
(svjumpstate-svstate-compatible jst st) → *
Arguments: jst — Guard (svjumpstate-p jst).; st — Guard (svstate-p st).

Definitions and Theorems

Function: svjumpstate-svstate-compatible

(defun svjumpstate-svstate-compatible (jst st)
  (declare (xargs :guard (and (svjumpstate-p jst)
                              (svstate-p st))))
  (let ((__function__ 'svjumpstate-svstate-compatible))
    (declare (ignorable __function__))
    (b* (((svjumpstate jst)))
      (and (svstates-compatible jst.breakst st)
           (svstates-compatible jst.continuest st)
           (svstates-compatible jst.returnst st)))))

Theorem: svjumpstates-compatible-implies-equal-svjumpstate-svstate-compatible-1

(defthm
 svjumpstates-compatible-implies-equal-svjumpstate-svstate-compatible-1
 (implies (svjumpstates-compatible jst jst-equiv)
          (equal (svjumpstate-svstate-compatible jst st)
                 (svjumpstate-svstate-compatible jst-equiv st)))
 :rule-classes (:congruence))

Theorem: svstates-compatible-implies-equal-svjumpstate-svstate-compatible-2

(defthm
 svstates-compatible-implies-equal-svjumpstate-svstate-compatible-2
 (implies (svstates-compatible st st-equiv)
          (equal (svjumpstate-svstate-compatible jst st)
                 (svjumpstate-svstate-compatible jst st-equiv)))
 :rule-classes (:congruence))

Theorem: svjumpstate-svstate-compatible-of-make-empty

(defthm svjumpstate-svstate-compatible-of-make-empty
  (svjumpstate-svstate-compatible (make-empty-svjumpstate st)
                                  st))

Theorem: svjumpstates-compatible-rewrite-to-svjumpstate-svstate-compatible

(defthm
  svjumpstates-compatible-rewrite-to-svjumpstate-svstate-compatible
  (implies (svjumpstate-svstate-compatible jst1 st)
           (equal (svjumpstates-compatible jst1 jst2)
                  (svjumpstate-svstate-compatible jst2 st))))

Theorem: svjumpstates-compatible-rewrite-to-svjumpstate-svstate-compatible-1

(defthm
 svjumpstates-compatible-rewrite-to-svjumpstate-svstate-compatible-1
 (implies (svjumpstate-svstate-compatible jst2 st)
          (equal (svjumpstates-compatible jst1 jst2)
                 (svjumpstate-svstate-compatible jst1 st))))

Theorem: svjumpstate-svstate-compatible-implies-rewrite-accs

(defthm svjumpstate-svstate-compatible-implies-rewrite-accs
  (implies (svjumpstate-svstate-compatible jst st)
           (and (svstates-compatible (svjumpstate->breakst jst)
                                     st)
                (svstates-compatible (svjumpstate->continuest jst)
                                     st)
                (svstates-compatible (svjumpstate->returnst jst)
                                     st))))

Theorem: svjumpstates-compatible-of-svjumpstate

(defthm svjumpstates-compatible-of-svjumpstate
 (implies
      (and (svjumpstate-svstate-compatible jst breakst)
           (svjumpstate-svstate-compatible jst continuest)
           (svjumpstate-svstate-compatible jst returnst))
      (and (equal (svjumpstates-compatible
                       (svjumpstate constraints
                                    breakcond breakst continuecond
                                    continuest returncond returnst)
                       jst)
                  t)
           (equal (svjumpstates-compatible
                       jst
                       (svjumpstate constraints
                                    breakcond breakst continuecond
                                    continuest returncond returnst))
                  t))))

Theorem: svjumpstates-compatible-of-change

(defthm svjumpstates-compatible-of-change
  (svjumpstates-compatible
       (change-svjumpstate jst
                           :constraints constraints
                           :breakcond breakcond
                           :continuecond continuecond
                           :returncond returncond)
       (double-rewrite jst)))

Theorem: svjumpstates-compatible-of-make-empty-svjumpstate

(defthm svjumpstates-compatible-of-make-empty-svjumpstate
 (and
  (equal (svjumpstates-compatible (make-empty-svjumpstate st)
                                  jst)
         (svjumpstate-svstate-compatible jst (double-rewrite st)))
  (equal (svjumpstates-compatible jst (make-empty-svjumpstate st))
         (svjumpstate-svstate-compatible jst (double-rewrite st)))))

Theorem: svjumpstates-svstate-compatible-of-svjumpstate

(defthm svjumpstates-svstate-compatible-of-svjumpstate
  (equal (svjumpstate-svstate-compatible
              (svjumpstate constraints
                           breakcond breakst continuecond
                           continuest returncond returnst)
              st)
         (and (svstates-compatible st breakst)
              (svstates-compatible st continuest)
              (svstates-compatible st returnst))))

Theorem: svjumpstate-svstate-compatible-of-make-empty-svjumpstate

(defthm svjumpstate-svstate-compatible-of-make-empty-svjumpstate
 (equal (svjumpstate-svstate-compatible (make-empty-svjumpstate st1)
                                        st2)
        (svstates-compatible (double-rewrite st1)
                             st2)))

Theorem: svjumpstate-svstate-compatible-of-svjumpstate-fix-jst

(defthm svjumpstate-svstate-compatible-of-svjumpstate-fix-jst
  (equal (svjumpstate-svstate-compatible (svjumpstate-fix jst)
                                         st)
         (svjumpstate-svstate-compatible jst st)))

Theorem: svjumpstate-svstate-compatible-svjumpstate-equiv-congruence-on-jst

(defthm
 svjumpstate-svstate-compatible-svjumpstate-equiv-congruence-on-jst
 (implies (svjumpstate-equiv jst jst-equiv)
          (equal (svjumpstate-svstate-compatible jst st)
                 (svjumpstate-svstate-compatible jst-equiv st)))
 :rule-classes :congruence)

Theorem: svjumpstate-svstate-compatible-of-svstate-fix-st

(defthm svjumpstate-svstate-compatible-of-svstate-fix-st
  (equal (svjumpstate-svstate-compatible jst (svstate-fix st))
         (svjumpstate-svstate-compatible jst st)))

Theorem: svjumpstate-svstate-compatible-svstate-equiv-congruence-on-st

(defthm
      svjumpstate-svstate-compatible-svstate-equiv-congruence-on-st
  (implies (svstate-equiv st st-equiv)
           (equal (svjumpstate-svstate-compatible jst st)
                  (svjumpstate-svstate-compatible jst st-equiv)))
  :rule-classes :congruence)