Check if a byte array is an RLP encoding of a tree.

This is a declarative, non-executable definition,
which essentially characterizes the image of `rlp-encode-tree`
(over trees that can be encoded,
i.e. such that `rlp-encode-tree` returns a

By definition, the witness function is right inverse of the encoding function, over the valid encodings.

**Theorem: **

(defthm rlp-tree-encoding-p-suff (implies (and (rlp-treep tree) (b* (((mv error? encoding1) (rlp-encode-tree tree))) (and (not error?) (equal encoding1 (byte-list-fix encoding))))) (rlp-tree-encoding-p encoding)))

**Theorem: **

(defthm booleanp-of-rlp-tree-encoding-p (b* ((yes/no (rlp-tree-encoding-p encoding))) (booleanp yes/no)) :rule-classes :rewrite)

**Theorem: **

(defthm rlp-tree-encoding-p-of-byte-list-fix-encoding (equal (rlp-tree-encoding-p (byte-list-fix encoding)) (rlp-tree-encoding-p encoding)))

**Theorem: **

(defthm rlp-tree-encoding-p-byte-list-equiv-congruence-on-encoding (implies (byte-list-equiv encoding encoding-equiv) (equal (rlp-tree-encoding-p encoding) (rlp-tree-encoding-p encoding-equiv))) :rule-classes :congruence)

**Theorem: **

(defthm rlp-treep-of-rlp-tree-encoding-witness (implies (rlp-tree-encoding-p encoding) (rlp-treep (rlp-tree-encoding-witness encoding))))

**Theorem: **

(defthm rlp-encode-tree-of-rlp-tree-encoding-witness (implies (rlp-tree-encoding-p encoding) (b* (((mv error? encoding1) (rlp-encode-tree (rlp-tree-encoding-witness encoding)))) (and (not error?) (equal encoding1 (byte-list-fix encoding))))))

**Theorem: **

(defthm rlp-tree-encoding-p-of-rlp-tree-encode-when-no-error (implies (not (mv-nth 0 (rlp-encode-tree tree))) (rlp-tree-encoding-p (mv-nth 1 (rlp-encode-tree tree)))))