		Search-engine friendly clone of the ACL2 documentation.

Defbytelist-standard-instances

Ubyte8-list

Fixtype of true lists of unsigned bytes of size 8.

This is an ordinary fty::deflist.

Theorem: ubyte8-listp-forward-unsigned-byte-listp

(defthm ubyte8-listp-forward-unsigned-byte-listp
  (implies (ubyte8-listp x)
           (unsigned-byte-listp 8 x))
  :rule-classes :forward-chaining)

Theorem: ubyte8-listp-rewrite-unsigned-byte-listp

(defthm ubyte8-listp-rewrite-unsigned-byte-listp
  (equal (ubyte8-listp x)
         (unsigned-byte-listp 8 x)))

Theorem: unsigned-byte-listp-rewrite-ubyte8-listp

(defthm unsigned-byte-listp-rewrite-ubyte8-listp
  (equal (unsigned-byte-listp 8 x)
         (ubyte8-listp x)))

Theorem: true-listp-when-ubyte8-listp-rewrite

(defthm true-listp-when-ubyte8-listp-rewrite
  (implies (ubyte8-listp x)
           (true-listp x)))

Theorem: ubyte8-list-fix-of-take

(defthm ubyte8-list-fix-of-take
  (implies (<= (nfix n) (len x))
           (equal (ubyte8-list-fix (take n x))
                  (take n (ubyte8-list-fix x)))))

Theorem: ubyte8-list-fix-of-rcons

(defthm ubyte8-list-fix-of-rcons
  (equal (ubyte8-list-fix (rcons a x))
         (rcons (ubyte8-fix a)
                (ubyte8-list-fix x))))

Subtopics

Ubyte8-list-fix: (ubyte8-list-fix x) is a usual fty list fixing function.
Ubyte8-list-equiv: Basic equivalence relation for ubyte8-list structures.
Ubyte8-listp: (ubyte8-listp x) recognizes lists where every element satisfies ubyte8p.