Make a right-associated conditional conjunction from a non-empty list of conjuncts.
(make-right-assoc-condand exprs) → expr
Function:
(defun make-right-assoc-condand (exprs) (declare (xargs :guard (jexpr-listp exprs))) (declare (xargs :guard (consp exprs))) (let ((__function__ 'make-right-assoc-condand)) (declare (ignorable __function__)) (cond ((not (mbt (consp exprs))) (ec-call (jexpr-fix :irrelevant))) ((consp (cdr exprs)) (jexpr-binary (jbinop-condand) (jexpr-fix (car exprs)) (make-right-assoc-condand (cdr exprs)))) (t (jexpr-fix (car exprs))))))
Theorem:
(defthm jexprp-of-make-right-assoc-condand (b* ((expr (make-right-assoc-condand exprs))) (jexprp expr)) :rule-classes :rewrite)
Theorem:
(defthm make-right-assoc-condand-of-jexpr-list-fix-exprs (equal (make-right-assoc-condand (jexpr-list-fix exprs)) (make-right-assoc-condand exprs)))
Theorem:
(defthm make-right-assoc-condand-jexpr-list-equiv-congruence-on-exprs (implies (jexpr-list-equiv exprs exprs-equiv) (equal (make-right-assoc-condand exprs) (make-right-assoc-condand exprs-equiv))) :rule-classes :congruence)