		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svjumpstate-levels

Signature
(svjumpstate-levels x) → levels
Arguments: x — Guard (svjumpstate-p x).
Returns: levels — Type (posp levels).

Definitions and Theorems

Function: svjumpstate-levels

(defun svjumpstate-levels (x)
  (declare (xargs :guard (svjumpstate-p x)))
  (let ((__function__ 'svjumpstate-levels))
    (declare (ignorable __function__))
    (b* (((svjumpstate x))
         ((svstate x.breakst))
         ((svstate x.continuest))
         ((svstate x.returnst)))
      (min (len x.breakst.blkst)
           (min (len x.continuest.blkst)
                (len x.returnst.blkst))))))

Theorem: posp-of-svjumpstate-levels

(defthm posp-of-svjumpstate-levels
  (b* ((levels (svjumpstate-levels x)))
    (posp levels))
  :rule-classes :type-prescription)

Theorem: svjumpstate-levels-of-svjumpstate-fix-x

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

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

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