		Search-engine friendly clone of the ACL2 documentation.

Atj-java-syntax-operations

Make-right-assoc-condand

Make a right-associated conditional conjunction from a non-empty list of conjuncts.

Signature
(make-right-assoc-condand exprs) → expr
Arguments: exprs — Guard (jexpr-listp exprs).
Returns: expr — Type (jexprp expr).

Definitions and Theorems

Function: make-right-assoc-condand

(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: jexprp-of-make-right-assoc-condand

(defthm jexprp-of-make-right-assoc-condand
  (b* ((expr (make-right-assoc-condand exprs)))
    (jexprp expr))
  :rule-classes :rewrite)

Theorem: make-right-assoc-condand-of-jexpr-list-fix-exprs

(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: make-right-assoc-condand-jexpr-list-equiv-congruence-on-exprs

(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)