FTY version of check-not-call.
(fty-check-not-call term) → (mv yes/no arg)
Function:
(defun fty-check-not-call (term) (declare (xargs :guard (pseudo-termp term))) (let ((__function__ 'fty-check-not-call)) (declare (ignorable __function__)) (check-not-call (pseudo-term-fix term))))
Theorem:
(defthm booleanp-of-fty-check-not-call.yes/no (b* (((mv ?yes/no ?arg) (fty-check-not-call term))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-fty-check-not-call.arg (b* (((mv ?yes/no ?arg) (fty-check-not-call term))) (pseudo-termp arg)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-term-count-of-check-not-call.arg (implies (pseudo-termp term) (b* (((mv yes/no arg) (check-not-call term))) (implies yes/no (< (pseudo-term-count arg) (pseudo-term-count term))))) :rule-classes :linear)
Theorem:
(defthm pseudo-term-count-of-fty-check-not-call.arg (b* (((mv ?yes/no ?arg) (fty-check-not-call term))) (implies yes/no (< (pseudo-term-count arg) (pseudo-term-count term)))) :rule-classes :linear)