Memoized. Get the set of dependencies for a single node.
(transdeps-direct-for-node node graph) → deps
Function:
(defun transdeps-direct-for-node (node graph) (declare (xargs :guard t)) (let ((__function__ 'transdeps-direct-for-node)) (declare (ignorable __function__)) (mbe :logic (mergesort (cdr (hons-get node graph))) :exec (b* ((look (cdr (hons-get node graph)))) (if (setp look) look (mergesort look))))))
Theorem:
(defthm setp-of-transdeps-direct-for-node (b* ((deps (transdeps-direct-for-node node graph))) (setp deps)) :rule-classes :rewrite)
Theorem:
(defthm transdeps-direct-for-node-in (implies (in a (transdeps-direct-for-node node graph)) (in a (transdeps-allnodes graph))))
Theorem:
(defthm transdeps-direct-for-node-subset (subset (transdeps-direct-for-node node graph) (transdeps-allnodes graph)))