		Search-engine friendly clone of the ACL2 documentation.

Fty-if-to-if*

Replace each if with if* in a term.

Theorem: return-type-of-fty-if-to-if*.term1

(defthm return-type-of-fty-if-to-if*.term1
  (b* ((?term1 (fty-if-to-if* term)))
    (pseudo-termp term1))
  :rule-classes :rewrite)

Theorem: return-type-of-fty-if-to-if*-lst.terms1

(defthm return-type-of-fty-if-to-if*-lst.terms1
  (b* ((?terms1 (fty-if-to-if*-lst terms)))
    (pseudo-term-listp terms1))
  :rule-classes :rewrite)

Theorem: len-of-fty-if-to-if*-lst

(defthm len-of-fty-if-to-if*-lst
  (b* ((?terms1 (fty-if-to-if*-lst terms)))
    (equal (len terms1) (len terms))))