Simplify conditional expressions whose condition is a boolean literal, in expressions.
Theorem:
(defthm return-type-of-atj-simplify-conds-in-jexpr.new-expr (b* ((?new-expr (atj-simplify-conds-in-jexpr expr))) (jexprp new-expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-simplify-conds-in-jexprs.new-exprs (b* ((?new-exprs (atj-simplify-conds-in-jexprs exprs))) (jexpr-listp new-exprs)) :rule-classes :rewrite)
Theorem:
(defthm atj-simplify-conds-in-jexpr-of-jexpr-fix-expr (equal (atj-simplify-conds-in-jexpr (jexpr-fix expr)) (atj-simplify-conds-in-jexpr expr)))
Theorem:
(defthm atj-simplify-conds-in-jexprs-of-jexpr-list-fix-exprs (equal (atj-simplify-conds-in-jexprs (jexpr-list-fix exprs)) (atj-simplify-conds-in-jexprs exprs)))
Theorem:
(defthm atj-simplify-conds-in-jexpr-jexpr-equiv-congruence-on-expr (implies (jexpr-equiv expr expr-equiv) (equal (atj-simplify-conds-in-jexpr expr) (atj-simplify-conds-in-jexpr expr-equiv))) :rule-classes :congruence)
Theorem:
(defthm atj-simplify-conds-in-jexprs-jexpr-list-equiv-congruence-on-exprs (implies (jexpr-list-equiv exprs exprs-equiv) (equal (atj-simplify-conds-in-jexprs exprs) (atj-simplify-conds-in-jexprs exprs-equiv))) :rule-classes :congruence)