diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex index cdf29ac097628a993f8cc25ae2e07b0eb7361d15..224999e236cf3c8ee5b098be6172263015c387a6 100644 --- a/docs/ghost-state.tex +++ b/docs/ghost-state.tex @@ -67,6 +67,12 @@ from timeless propositions even when working under the later modality: \infer{\timeless{\prop} \and \prop \proves \later \propB} {\later\prop \proves \later\propB} \end{mathpar} +This rule looks different from the above ones, because we still do not have that +\begin{mathpar} + \inferH{later-fake-rule}{\timeless{\prop}} + {\later\prop \proves \prop} +\end{mathpar} + The following rules can be derived about except-0: \begin{mathpar}