# Rlp-encode-bytes-prefix-unambiguity-proof

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 len-of-rlp-encode-bytes-from-prefix.
We use suitable instances of
acl2::same-car-when-prefixp-and-consp and
acl2::same-take-when-prefixp-and-longer
to establish that the first (few) bytes of the encodings are the same.

### Definitions and Theorems

**Theorem: **rlp-encode-bytes-unamb-prefix

(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))))))