From e85a1027d1e71d92995bf58f2a0e0930fd5ebfb5 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 17 Apr 2019 18:00:53 +0200
Subject: [PATCH] Sketch proof
---
docs/ghost-state.tex | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 169dcfaeb..953a2fea7 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -72,6 +72,13 @@ This rule looks different from the above ones, because we still do not have that
\inferH{later-fake-rule}{\timeless{\prop}}
{\later\prop \proves \prop}
\end{mathpar}
+The proof of the former is $\later \prop \proves \diamond \prop =
+\later\FALSE \lor \prop$, and then by straightforward disjunction elimination:
+% Cut the second part if trivial.
+\begin{mathpar}
+ \infer{\later\FALSE \proves \later \propB \and \prop \proves \later \propB}
+ {\later\FALSE \lor \prop \proves \propB}
+\end{mathpar}
The following rules can be derived about except-0:
--
GitLab