		Search-engine friendly clone of the ACL2 documentation.

Svex-composition

Svex-assigns-compose1

Given an alist mapping variables to assigned expressions, compose them together into full update functions.

Signature
(svex-assigns-compose1 x &key (rewrite 't) (scc-selfcompose-limit 'nil)) → (mv err xx)
Arguments: x — Guard (svex-alist-p x).; scc-selfcompose-limit — Guard (maybe-natp scc-selfcompose-limit).
Returns: xx — Type (svex-alist-p xx).

Definitions and Theorems

Function: svex-assigns-compose1-fn

(defun svex-assigns-compose1-fn (x rewrite scc-selfcompose-limit)
 (declare (xargs :guard (and (svex-alist-p x)
                             (maybe-natp scc-selfcompose-limit))))
 (let ((__function__ 'svex-assigns-compose1))
   (declare (ignorable __function__))
   (b* ((phase1 (svex-assigns-compose-phase1 x))
        ((mv masks phase2)
         (svex-assigns-compose-phase2
              phase1
              :simpconf (mbe :logic (if* rewrite 20 t)
                             :exec (if rewrite 20 t))))
        ((mv err phase3 splittab)
         (svex-assigns-compose-phase3 phase2 masks))
        ((when err) (mv err nil))
        ((unless splittab) (mv nil phase2))
        ((mv err phase4)
         (svex-assigns-compose-phase4 phase3 scc-selfcompose-limit))
        ((when err) (mv err nil)))
     (mv nil
         (svex-assigns-compose-phase5 phase2 phase4 splittab)))))

Theorem: svex-alist-p-of-svex-assigns-compose1.xx

(defthm svex-alist-p-of-svex-assigns-compose1.xx
  (b* (((mv ?err ?xx)
        (svex-assigns-compose1-fn x rewrite scc-selfcompose-limit)))
    (svex-alist-p xx))
  :rule-classes :rewrite)

Theorem: netcomp-p-of-svex-assigns-compose1

(defthm netcomp-p-of-svex-assigns-compose1
  (b* (((mv ?err ?xx)
        (svex-assigns-compose1-fn x rewrite scc-selfcompose-limit)))
    (netcomp-p xx x)))

Theorem: netcomp-p-of-svex-assigns-compose1-trans

(defthm netcomp-p-of-svex-assigns-compose1-trans
  (b* (((mv ?err ?xx)
        (svex-assigns-compose1-fn x rewrite scc-selfcompose-limit)))
    (implies (netcomp-p x y)
             (netcomp-p xx y))))

Theorem: svex-alist-keys-of-svex-assigns-compose1

(defthm svex-alist-keys-of-svex-assigns-compose1
  (b* (((mv ?err ?xx)
        (svex-assigns-compose1-fn x rewrite scc-selfcompose-limit)))
    (implies (not err)
             (set-equiv (svex-alist-keys xx)
                        (svex-alist-keys x)))))

Theorem: svex-assigns-compose1-fn-of-svex-alist-fix-x

(defthm svex-assigns-compose1-fn-of-svex-alist-fix-x
 (equal (svex-assigns-compose1-fn (svex-alist-fix x)
                                  rewrite scc-selfcompose-limit)
        (svex-assigns-compose1-fn x rewrite scc-selfcompose-limit)))

Theorem: svex-assigns-compose1-fn-svex-alist-equiv-congruence-on-x

(defthm svex-assigns-compose1-fn-svex-alist-equiv-congruence-on-x
 (implies
   (svex-alist-equiv x x-equiv)
   (equal (svex-assigns-compose1-fn x rewrite scc-selfcompose-limit)
          (svex-assigns-compose1-fn
               x-equiv rewrite scc-selfcompose-limit)))
 :rule-classes :congruence)

Theorem: svex-assigns-compose1-fn-of-maybe-natp-fix-scc-selfcompose-limit

(defthm
   svex-assigns-compose1-fn-of-maybe-natp-fix-scc-selfcompose-limit
 (equal (svex-assigns-compose1-fn
             x rewrite
             (acl2::maybe-natp-fix scc-selfcompose-limit))
        (svex-assigns-compose1-fn x rewrite scc-selfcompose-limit)))

Theorem: svex-assigns-compose1-fn-maybe-nat-equiv-congruence-on-scc-selfcompose-limit

(defthm
 svex-assigns-compose1-fn-maybe-nat-equiv-congruence-on-scc-selfcompose-limit
 (implies
   (acl2::maybe-nat-equiv scc-selfcompose-limit
                          scc-selfcompose-limit-equiv)
   (equal (svex-assigns-compose1-fn x rewrite scc-selfcompose-limit)
          (svex-assigns-compose1-fn
               x rewrite scc-selfcompose-limit-equiv)))
 :rule-classes :congruence)