		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Constraintlist-merge-branches

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

Definitions and Theorems

Function: constraintlist-merge-branches

(defun constraintlist-merge-branches
       (cond then-constraints else-constraints)
  (declare (xargs :guard (and (svex-p cond)
                              (constraintlist-p then-constraints)
                              (constraintlist-p else-constraints))))
  (let ((__function__ 'constraintlist-merge-branches))
    (declare (ignorable __function__))
    (append (constraintlist-add-pathcond cond nil then-constraints)
            (constraintlist-add-pathcond cond t else-constraints))))

Theorem: constraintlist-p-of-constraintlist-merge-branches

(defthm constraintlist-p-of-constraintlist-merge-branches
  (b* ((new-constraints (constraintlist-merge-branches
                             cond
                             then-constraints else-constraints)))
    (constraintlist-p new-constraints))
  :rule-classes :rewrite)

Theorem: vars-of-constraintlist-merge-branches

(defthm vars-of-constraintlist-merge-branches
  (b* ((?new-constraints (constraintlist-merge-branches
                              cond
                              then-constraints else-constraints)))
    (implies
         (and (not (member v
                           (constraintlist-vars then-constraints)))
              (not (member v
                           (constraintlist-vars else-constraints)))
              (not (member v (svex-vars cond))))
         (not (member v
                      (constraintlist-vars new-constraints))))))

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

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

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

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

Theorem: constraintlist-merge-branches-of-constraintlist-fix-then-constraints

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

Theorem: constraintlist-merge-branches-constraintlist-equiv-congruence-on-then-constraints

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

Theorem: constraintlist-merge-branches-of-constraintlist-fix-else-constraints

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

Theorem: constraintlist-merge-branches-constraintlist-equiv-congruence-on-else-constraints

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