		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svjumpstate-pop-scope

Signature
(svjumpstate-pop-scope x) → new-x
Arguments: x — Guard (svjumpstate-p x).
Returns: new-x — Type (svjumpstate-p new-x).

Definitions and Theorems

Function: svjumpstate-pop-scope

(defun svjumpstate-pop-scope (x)
 (declare (xargs :guard (svjumpstate-p x)))
 (let ((__function__ 'svjumpstate-pop-scope))
  (declare (ignorable __function__))
  (b* (((svjumpstate x)))
    (change-svjumpstate x
                        :breakst (svstate-pop-scope x.breakst)
                        :continuest (svstate-pop-scope x.continuest)
                        :returnst (svstate-pop-scope x.returnst)))))

Theorem: svjumpstate-p-of-svjumpstate-pop-scope

(defthm svjumpstate-p-of-svjumpstate-pop-scope
  (b* ((new-x (svjumpstate-pop-scope x)))
    (svjumpstate-p new-x))
  :rule-classes :rewrite)

Theorem: svjumpstate-vars-of-pop-scope

(defthm svjumpstate-vars-of-pop-scope
  (b* ((?new-x (svjumpstate-pop-scope x)))
    (implies (not (member v (svjumpstate-vars x)))
             (not (member v (svjumpstate-vars new-x))))))

Theorem: svjumpstate-pop-scope-compatible-with-svstate-pop-scope

(defthm svjumpstate-pop-scope-compatible-with-svstate-pop-scope
  (b* nil
    (implies
         (svjumpstate-svstate-compatible jst st)
         (svjumpstate-svstate-compatible (svjumpstate-pop-scope jst)
                                         (svstate-pop-scope st)))))

Theorem: svjumpstate-pop-scope-compatible-with-svstate-pop-scope-free

(defthm svjumpstate-pop-scope-compatible-with-svstate-pop-scope-free
 (b* nil
  (implies
    (svjumpstate-svstate-compatible jst st)
    (equal
         (svjumpstate-svstate-compatible (svjumpstate-pop-scope jst)
                                         st1)
         (svstates-compatible (svstate-pop-scope st)
                              st1)))))

Theorem: svjumpstates-compatible-implies-svjumpstates-compatible-svjumpstate-pop-scope-1

(defthm
 svjumpstates-compatible-implies-svjumpstates-compatible-svjumpstate-pop-scope-1
 (implies
      (svjumpstates-compatible jst jst-equiv)
      (svjumpstates-compatible (svjumpstate-pop-scope jst)
                               (svjumpstate-pop-scope jst-equiv)))
 :rule-classes (:congruence))

Theorem: svjumpstate-pop-scope-of-svjumpstate-fix-x

(defthm svjumpstate-pop-scope-of-svjumpstate-fix-x
  (equal (svjumpstate-pop-scope (svjumpstate-fix x))
         (svjumpstate-pop-scope x)))

Theorem: svjumpstate-pop-scope-svjumpstate-equiv-congruence-on-x

(defthm svjumpstate-pop-scope-svjumpstate-equiv-congruence-on-x
  (implies (svjumpstate-equiv x x-equiv)
           (equal (svjumpstate-pop-scope x)
                  (svjumpstate-pop-scope x-equiv)))
  :rule-classes :congruence)