Topologically-ordered-p-aux
- Signature
(topologically-ordered-p-aux nodes graph seen)
→
(mv ordered-p seen)
Definitions and Theorems
Function: topologically-ordered-p-aux
(defun topologically-ordered-p-aux (nodes graph seen)
(declare (xargs :guard t))
(let ((__function__ 'topologically-ordered-p-aux))
(declare (ignorable __function__))
(b* (((when (atom nodes)) (mv t seen))
(node1 (car nodes))
(deps1 (cdr (hons-get node1 graph)))
((unless (fal-all-boundp deps1 seen))
(mv nil seen))
(seen (hons-acons node1 t seen)))
(topologically-ordered-p-aux (cdr nodes)
graph seen))))
