		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svjumpstate-merge-branches

Signature
(svjumpstate-merge-branches cond then else) → ite
Arguments: cond — Guard (svex-p cond).; then — Guard (svjumpstate-p then).; else — Guard (svjumpstate-p else).
Returns: ite — Type (svjumpstate-p ite).

Definitions and Theorems

Function: svjumpstate-merge-branches

(defun svjumpstate-merge-branches (cond then else)
 (declare (xargs :guard (and (svex-p cond)
                             (svjumpstate-p then)
                             (svjumpstate-p else))))
 (let ((__function__ 'svjumpstate-merge-branches))
  (declare (ignorable __function__))
  (b* (((svjumpstate then))
       ((svjumpstate else)))
   (make-svjumpstate
     :constraints (constraintlist-merge-branches
                       cond then.constraints else.constraints)
     :breakcond (svex-svstmt-ite cond then.breakcond else.breakcond)
     :breakst (svjumpstate-merge-svstate-branches
                   cond then.breakcond else.breakcond
                   then.breakst else.breakst)
     :continuecond
     (svex-svstmt-ite cond
                      then.continuecond else.continuecond)
     :continuest (svjumpstate-merge-svstate-branches
                      cond then.continuecond else.continuecond
                      then.continuest else.continuest)
     :returncond
     (svex-svstmt-ite cond then.returncond else.returncond)
     :returnst (svjumpstate-merge-svstate-branches
                    cond then.returncond else.returncond
                    then.returnst else.returnst)))))

Theorem: svjumpstate-p-of-svjumpstate-merge-branches

(defthm svjumpstate-p-of-svjumpstate-merge-branches
  (b* ((ite (svjumpstate-merge-branches cond then else)))
    (svjumpstate-p ite))
  :rule-classes :rewrite)

Theorem: vars-of-svjumpstate-merge-branches

(defthm vars-of-svjumpstate-merge-branches
 (b* ((?ite (svjumpstate-merge-branches cond then else)))
  (implies (and (double-rewrite (svjumpstates-compatible then else))
                (not (member v (svex-vars cond)))
                (not (member v (svjumpstate-vars then)))
                (not (member v (svjumpstate-vars else))))
           (not (member v (svjumpstate-vars ite))))))

Theorem: svjumpstate-merge-branches-preserves-compatible

(defthm svjumpstate-merge-branches-preserves-compatible
  (b* ((?ite (svjumpstate-merge-branches cond then else)))
    (implies (double-rewrite (svjumpstates-compatible then else))
             (svjumpstates-compatible ite (double-rewrite then)))))

Theorem: svjumpstate-merge-branches-of-svex-fix-cond

(defthm svjumpstate-merge-branches-of-svex-fix-cond
  (equal (svjumpstate-merge-branches (svex-fix cond)
                                     then else)
         (svjumpstate-merge-branches cond then else)))

Theorem: svjumpstate-merge-branches-svex-equiv-congruence-on-cond

(defthm svjumpstate-merge-branches-svex-equiv-congruence-on-cond
 (implies (svex-equiv cond cond-equiv)
          (equal (svjumpstate-merge-branches cond then else)
                 (svjumpstate-merge-branches cond-equiv then else)))
 :rule-classes :congruence)

Theorem: svjumpstate-merge-branches-of-svjumpstate-fix-then

(defthm svjumpstate-merge-branches-of-svjumpstate-fix-then
  (equal (svjumpstate-merge-branches cond (svjumpstate-fix then)
                                     else)
         (svjumpstate-merge-branches cond then else)))

Theorem: svjumpstate-merge-branches-svjumpstate-equiv-congruence-on-then

(defthm
    svjumpstate-merge-branches-svjumpstate-equiv-congruence-on-then
 (implies (svjumpstate-equiv then then-equiv)
          (equal (svjumpstate-merge-branches cond then else)
                 (svjumpstate-merge-branches cond then-equiv else)))
 :rule-classes :congruence)

Theorem: svjumpstate-merge-branches-of-svjumpstate-fix-else

(defthm svjumpstate-merge-branches-of-svjumpstate-fix-else
  (equal
       (svjumpstate-merge-branches cond then (svjumpstate-fix else))
       (svjumpstate-merge-branches cond then else)))

Theorem: svjumpstate-merge-branches-svjumpstate-equiv-congruence-on-else

(defthm
    svjumpstate-merge-branches-svjumpstate-equiv-congruence-on-else
 (implies (svjumpstate-equiv else else-equiv)
          (equal (svjumpstate-merge-branches cond then else)
                 (svjumpstate-merge-branches cond then else-equiv)))
 :rule-classes :congruence)