		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svjumpstate-vars

Signature
(svjumpstate-vars x) → vars
Arguments: x — Guard (svjumpstate-p x).
Returns: vars — Type (and (svarlist-p vars) (setp vars)).

Definitions and Theorems

Function: svjumpstate-vars

(defun svjumpstate-vars (x)
 (declare (xargs :guard (svjumpstate-p x)))
 (let ((__function__ 'svjumpstate-vars))
  (declare (ignorable __function__))
  (b* (((svjumpstate x)))
   (union
    (union (svex-vars x.breakcond)
           (svstate-vars x.breakst))
    (union
     (union (svex-vars x.continuecond)
            (svstate-vars x.continuest))
     (union
       (svex-vars x.returncond)
       (union (svstate-vars x.returnst)
              (mergesort (constraintlist-vars x.constraints)))))))))

Theorem: return-type-of-svjumpstate-vars

(defthm return-type-of-svjumpstate-vars
  (b* ((vars (svjumpstate-vars x)))
    (and (svarlist-p vars) (setp vars)))
  :rule-classes :rewrite)

Theorem: svjumpstate-vars-of-svjumpstate

(defthm svjumpstate-vars-of-svjumpstate
 (equal
  (svjumpstate-vars (svjumpstate constraints
                                 breakcond breakst continuecond
                                 continuest returncond returnst))
  (union
   (union (svex-vars breakcond)
          (svstate-vars breakst))
   (union
     (union (svex-vars continuecond)
            (svstate-vars continuest))
     (union
          (svex-vars returncond)
          (union (svstate-vars returnst)
                 (mergesort (constraintlist-vars constraints))))))))

Theorem: vars-of-accessors-of-svjumpstate-vars

(defthm vars-of-accessors-of-svjumpstate-vars
 (b* ((?vars (svjumpstate-vars x)))
  (implies
      (not (member v vars))
      (b* (((svjumpstate x)))
        (and (not (member v (svex-vars x.breakcond)))
             (not (member v (svstate-vars x.breakst)))
             (not (member v (svex-vars x.continuecond)))
             (not (member v (svstate-vars x.continuest)))
             (not (member v (svex-vars x.returncond)))
             (not (member v (svstate-vars x.returnst)))
             (not (member v
                          (constraintlist-vars x.constraints))))))))

Theorem: svjumpstate-vars-of-svjumpstate-fix-x

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

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

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