|
|
|---|
|
|
|
|---|
Fixtype of true lists of unsigned bytes of size 3.
This is an ordinary fty::deflist.
Theorem:
(defthm ubyte3-listp-forward-unsigned-byte-listp (implies (ubyte3-listp x) (unsigned-byte-listp 3 x)) :rule-classes :forward-chaining)
Theorem:
(defthm ubyte3-listp-rewrite-unsigned-byte-listp (equal (ubyte3-listp x) (unsigned-byte-listp 3 x)))
Theorem:
(defthm unsigned-byte-listp-rewrite-ubyte3-listp (equal (unsigned-byte-listp 3 x) (ubyte3-listp x)))
Theorem:
(defthm true-listp-when-ubyte3-listp-rewrite (implies (ubyte3-listp x) (true-listp x)))
Theorem:
(defthm ubyte3-list-fix-of-take (implies (<= (nfix n) (len x)) (equal (ubyte3-list-fix (take n x)) (take n (ubyte3-list-fix x)))))
Theorem:
(defthm ubyte3-list-fix-of-rcons (equal (ubyte3-list-fix (rcons a x)) (rcons (ubyte3-fix a) (ubyte3-list-fix x))))