(m-assumption-n-output-comb-transform->name x) → name
Function:
(defun m-assumption-n-output-comb-transform->name (x) (declare (xargs :guard (m-assumption-n-output-comb-transform-p x))) (let ((__function__ 'm-assumption-n-output-comb-transform->name)) (declare (ignorable __function__)) (case (tag (m-assumption-n-output-comb-transform-fix x)) (:n-outputs-unreachability-config "N-output Unreachability") (:n-outputs-dom-supergates-sweep-config "N-output observability supergate sweep") (:m-assum-n-output-observability-config "M-assumption N-output observability") (:parametrize-config "Parametrization") (otherwise (comb-transform->name x)))))
Theorem:
(defthm stringp-of-m-assumption-n-output-comb-transform->name (b* ((name (m-assumption-n-output-comb-transform->name x))) (stringp name)) :rule-classes :type-prescription)