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