Injectivity of `rlp-encode-tree`
and `rlp-encode-tree-list`,
over the encodable trees and lists thereof.

This is proved by induction.
There are two theorems:
one for `rlp-encode-tree`
and one for `rlp-encode-tree-list`.
The theorems are formulated similarly to
the one for `rlp-encode-bytes`.

Since the theorems involve two variables (two trees or two lists of trees),
we locally define mutually recursive functions `defines`.

Attempting to induct according to the mutually recursive encoding functions only applies to one variable, leaving the other variable unchanged in the hypotheses and conclusions of the induction steps: then the same unchanged variable cannot suitably ``relate'' to the different instances of the changing variable in the hypotheses and conclusions. Submitting the injectivity theorems via the flag theorem macro of the encoding functions, an examining the induction scheme printed by ACL2, should make the problem apparent.

The induction proof makes use of two helper lemmas.

The first helper lemma applies to the two cases in which
`rlp-encode-tree` to expand on `rlp-encode-bytes` on the subtrees.
This motivates the formulation of the first helper lemma,
whose variable `rlp-encode-tree` in the subgoal
is not expanded.
We use an expansion hint to expand that; an enable hint does not suffice.
If `rlp-encode-tree` reduces to `rlp-encode-bytes` on the subtrees
and the injectivity theorem of `rlp-encode-bytes` applies.
Otherwise, the expansion starts with a byte that is at least 192 or 247,
which is incompatible with
the starting byte of `rlp-encode-bytes` on (the subtrees of)

The second helper lemma applies to the case in which
the lists of trees `append`s
of the encodings of their `car`s and of their `cdr`s.
Commenting out this helper lemma from the hints of the induction theorem
shows a subgoal that involves these `append`s.
To use the induction hypotheses,
we need to decompose the equality of the `append`s
into the equalities of their `car` and `cdr` encodings,
via the rule `rlp-encode-bytes`.
For this, we need to relieve the hypothesis of that rule
that the lengths of the encodings of the `car`s are equal:
this is done by the lemma

The key to proving `car`s
are completely determined by the first (few) bytes of the encodings,
as expressed by the rule `car`s of `append`s of the encodings of the `car`s
with something else (the encodings of the `cdr`s) are equal.
Fortunately, the first (few) bytes of the encodings of the `car`s
are also the first (few) bytes of the `append`s.
So we use the rules
`append`s;
note that these two rules have a strictly more complex right hand side,
so they are generally undesirable,
yet they are useful in this proof.
We disable the rules

The two helper lemmas are enabled
in the proof by induction of the injectivity lemmas,
along with the rule

Similarly to the injectivity theorem for `rlp-encode-bytes`,
the injectivity theorems
for `rlp-encode-tree` and `rlp-encode-tree-list`
omit the `rlp-treep` and `rlp-tree-listp` hypotheses
and weaken the equality
with `rlp-tree-fix` and `rlp-tree-list-fix`.
These theorems subsume the lemmas,
but attempting to prove directly the theorems by induction fails.

**Theorem: **

(defthm rlp-encode-tree-injective (implies (and (not (mv-nth 0 (rlp-encode-tree x))) (not (mv-nth 0 (rlp-encode-tree y)))) (equal (equal (mv-nth 1 (rlp-encode-tree x)) (mv-nth 1 (rlp-encode-tree y))) (equal (rlp-tree-fix x) (rlp-tree-fix y)))))

**Theorem: **

(defthm rlp-encode-tree-list-injective (implies (and (not (mv-nth 0 (rlp-encode-tree-list xs))) (not (mv-nth 0 (rlp-encode-tree-list ys)))) (equal (equal (mv-nth 1 (rlp-encode-tree-list xs)) (mv-nth 1 (rlp-encode-tree-list ys))) (equal (rlp-tree-list-fix xs) (rlp-tree-list-fix ys)))))