Return the leftmost term in a list that is not a quoted constant.
This is used as explained in step-from-trans.
If there is no such term, we return
(defun get-leftmost-nonconst (terms) (declare (xargs :guard (tterm-listp terms))) (let ((__function__ 'get-leftmost-nonconst)) (declare (ignorable __function__)) (b* (((when (endp terms)) nil) (term (car terms)) ((when (tterm-case term :constant)) (get-leftmost-nonconst (cdr terms)))) (tterm-fix term))))
(defthm maybe-ttermp-of-get-leftmost-nonconst (b* ((term? (get-leftmost-nonconst terms))) (maybe-ttermp term?)) :rule-classes :rewrite)
(defthm tterm-case-constant-listp-when-not-get-leftmost-nonconst (implies (and (tterm-listp terms) (not (ttermp (get-leftmost-nonconst terms)))) (tterm-case-constant-listp terms)))
(defthm get-leftmost-nonconst-of-tterm-list-fix-terms (equal (get-leftmost-nonconst (tterm-list-fix terms)) (get-leftmost-nonconst terms)))
(defthm get-leftmost-nonconst-tterm-list-equiv-congruence-on-terms (implies (tterm-list-equiv terms terms-equiv) (equal (get-leftmost-nonconst terms) (get-leftmost-nonconst terms-equiv))) :rule-classes :congruence)