		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svjumpstate-sequence

Signature
(svjumpstate-sequence jst1 jst2) → seq
Arguments: jst1 — Guard (svjumpstate-p jst1).; jst2 — Guard (svjumpstate-p jst2).
Returns: seq — Type (svjumpstate-p seq).

Definitions and Theorems

Function: svjumpstate-sequence

(defun svjumpstate-sequence (jst1 jst2)
 (declare (xargs :guard (and (svjumpstate-p jst1)
                             (svjumpstate-p jst2))))
 (let ((__function__ 'svjumpstate-sequence))
  (declare (ignorable __function__))
  (b*
   (((svjumpstate jst1))
    ((svjumpstate jst2))
    (jst1.anyjump
         (svex-svstmt-or
              jst1.breakcond
              (svex-svstmt-or jst1.continuecond jst1.returncond))))
   (make-svjumpstate
    :constraints
    (append-without-guard jst1.constraints jst2.constraints)
    :breakcond
    (svex-svstmt-or jst1.breakcond
                    (svex-svstmt-andc1 jst1.anyjump jst2.breakcond))
    :breakst
    (svjumpstate-sequence-svstates jst1.breakcond jst2.breakcond
                                   jst1.breakst jst2.breakst)
    :continuecond
    (svex-svstmt-or
         jst1.continuecond
         (svex-svstmt-andc1 jst1.anyjump jst2.continuecond))
    :continuest (svjumpstate-sequence-svstates
                     jst1.continuecond jst2.continuecond
                     jst1.continuest jst2.continuest)
    :returncond
    (svex-svstmt-or
         jst1.returncond
         (svex-svstmt-andc1 jst1.anyjump jst2.returncond))
    :returnst
    (svjumpstate-sequence-svstates jst1.returncond jst2.returncond
                                   jst1.returnst jst2.returnst)))))

Theorem: svjumpstate-p-of-svjumpstate-sequence

(defthm svjumpstate-p-of-svjumpstate-sequence
  (b* ((seq (svjumpstate-sequence jst1 jst2)))
    (svjumpstate-p seq))
  :rule-classes :rewrite)

Theorem: vars-of-svjumpstate-sequence

(defthm vars-of-svjumpstate-sequence
  (b* ((acl2::?seq (svjumpstate-sequence jst1 jst2)))
    (implies
         (and (not (member v (svjumpstate-vars jst1)))
              (not (member v (svjumpstate-vars jst2)))
              (double-rewrite (svjumpstates-compatible jst1 jst2)))
         (not (member v (svjumpstate-vars seq))))))

Theorem: svjumpstates-compatible-of-svjumpstate-sequence

(defthm svjumpstates-compatible-of-svjumpstate-sequence
  (b* ((acl2::?seq (svjumpstate-sequence jst1 jst2)))
    (implies (double-rewrite (svjumpstates-compatible jst1 jst2))
             (svjumpstates-compatible seq (double-rewrite jst1)))))

Theorem: svstates-compatible-of-svjumpstate-sequence

(defthm svstates-compatible-of-svjumpstate-sequence
 (b* ((acl2::?seq (svjumpstate-sequence jst1 jst2)))
   (implies
        (double-rewrite (svjumpstates-compatible jst1 jst2))
        (b* (((svjumpstate seq))
             ((svjumpstate jst1)
              (double-rewrite jst1)))
          (and (svstates-compatible seq.breakst jst1.breakst)
               (svstates-compatible seq.continuest jst1.continuest)
               (svstates-compatible seq.returnst jst1.returnst))))))

Theorem: svjumpstate-sequence-of-svjumpstate-fix-jst1

(defthm svjumpstate-sequence-of-svjumpstate-fix-jst1
  (equal (svjumpstate-sequence (svjumpstate-fix jst1)
                               jst2)
         (svjumpstate-sequence jst1 jst2)))

Theorem: svjumpstate-sequence-svjumpstate-equiv-congruence-on-jst1

(defthm svjumpstate-sequence-svjumpstate-equiv-congruence-on-jst1
  (implies (svjumpstate-equiv jst1 jst1-equiv)
           (equal (svjumpstate-sequence jst1 jst2)
                  (svjumpstate-sequence jst1-equiv jst2)))
  :rule-classes :congruence)

Theorem: svjumpstate-sequence-of-svjumpstate-fix-jst2

(defthm svjumpstate-sequence-of-svjumpstate-fix-jst2
  (equal (svjumpstate-sequence jst1 (svjumpstate-fix jst2))
         (svjumpstate-sequence jst1 jst2)))

Theorem: svjumpstate-sequence-svjumpstate-equiv-congruence-on-jst2

(defthm svjumpstate-sequence-svjumpstate-equiv-congruence-on-jst2
  (implies (svjumpstate-equiv jst2 jst2-equiv)
           (equal (svjumpstate-sequence jst1 jst2)
                  (svjumpstate-sequence jst1 jst2-equiv)))
  :rule-classes :congruence)