		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Make-empty-svjumpstate

Signature
(make-empty-svjumpstate st &key (constraints 'nil)) → jst
Arguments: st — Guard (svstate-p st).; constraints — Guard (constraintlist-p constraints).
Returns: jst — Type (svjumpstate-p jst).

Definitions and Theorems

Function: make-empty-svjumpstate-fn

(defun make-empty-svjumpstate-fn (st constraints)
  (declare (xargs :guard (and (svstate-p st)
                              (constraintlist-p constraints))))
  (let ((__function__ 'make-empty-svjumpstate))
    (declare (ignorable __function__))
    (make-svjumpstate :constraints constraints
                      :breakcond 0
                      :breakst st
                      :continuecond 0
                      :continuest st
                      :returncond 0
                      :returnst st)))

Theorem: svjumpstate-p-of-make-empty-svjumpstate

(defthm svjumpstate-p-of-make-empty-svjumpstate
  (b* ((jst (make-empty-svjumpstate-fn st constraints)))
    (svjumpstate-p jst))
  :rule-classes :rewrite)

Theorem: vars-of-make-empty-svjumpstate

(defthm vars-of-make-empty-svjumpstate
 (b* ((?jst (make-empty-svjumpstate-fn st constraints)))
   (implies (and (not (member v (svstate-vars st)))
                 (not (member v (constraintlist-vars constraints))))
            (not (member v (svjumpstate-vars jst))))))

Theorem: accs-of-make-empty-svjumpstate

(defthm accs-of-make-empty-svjumpstate
  (b* ((?jst (make-empty-svjumpstate-fn st constraints)))
    (b* (((svjumpstate jst)))
      (and (equal jst.constraints
                  (constraintlist-fix constraints))
           (equal jst.breakcond 0)
           (equal jst.breakst (svstate-fix st))
           (equal jst.continuecond 0)
           (equal jst.continuest (svstate-fix st))
           (equal jst.returncond 0)
           (equal jst.returnst (svstate-fix st))))))

Theorem: make-empty-svjumpstate-fn-of-svstate-fix-st

(defthm make-empty-svjumpstate-fn-of-svstate-fix-st
  (equal (make-empty-svjumpstate-fn (svstate-fix st)
                                    constraints)
         (make-empty-svjumpstate-fn st constraints)))

Theorem: make-empty-svjumpstate-fn-svstate-equiv-congruence-on-st

(defthm make-empty-svjumpstate-fn-svstate-equiv-congruence-on-st
  (implies (svstate-equiv st st-equiv)
           (equal (make-empty-svjumpstate-fn st constraints)
                  (make-empty-svjumpstate-fn st-equiv constraints)))
  :rule-classes :congruence)

Theorem: make-empty-svjumpstate-fn-of-constraintlist-fix-constraints

(defthm make-empty-svjumpstate-fn-of-constraintlist-fix-constraints
 (equal
     (make-empty-svjumpstate-fn st (constraintlist-fix constraints))
     (make-empty-svjumpstate-fn st constraints)))

Theorem: make-empty-svjumpstate-fn-constraintlist-equiv-congruence-on-constraints

(defthm
 make-empty-svjumpstate-fn-constraintlist-equiv-congruence-on-constraints
 (implies (constraintlist-equiv constraints constraints-equiv)
          (equal (make-empty-svjumpstate-fn st constraints)
                 (make-empty-svjumpstate-fn st constraints-equiv)))
 :rule-classes :congruence)