		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svjumpstate-sequence-svstates

Signature
(svjumpstate-sequence-svstates cond1 cond2 st1 st2) → seq
Arguments: cond1 — Guard (svex-p cond1).; cond2 — Guard (svex-p cond2).; st1 — Guard (svstate-p st1).; st2 — Guard (svstate-p st2).
Returns: seq — Type (svstate-p seq).

Definitions and Theorems

Function: svjumpstate-sequence-svstates

(defun svjumpstate-sequence-svstates (cond1 cond2 st1 st2)
  (declare (xargs :guard (and (svex-p cond1)
                              (svex-p cond2)
                              (svstate-p st1)
                              (svstate-p st2))))
  (let ((__function__ 'svjumpstate-sequence-svstates))
    (declare (ignorable __function__))
    (b* ((cond1 (svex-fix cond1))
         (cond2 (svex-fix cond2))
         (st1 (svstate-fix st1))
         (st2 (svstate-fix st2))
         ((when (eql 0 cond1)) st2)
         ((when (eql 0 cond2)) st1))
      (svstate-merge-branches cond1 st1 st2))))

Theorem: svstate-p-of-svjumpstate-sequence-svstates

(defthm svstate-p-of-svjumpstate-sequence-svstates
  (b* ((seq (svjumpstate-sequence-svstates cond1 cond2 st1 st2)))
    (svstate-p seq))
  :rule-classes :rewrite)

Theorem: vars-of-svjumpstate-sequence-svstates

(defthm vars-of-svjumpstate-sequence-svstates
 (b*
  ((acl2::?seq (svjumpstate-sequence-svstates cond1 cond2 st1 st2)))
  (implies (and (not (member v (svstate-vars st1)))
                (not (member v (svstate-vars st2)))
                (not (member v (svex-vars cond1)))
                (svstates-compatible st1 st2))
           (not (member v (svstate-vars seq))))))

Theorem: svstates-compatible-of-svjumpstate-sequence-svstates

(defthm svstates-compatible-of-svjumpstate-sequence-svstates
 (b*
  ((acl2::?seq (svjumpstate-sequence-svstates cond1 cond2 st1 st2)))
  (implies (svstates-compatible st1 st2)
           (svstates-compatible seq st1))))

Theorem: svjumpstate-sequence-svstates-of-svex-fix-cond1

(defthm svjumpstate-sequence-svstates-of-svex-fix-cond1
  (equal (svjumpstate-sequence-svstates (svex-fix cond1)
                                        cond2 st1 st2)
         (svjumpstate-sequence-svstates cond1 cond2 st1 st2)))

Theorem: svjumpstate-sequence-svstates-svex-equiv-congruence-on-cond1

(defthm svjumpstate-sequence-svstates-svex-equiv-congruence-on-cond1
 (implies
  (svex-equiv cond1 cond1-equiv)
  (equal (svjumpstate-sequence-svstates cond1 cond2 st1 st2)
         (svjumpstate-sequence-svstates cond1-equiv cond2 st1 st2)))
 :rule-classes :congruence)

Theorem: svjumpstate-sequence-svstates-of-svex-fix-cond2

(defthm svjumpstate-sequence-svstates-of-svex-fix-cond2
  (equal (svjumpstate-sequence-svstates cond1 (svex-fix cond2)
                                        st1 st2)
         (svjumpstate-sequence-svstates cond1 cond2 st1 st2)))

Theorem: svjumpstate-sequence-svstates-svex-equiv-congruence-on-cond2

(defthm svjumpstate-sequence-svstates-svex-equiv-congruence-on-cond2
 (implies
  (svex-equiv cond2 cond2-equiv)
  (equal (svjumpstate-sequence-svstates cond1 cond2 st1 st2)
         (svjumpstate-sequence-svstates cond1 cond2-equiv st1 st2)))
 :rule-classes :congruence)

Theorem: svjumpstate-sequence-svstates-of-svstate-fix-st1

(defthm svjumpstate-sequence-svstates-of-svstate-fix-st1
 (equal (svjumpstate-sequence-svstates cond1 cond2 (svstate-fix st1)
                                       st2)
        (svjumpstate-sequence-svstates cond1 cond2 st1 st2)))

Theorem: svjumpstate-sequence-svstates-svstate-equiv-congruence-on-st1

(defthm
      svjumpstate-sequence-svstates-svstate-equiv-congruence-on-st1
 (implies
  (svstate-equiv st1 st1-equiv)
  (equal (svjumpstate-sequence-svstates cond1 cond2 st1 st2)
         (svjumpstate-sequence-svstates cond1 cond2 st1-equiv st2)))
 :rule-classes :congruence)

Theorem: svjumpstate-sequence-svstates-of-svstate-fix-st2

(defthm svjumpstate-sequence-svstates-of-svstate-fix-st2
 (equal
   (svjumpstate-sequence-svstates cond1 cond2 st1 (svstate-fix st2))
   (svjumpstate-sequence-svstates cond1 cond2 st1 st2)))

Theorem: svjumpstate-sequence-svstates-svstate-equiv-congruence-on-st2

(defthm
      svjumpstate-sequence-svstates-svstate-equiv-congruence-on-st2
 (implies
  (svstate-equiv st2 st2-equiv)
  (equal (svjumpstate-sequence-svstates cond1 cond2 st1 st2)
         (svjumpstate-sequence-svstates cond1 cond2 st1 st2-equiv)))
 :rule-classes :congruence)