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