		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-simplify-conds

Atj-simplify-conds-in-jexpr

Simplify conditional expressions whose condition is a boolean literal, in expressions.

Signature
(atj-simplify-conds-in-jexpr expr) → new-expr
Arguments: expr — Guard (jexprp expr).
Returns: new-expr — Type (jexprp new-expr).

Theorem: return-type-of-atj-simplify-conds-in-jexpr.new-expr

(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: return-type-of-atj-simplify-conds-in-jexprs.new-exprs

(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: atj-simplify-conds-in-jexpr-of-jexpr-fix-expr

(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: atj-simplify-conds-in-jexprs-of-jexpr-list-fix-exprs

(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: atj-simplify-conds-in-jexpr-jexpr-equiv-congruence-on-expr

(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: atj-simplify-conds-in-jexprs-jexpr-list-equiv-congruence-on-exprs

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

Subtopics

Atj-simplify-conds-in-jexprs