# Rlp-encode-tree-prefix-unambiguity-proof

Property that no valid RLP tree encoding
is a strict prefix of another one.

This is quite analogous to the proof for byte array encoding.

We cannot, and do not need to, prove a similar property
for encodings of lists of trees,
because a list of encoded trees could be extended with another one.
However, when we decode a list of trees,
we know the total length of their super-tree,
because at the top level we always start by decoding a tree,
never a list of trees.

### Definitions and Theorems

**Theorem: **rlp-encode-tree-umamb-prefix

(defthm rlp-encode-tree-umamb-prefix
(implies (and (not (mv-nth 0 (rlp-encode-tree x)))
(not (mv-nth 0 (rlp-encode-tree y))))
(equal (prefixp (mv-nth 1 (rlp-encode-tree x))
(mv-nth 1 (rlp-encode-tree y)))
(equal (mv-nth 1 (rlp-encode-tree x))
(mv-nth 1 (rlp-encode-tree y))))))