(call-graph-transitive-closure0 ident?s call-graph acc steps) → called
Function:
(defun call-graph-transitive-closure0 (ident?s call-graph acc steps) (declare (type (unsigned-byte 60) steps)) (declare (xargs :guard (and (ident-option-setp ident?s) (ident-ident-option-set-mapp call-graph) (ident-option-setp acc)))) (let ((__function__ 'call-graph-transitive-closure0)) (declare (ignorable __function__)) (b* (((when (or (int= 0 (mbe :logic (if (natp (acl2::the-fixnat steps)) (acl2::the-fixnat steps) 0) :exec (acl2::the-fixnat steps))) (emptyp ident?s))) (ident-option-set-fix acc)) (ident? (head ident?s)) ((when (not ident?)) (call-graph-transitive-closure0 (tail ident?s) call-graph (insert nil acc) (- steps 1))) (lookup (omap::assoc ident? call-graph)) (ident?s (if lookup (union (difference (cdr lookup) acc) (tail ident?s)) (tail ident?s))) (acc (if lookup (union (cdr lookup) acc) acc))) (call-graph-transitive-closure0 ident?s call-graph acc (- steps 1)))))
Theorem:
(defthm ident-option-setp-of-call-graph-transitive-closure0 (b* ((called (call-graph-transitive-closure0 ident?s call-graph acc steps))) (ident-option-setp called)) :rule-classes :rewrite)