		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svexlist-toposort-p

Signature
(svexlist-toposort-p x) → *
Arguments: x — Guard (svexlist-p x).

Definitions and Theorems

Function: svexlist-toposort-p

(defun svexlist-toposort-p (x)
  (declare (xargs :guard (svexlist-p x)))
  (let ((__function__ 'svexlist-toposort-p))
    (declare (ignorable __function__))
    (b* (((when (atom x)) t)
         (rest (mbe :logic (svexlist-fix (cdr x))
                    :exec (cdr x)))
         (first (car x)))
      (and (or (not (eq (svex-kind first) :call))
               (subsetp-equal (svex-call->args first)
                              rest))
           (svexlist-toposort-p rest)))))

Theorem: svexlist-toposort-p-of-svexlist-fix-x

(defthm svexlist-toposort-p-of-svexlist-fix-x
  (equal (svexlist-toposort-p (svexlist-fix x))
         (svexlist-toposort-p x)))

Theorem: svexlist-toposort-p-svexlist-equiv-congruence-on-x

(defthm svexlist-toposort-p-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-toposort-p x)
                  (svexlist-toposort-p x-equiv)))
  :rule-classes :congruence)