		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svjumpstate-free

Signature
(svjumpstate-free x) → new-x
Arguments: x — Guard (svjumpstate-p x).
Returns: new-x — Type (equal new-x (svjumpstate-fix x)).

Definitions and Theorems

Function: svjumpstate-free

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

Theorem: return-type-of-svjumpstate-free

(defthm return-type-of-svjumpstate-free
  (b* ((new-x (svjumpstate-free x)))
    (equal new-x (svjumpstate-fix x)))
  :rule-classes :rewrite)

Theorem: svjumpstate-free-of-svjumpstate-fix-x

(defthm svjumpstate-free-of-svjumpstate-fix-x
  (equal (svjumpstate-free (svjumpstate-fix x))
         (svjumpstate-free x)))

Theorem: svjumpstate-free-svjumpstate-equiv-congruence-on-x

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