Property that no valid RLP byte array encoding is a strict prefix of another one.
This is expressed by saying that if a valid encoding is a prefix of another one, the two encodings must be equal. Thus, it is not possible for a valid encoding to be a strict prefix of another valid encoding.
We do a case split on whether the two encodings have the same length
(in which case the prefix relationship implies equality),
or not.
In the latter case,
we show that in fact the two encodings must have the same length
(and therefore we get a contradiction),
because the length of an encoding is determined
by its first byte or few bytes:
we thus enable the rule
Theorem:
(defthm rlp-encode-bytes-unamb-prefix (implies (and (not (mv-nth 0 (rlp-encode-bytes x))) (not (mv-nth 0 (rlp-encode-bytes y)))) (equal (prefixp (mv-nth 1 (rlp-encode-bytes x)) (mv-nth 1 (rlp-encode-bytes y))) (equal (mv-nth 1 (rlp-encode-bytes x)) (mv-nth 1 (rlp-encode-bytes y))))))