		Search-engine friendly clone of the ACL2 documentation.

Transdeps

Transdeps-allnodes

Overapproximation of all of the nodes in the graph.

Signature
(transdeps-allnodes graph) → nodes
Returns: nodes — Type (setp nodes).

Never executed. We just use this for termination. It's possibly an overapproximation because of shadowed pairs in the graph.

Definitions and Theorems

Function: transdeps-allnodes

(defun transdeps-allnodes (graph)
  (declare (xargs :guard t))
  (let ((__function__ 'transdeps-allnodes))
    (declare (ignorable __function__))
    (mergesort (append (alist-keys graph)
                       (flatten (alist-vals graph))))))

Theorem: setp-of-transdeps-allnodes

(defthm setp-of-transdeps-allnodes
  (b* ((nodes (transdeps-allnodes graph)))
    (setp nodes))
  :rule-classes :rewrite)