		Search-engine friendly clone of the ACL2 documentation.

Atj-java-syntax-operations

Unmake-right-assoc-condand

Split a right-associated conditional conjunction into its conjuncts.

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

Let the expression be expr1 && (expr2 && (... && exprN)...), where exprN is not a conditional conjunction. We return the list of expr1, expr2, ..., exprN.

Definitions and Theorems

Function: unmake-right-assoc-condand

(defun unmake-right-assoc-condand (expr)
 (declare (xargs :guard (jexprp expr)))
 (let ((__function__ 'unmake-right-assoc-condand))
  (declare (ignorable __function__))
  (if (and (jexpr-case expr :binary)
           (jbinop-case (jexpr-binary->op expr)
                        :condand))
      (cons (jexpr-binary->left expr)
            (unmake-right-assoc-condand (jexpr-binary->right expr)))
    (list (jexpr-fix expr)))))

Theorem: jexpr-listp-of-unmake-right-assoc-condand

(defthm jexpr-listp-of-unmake-right-assoc-condand
  (b* ((exprs (unmake-right-assoc-condand expr)))
    (jexpr-listp exprs))
  :rule-classes :rewrite)

Theorem: consp-of-unmake-right-assoc-condand

(defthm consp-of-unmake-right-assoc-condand
  (b* ((?exprs (unmake-right-assoc-condand expr)))
    (consp exprs))
  :rule-classes :type-prescription)

Theorem: unmake-right-assoc-condand-of-jexpr-fix-expr

(defthm unmake-right-assoc-condand-of-jexpr-fix-expr
  (equal (unmake-right-assoc-condand (jexpr-fix expr))
         (unmake-right-assoc-condand expr)))

Theorem: unmake-right-assoc-condand-jexpr-equiv-congruence-on-expr

(defthm unmake-right-assoc-condand-jexpr-equiv-congruence-on-expr
  (implies (jexpr-equiv expr expr-equiv)
           (equal (unmake-right-assoc-condand expr)
                  (unmake-right-assoc-condand expr-equiv)))
  :rule-classes :congruence)