(call-graph-extdecl-list extdecls acc) → call-graph
Function:
(defun call-graph-extdecl-list (extdecls acc) (declare (xargs :guard (and (extdecl-listp extdecls) (ident-ident-option-set-mapp acc)))) (let ((__function__ 'call-graph-extdecl-list)) (declare (ignorable __function__)) (if (endp extdecls) (ident-ident-option-set-map-fix acc) (call-graph-extdecl-list (rest extdecls) (call-graph-extdecl (first extdecls) acc)))))
Theorem:
(defthm ident-ident-option-set-mapp-of-call-graph-extdecl-list (b* ((call-graph (call-graph-extdecl-list extdecls acc))) (ident-ident-option-set-mapp call-graph)) :rule-classes :rewrite)