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