		Search-engine friendly clone of the ACL2 documentation.

Bytes

Byte-sequences

Byte sequences.

These are finite lists of bytes, which model byte arrays in particular.

We use the library type byte-list to model byte sequences in our Bitcoin model.

Definitions and Theorems

Theorem: nat-listp-when-byte-listp

(defthm nat-listp-when-byte-listp
  (implies (byte-listp bytes)
           (nat-listp bytes)))

Theorem: car-of-byte-list-fix

(defthm car-of-byte-list-fix
  (implies (consp x)
           (equal (car (byte-list-fix x))
                  (byte-fix (car x)))))

Theorem: cdr-of-byte-list-fix

(defthm cdr-of-byte-list-fix
  (equal (cdr (byte-list-fix x))
         (byte-list-fix (cdr x))))

Theorem: byte-list-equiv-implies-byte-list-equiv-append-1

(defthm byte-list-equiv-implies-byte-list-equiv-append-1
  (implies (byte-list-equiv x x-equiv)
           (byte-list-equiv (append x y)
                            (append x-equiv y)))
  :rule-classes (:congruence))

Theorem: byte-list-equiv-implies-byte-list-equiv-append-2

(defthm byte-list-equiv-implies-byte-list-equiv-append-2
  (implies (byte-list-equiv y y-equiv)
           (byte-list-equiv (append x y)
                            (append x y-equiv)))
  :rule-classes (:congruence))