		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svexlist-mask-alist/toposort

Signature
(svexlist-mask-alist/toposort x) → (mv mask-al toposort)
Arguments: x — Guard (svexlist-p x).
Returns: mask-al — Type (svex-mask-alist-p mask-al).; toposort — Type (and (svexlist-p toposort) (svexlist-toposort-p toposort)).

Definitions and Theorems

Function: svexlist-mask-alist/toposort

(defun svexlist-mask-alist/toposort (x)
 (declare (xargs :guard (svexlist-p x)))
 (let ((__function__ 'svexlist-mask-alist/toposort))
   (declare (ignorable __function__))
   (b*
     (((mv toposort al)
       (cwtime (svexlist-toposort x nil nil)
               :mintime 1))
      (- (fast-alist-free al))
      (mask-al (cwtime (svexlist-compute-masks
                            toposort (svexlist-mask-acons x -1 nil))
                       :mintime 1)))
     (mv mask-al toposort))))

Theorem: svex-mask-alist-p-of-svexlist-mask-alist/toposort.mask-al

(defthm svex-mask-alist-p-of-svexlist-mask-alist/toposort.mask-al
  (b* (((mv ?mask-al ?toposort)
        (svexlist-mask-alist/toposort x)))
    (svex-mask-alist-p mask-al))
  :rule-classes :rewrite)

Theorem: return-type-of-svexlist-mask-alist/toposort.toposort

(defthm return-type-of-svexlist-mask-alist/toposort.toposort
  (b* (((mv ?mask-al ?toposort)
        (svexlist-mask-alist/toposort x)))
    (and (svexlist-p toposort)
         (svexlist-toposort-p toposort)))
  :rule-classes :rewrite)

Theorem: svexlist-mask-alist/toposort-of-svexlist-fix-x

(defthm svexlist-mask-alist/toposort-of-svexlist-fix-x
  (equal (svexlist-mask-alist/toposort (svexlist-fix x))
         (svexlist-mask-alist/toposort x)))

Theorem: svexlist-mask-alist/toposort-svexlist-equiv-congruence-on-x

(defthm svexlist-mask-alist/toposort-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-mask-alist/toposort x)
                  (svexlist-mask-alist/toposort x-equiv)))
  :rule-classes :congruence)

Theorem: svexlist-mask-alist/toposort-complete

(defthm svexlist-mask-alist/toposort-complete
  (b* (((mv ?mask-al ?toposort)
        (svexlist-mask-alist/toposort x)))
    (svex-mask-alist-complete mask-al)))

Theorem: svexlist-mask-alist/toposort-lookup

(defthm svexlist-mask-alist/toposort-lookup
  (b* (((mv ?mask-al ?toposort)
        (svexlist-mask-alist/toposort x)))
    (implies (member-equal (svex-fix y)
                           (svexlist-fix x))
             (equal (svex-mask-lookup y mask-al)
                    -1))))

Theorem: svex-argmasks-lookup-of-svexlist-mask-alist/toposort

(defthm svex-argmasks-lookup-of-svexlist-mask-alist/toposort
  (b* (((mv ?mask-al ?toposort)
        (svexlist-mask-alist/toposort x)))
    (implies (subsetp-equal (svexlist-fix y)
                            (svexlist-fix x))
             (equal (svex-argmasks-lookup y mask-al)
                    (replicate (len y) -1)))))