\gathbegin
B \hasparents \{ L \}
\gathnext
- \patchof{B} = \pan{B}
+ \patchof{B} = \pan{Q}
\gathnext
D \isin B \equiv D \isin L \lor D = B
\end{gather}
\patchof{L} = \pa{L} \lor \patchof{L} = \bot
}\]
\[ \eqn{ Non-recursion }{
- L \not\in \pa{B}
+ L \not\in \pa{Q}
}\]
\subsection{No Replay}