		Search-engine friendly clone of the ACL2 documentation.

Defbytelist-standard-instances

Ubyte32-list

Fixtype of true lists of unsigned bytes of size 32.

This is an ordinary fty::deflist.

Theorem: ubyte32-listp-forward-unsigned-byte-listp

(defthm ubyte32-listp-forward-unsigned-byte-listp
  (implies (ubyte32-listp x)
           (unsigned-byte-listp 32 x))
  :rule-classes :forward-chaining)

Theorem: ubyte32-listp-rewrite-unsigned-byte-listp

(defthm ubyte32-listp-rewrite-unsigned-byte-listp
  (equal (ubyte32-listp x)
         (unsigned-byte-listp 32 x)))

Theorem: unsigned-byte-listp-rewrite-ubyte32-listp

(defthm unsigned-byte-listp-rewrite-ubyte32-listp
  (equal (unsigned-byte-listp 32 x)
         (ubyte32-listp x)))

Theorem: true-listp-when-ubyte32-listp-rewrite

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

Theorem: ubyte32-list-fix-of-take

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

Theorem: ubyte32-list-fix-of-rcons

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

Subtopics

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