		Search-engine friendly clone of the ACL2 documentation.

Defbytelist-standard-instances

Ubyte4-list

Fixtype of true lists of unsigned bytes of size 4.

This is an ordinary fty::deflist.

Theorem: ubyte4-listp-forward-unsigned-byte-listp

(defthm ubyte4-listp-forward-unsigned-byte-listp
  (implies (ubyte4-listp x)
           (unsigned-byte-listp 4 x))
  :rule-classes :forward-chaining)

Theorem: ubyte4-listp-rewrite-unsigned-byte-listp

(defthm ubyte4-listp-rewrite-unsigned-byte-listp
  (equal (ubyte4-listp x)
         (unsigned-byte-listp 4 x)))

Theorem: unsigned-byte-listp-rewrite-ubyte4-listp

(defthm unsigned-byte-listp-rewrite-ubyte4-listp
  (equal (unsigned-byte-listp 4 x)
         (ubyte4-listp x)))

Theorem: true-listp-when-ubyte4-listp-rewrite

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

Theorem: ubyte4-list-fix-of-take

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

Theorem: ubyte4-list-fix-of-rcons

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

Subtopics

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