Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jonas Kastberg
iris
Commits
390748ab
Commit
390748ab
authored
Dec 12, 2016
by
Ralf Jung
Browse files
fix multiply defined label
parent
10186bd8
Changes
1
Hide whitespace changes
Inline
Side-by-side
docs/derived.tex
View file @
390748ab
...
...
@@ -130,7 +130,7 @@ Here are some derived rules:
\inferH
{
Slice-insert-full
}{}
{
\later\propB
*
\lateropt
b
\ABox\namesp\prop
{
f
}
\vs
[\namesp]
\Exists\sname
\notin
\dom
(f).
\always\BoxSlice\namesp\propB\sname
*
\lateropt
b
\ABox\namesp
{
\prop
*
\propB
}{
\mapinsert\sname\BoxFull
{
f
}}}
\inferH
{
Slice-
insert-empty
}
\inferH
{
Slice-
delete-full
}
{
f(
\sname
) =
\BoxFull
}
{
\BoxSlice\namesp\propB\sname
\proves
\lateropt
b
\ABox\namesp\prop
{
f
}
\vs
[\namesp]
\later\propB
*
\Exists
\prop
'.
\lateropt
b (
\later
(
\prop
=
\prop
' *
\propB
) *
\ABox\namesp
{
\prop
'
}{
\mapinsert\sname\bot
{
f
}}
)
}
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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