Check if an expression is a multiplication.
If it is, return its two sub-expressions.
Function:
(defun check-expr-mul (expr) (declare (xargs :guard (exprp expr))) (let ((__function__ 'check-expr-mul)) (declare (ignorable __function__)) (if (and (expr-case expr :binary) (binop-case (expr-binary->op expr) :mul)) (mv t (expr-binary->arg1 expr) (expr-binary->arg2 expr)) (mv nil (irr-expr) (irr-expr)))))
Theorem:
(defthm booleanp-of-check-expr-mul.yes/no (b* (((mv ?yes/no ?arg1 ?arg2) (check-expr-mul expr))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm exprp-of-check-expr-mul.arg1 (b* (((mv ?yes/no ?arg1 ?arg2) (check-expr-mul expr))) (exprp arg1)) :rule-classes :rewrite)
Theorem:
(defthm exprp-of-check-expr-mul.arg2 (b* (((mv ?yes/no ?arg1 ?arg2) (check-expr-mul expr))) (exprp arg2)) :rule-classes :rewrite)
Theorem:
(defthm expr-count-of-check-expr-mul-arg1 (b* (((mv ?yes/no ?arg1 ?arg2) (check-expr-mul expr))) (implies yes/no (< (expr-count arg1) (expr-count expr)))) :rule-classes :linear)
Theorem:
(defthm expr-count-of-check-expr-mul-arg2 (b* (((mv ?yes/no ?arg1 ?arg2) (check-expr-mul expr))) (implies yes/no (< (expr-count arg2) (expr-count expr)))) :rule-classes :linear)
Theorem:
(defthm check-expr-mul-of-expr-fix-expr (equal (check-expr-mul (expr-fix expr)) (check-expr-mul expr)))
Theorem:
(defthm check-expr-mul-expr-equiv-congruence-on-expr (implies (expr-equiv expr expr-equiv) (equal (check-expr-mul expr) (check-expr-mul expr-equiv))) :rule-classes :congruence)