Relation between Laver generic reals Suppose we have a ctm $M$ and $x, y$ Laver generic reals over $M$ so that $M[x] = M[y]$ (recall that Laver forcing is minimal, so that if $x \in M[y]$ then we already have $M[x] = M[y]$). Is there any "nice" relation between $x$ and $y$?
In many ways Laver forcing is close to Mathias forcing, so one particular kind of relation between $x$ and $y$ which I had in mind (but I am also interested in other kinds of relations) was the following fact which holds for $x, y$ Mathias generics:
If $z$ is a Mathias generic over a ctm $M$ and $x, y \subseteq z$ then $M[x] = M[y]$ iff $x E_0 y$, where $x E_0 y$ iff $x \Delta y$ is finite. (This is Claim 8.20 from Canonical Ramsey theory on Polish spaces by Kanovei, Sabok and Zapletal)
Since I think that minimality implies that there cannot be anything as nice for Laver forcing as there is for Mathias, here is the follow up question:
We know that we can get a Laver tree $p$ of Laver generics over $M$ (since $M$ is countable, see The Kunen-Miller chart by Judah and Shelah). Is there a Laver tree $q$ with $q \leq_0 p$ (meaning that $q$ has the same stem as $p$) where there is some "nice" relation between its branches? (or just $q \leq p$?)
 A: In a general sense, yes. What follows is perhaps not the answer you are looking for, but seems to me to be relevant nonetheless.
Recall that the following are equivalent:

*

*$\Bbb P$ is a weakly homogeneous forcing,

*If $V[G]=V[H]$ for two $V$-generic filters, then there is an automorphism of $B(\Bbb P)$ such that $\pi``G=H$.

Since you assume that $M[x]=M[y]$, and since the Laver forcing is weakly homogeneous, that means that there is an automorphism of the Boolean completion of the Laver forcing.
Now, whether or not this automorphism has a nice description arising from the Laver forcing itself or it there is some descriptive set theoretic property that gives us this equivalence, that's a different question, which I am certain someone will answer not before long.
A: The following is not precisely what I was looking for in my question (one might very well call what I did "cheating"), but since it did give me some new insight into the problem that led me to ask the question, I am posting it anyway in hope that it will also be helpful to others.
For simplicity suppose that all our Laver trees are increasing, meaning that the sequences constituting them are strictly increasing sequences (this setting is often useful when we are comparing Laver forcing to Mathias forcing, since we identify infinite strictly increasing sequences with infinite subsets of $\omega$).
We have a ctm $M$ and a Laver tree $p$ of Laver generics over $M$. Let $N$ be the smallest model containing $M$ and $p$, and let $x$ be a Mathias generic over $N$. Then there is a Laver $q \leq_0 p$ encoding $x$, in a way that moreover $y \in [q]$ correspond bijectively to $\tilde{y} \in [x]^{\infty}$. Then if $y_0, y_1 \in [q]$ satisfy $N[y_0] = N[y_1]$, then of course also $N[\tilde{y}_0] = N[\tilde{y}_1]$ (since $p \in N$ and we need only $p$ to decode $\tilde{y}_i$ from $y_i$), so by the result mentioned in my question, we have that $\tilde{y}_0 E_0 \tilde{y}_1$.
