Split a right-associated conditional conjunction into its conjuncts.
(unmake-right-assoc-condand expr) → exprs
Let the expression be
Function:
(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:
(defthm jexpr-listp-of-unmake-right-assoc-condand (b* ((exprs (unmake-right-assoc-condand expr))) (jexpr-listp exprs)) :rule-classes :rewrite)
Theorem:
(defthm consp-of-unmake-right-assoc-condand (b* ((?exprs (unmake-right-assoc-condand expr))) (consp exprs)) :rule-classes :type-prescription)
Theorem:
(defthm unmake-right-assoc-condand-of-jexpr-fix-expr (equal (unmake-right-assoc-condand (jexpr-fix expr)) (unmake-right-assoc-condand expr)))
Theorem:
(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)