		Search-engine friendly clone of the ACL2 documentation.

Explode-implode-equalities

Theorems about equalities involving explode and implode.

Definitions and Theorems

Theorem: equal-of-implode-left-to-equal-of-explode-right

(defthm equal-of-implode-left-to-equal-of-explode-right
  (implies (and (character-listp a) (stringp b))
           (equal (equal (implode a) b)
                  (equal a (explode b)))))

Theorem: equal-of-implode-right-to-equal-of-explode-left

(defthm equal-of-implode-right-to-equal-of-explode-left
  (implies (and (character-listp a) (stringp b))
           (equal (equal a (implode b))
                  (equal (explode a) b))))

Theorem: equal-of-explode-left-to-equal-of-implode-right

(defthm equal-of-explode-left-to-equal-of-implode-right
  (implies (and (character-listp a) (stringp b))
           (equal (equal (explode a) b)
                  (equal a (implode b)))))

Theorem: equal-of-explode-right-to-equal-of-implode-left

(defthm equal-of-explode-right-to-equal-of-implode-left
  (implies (and (character-listp a) (stringp b))
           (equal (equal a (explode b))
                  (equal (implode a) b))))