Lemma 22 ([A walk tests a shared readout]). For distinct blocks B,C and a shared name ρ , there is a fixed sequence of sorts such that s_B^(z) and s_C^(w) are joined by a walk following that sequence if and only if z|_ρ=w|_ρ . The sequence …

Starting at channel zero of B , follow its spine to c_B(C,ρ) , then go to the leaf and ascend its tree to the root. Cross the matching to the opposite root in C . Descend to a leaf, go to its spine, and follow the spine to channel zero of C . Record the sort at every position of this route. When a root is also a leaf it contributes just one position. The route is illustrated in. The sorts specify the block and channel throughout, and the level of each tree vertex. Every spine step preserves the full valuation. The leaf is indexed by that valuation, and truncation to the root retains exactly the coordinates of ρ . The prescribed step to the opposite root can only use the matching of equal values. A descent on the other side extends that same root value, and its subsequent spine steps preserve the chosen extension. Consequently every walk with the specified sorts has equal endpoint readouts. Conversely, when the endpoint readouts agree, their two prefix paths reach a matched pair of roots and give the required walk.