		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstate-pop-scope

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

Definitions and Theorems

Function: svstate-pop-scope

(defun svstate-pop-scope (x)
  (declare (xargs :guard (svstate-p x)))
  (let ((__function__ 'svstate-pop-scope))
    (declare (ignorable __function__))
    (b* (((svstate x)))
      (change-svstate x :blkst
                      (if (consp (cdr x.blkst))
                          (cdr x.blkst)
                        (list nil))))))

Theorem: svstate-p-of-svstate-pop-scope

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

Theorem: vars-of-svate-pop-scope

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

Theorem: svstates-compatible-of-pop-of-push

(defthm svstates-compatible-of-pop-of-push
  (svstates-compatible
       (svstate-pop-scope (svstate-push-scope x locals))
       x))

Theorem: svstates-compatible-of-pop

(defthm svstates-compatible-of-pop
  (implies (svstates-compatible x y)
           (equal (svstates-compatible (svstate-pop-scope x)
                                       (svstate-pop-scope y))
                  t)))

Theorem: svstates-compatible-implies-svstates-compatible-svstate-pop-scope-1

(defthm
 svstates-compatible-implies-svstates-compatible-svstate-pop-scope-1
 (implies (svstates-compatible x x-equiv)
          (svstates-compatible (svstate-pop-scope x)
                               (svstate-pop-scope x-equiv)))
 :rule-classes (:congruence))

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

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

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

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