\patchof{L} = \pa{L} \lor \patchof{L} = \bot
}\]
\[ \eqn{ Non-recursion }{
- L \not\in \pa{Q}
+ L \not\haspatch \pa{Q}
}\]
\subsection{No Replay}
\subsection{Base Acyclic}
-Consider some $D \isin B$. If $D = B$, $D \in \pn$, OK.
-
-If $D \neq B$, $D \isin L$. By No Replay of $D$ in $L$, $D \le L$.
-Thus by Foreign Contents of $L$, $\patchof{D} = \bot$. OK.
-
-xxx this is wrong
-
-$\qed$
+Consider some $D \isin B$. If $D = B$, $D \in \pan{Q}$.
+If $D \neq B$, $D \isin L$, and by Non-recursion
+$D \not\in \pay{Q}$. $\qed$
\subsection{Coherence and Patch Inclusion}