		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svjumpstate-fork

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

Definitions and Theorems

Function: svjumpstate-fork

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

Theorem: svjumpstate-p-of-svjumpstate-fork

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

Theorem: svjumpstate-fork-preserves-compatible

(defthm svjumpstate-fork-preserves-compatible
  (b* ((?new-x (svjumpstate-fork x)))
    (svjumpstates-compatible new-x (double-rewrite x))))

Theorem: svjumpstate-fork-of-svjumpstate-fix-x

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

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

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