		Search-engine friendly clone of the ACL2 documentation.

Transdeps

Transdeps-direct-for-nodes

Get the set of direct dependencies for a set of nodes.

Signature
(transdeps-direct-for-nodes nodes graph) → deps
Arguments: nodes — Guard (setp nodes).
Returns: deps — Type (setp deps).

Definitions and Theorems

Function: transdeps-direct-for-nodes

(defun transdeps-direct-for-nodes (nodes graph)
  (declare (xargs :guard (setp nodes)))
  (let ((__function__ 'transdeps-direct-for-nodes))
    (declare (ignorable __function__))
    (if (emptyp nodes)
        nil
      (union (transdeps-direct-for-node (head nodes)
                                        graph)
             (transdeps-direct-for-nodes (tail nodes)
                                         graph)))))

Theorem: setp-of-transdeps-direct-for-nodes

(defthm setp-of-transdeps-direct-for-nodes
  (b* ((deps (transdeps-direct-for-nodes nodes graph)))
    (setp deps))
  :rule-classes :rewrite)

Theorem: transdeps-direct-for-nodes-in

(defthm transdeps-direct-for-nodes-in
  (implies (in a
               (transdeps-direct-for-nodes nodes graph))
           (in a (transdeps-allnodes graph))))

Theorem: transdeps-direct-for-nodes-subset

(defthm transdeps-direct-for-nodes-subset
  (subset (transdeps-direct-for-nodes nodes graph)
          (transdeps-allnodes graph)))