Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
George Pirlea
Iris
Commits
c02adf58
Verified
Commit
c02adf58
authored
Apr 17, 2019
by
Paolo G. Giarrusso
Browse files
Explain why the rule looks different
parent
c3e98412
Changes
1
Hide whitespace changes
Inline
Side-by-side
docs/ghost-state.tex
View file @
c02adf58
...
@@ -67,6 +67,12 @@ from timeless propositions even when working under the later modality:
...
@@ -67,6 +67,12 @@ from timeless propositions even when working under the later modality:
\infer
{
\timeless
{
\prop
}
\and
\prop
\proves
\later
\propB
}
\infer
{
\timeless
{
\prop
}
\and
\prop
\proves
\later
\propB
}
{
\later\prop
\proves
\later\propB
}
{
\later\prop
\proves
\later\propB
}
\end{mathpar}
\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:
The following rules can be derived about except-0:
\begin{mathpar}
\begin{mathpar}
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment