Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Giuseppe Castagna
occurrence-typing
Commits
7f9f5dff
Commit
7f9f5dff
authored
Nov 13, 2020
by
Mickael Laurent
Browse files
fix
parent
7e11b6a6
Changes
1
Hide whitespace changes
Inline
Side-by-side
new_system3.tex
View file @
7f9f5dff
...
...
@@ -141,7 +141,7 @@ TODO: Theorems and proof: no need for rule Inter, etc.
\\
\Infer
[Proj*]
{
\Gamma
(x)
\equiv\textstyle\bigvee
_{
i
\in
I
}
\pair
{
t
_
i
}{
s
_
i
}
\\
\forall
i
\in
I.
\ \Gamma\subst
{
x
}{
\pair
{
t
_
i
}{
s
_
i
}}
\vdash
_
\ct
\ct
[\pi_i x]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
_
i
}
\forall
i
\in
I.
\ \Gamma\subst
{
x
}{
\pair
{
t
_
i
}{
s
_
i
}}
\vdash
_
{
[]
}
\ct
[\pi_i x]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
_
i
}
}
{
\Gamma
\vdash
_
\ct
\pi
_
i x:
\{
(u
_
j,
\Gamma
_
j)
\,\alt\,
i
\in
I,
\
j
\in
J
_
i
\}
}
{
}
...
...
@@ -150,8 +150,8 @@ TODO: Theorems and proof: no need for rule Inter, etc.
{
\Gamma
(x) = t
\\
t
\land
(
\pair
{
\Any
}{
\Any
}
)
\neq\Empty\\
t
\land\neg
(
\pair
{
\Any
}{
\Any
}
)
\neq\Empty\\
\Gamma\subst
{
x
}{
t
\land
(
\pair
{
\Any
}{
\Any
}
)
}
\vdash
_
\ct
\ct
[\pi_i x]
:
\{
(u
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\\
\Gamma\subst
{
x
}{
t
\land\neg
(
\pair
{
\Any
}{
\Any
}
)
}
\vdash
_
\ct
\ct
[\pi_i x]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
}
\Gamma\subst
{
x
}{
t
\land
(
\pair
{
\Any
}{
\Any
}
)
}
\vdash
_
{
[]
}
\ct
[\pi_i x]
:
\{
(u
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\\
\Gamma\subst
{
x
}{
t
\land\neg
(
\pair
{
\Any
}{
\Any
}
)
}
\vdash
_
{
[]
}
\ct
[\pi_i x]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
}
}
{
\Gamma
\vdash
_
\ct
\pi
_
i x:
\{
(u
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\cup\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
}}
{
}
...
...
@@ -175,7 +175,7 @@ t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
\Gamma
(x
_
1)
\equiv
\textstyle\bigwedge
_{
i
\in
I
}
\arrow
{
s
_
i
}{
t
_
i
}
\\
\Gamma
(x
_
2)=s
\\
s
\leq
\textstyle\bigvee
_{
i
\in
I
}
s
_
i
\\
\forall
i
\in
I.
\ \Gamma\subst
{
x
_
2
}{
s
\land
s
_
i
}
\vdash
_
\ct
\ct
[{x_1}{x_2}]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
_
i
}
\forall
i
\in
I.
\ \Gamma\subst
{
x
_
2
}{
s
\land
s
_
i
}
\vdash
_
{
[]
}
\ct
[{x_1}{x_2}]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
_
i
}
}
{
\Gamma
\vdash
_
\ct
{
x
_
1
}{
x
_
2
}
:
\{
(u
_
j,
\Gamma
_
j)
\,\alt\,
i
\in
I,
\
j
\in
J
_
i
\}
}
{
}
...
...
@@ -185,23 +185,23 @@ t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
\Gamma
(x
_
1)
\equiv
\textstyle\bigwedge
_{
i
\in
I
}
\arrow
{
s
_
i
}{
t
_
i
}
\\
s
_
\circ
=
\textstyle\bigvee
_{
i
\in
I
}
s
_
i
\\
\Gamma
(x
_
2)=s
\\
s
\land
s
_
\circ\neq\Empty\\
s
\land
\neg
s
_
\circ\neq\Empty\\
\Gamma\subst
{
x
_
2
}{
s
\land
s
_
\circ
}
\vdash
_
\ct
\ct
[{x_1}{x_2}]
:
\{
(u
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\\
\Gamma\subst
{
x
_
2
}{
s
\land
\neg
s
_
\circ
}
\vdash
_
\ct
\ct
[{x_1}{x_2}]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
}
\Gamma\subst
{
x
_
2
}{
s
\land
s
_
\circ
}
\vdash
_
{
[]
}
\ct
[{x_1}{x_2}]
:
\{
(u
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\\
\Gamma\subst
{
x
_
2
}{
s
\land
\neg
s
_
\circ
}
\vdash
_
{
[]
}
\ct
[{x_1}{x_2}]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
}
}
{
\Gamma
\vdash
_
\ct
{
x
_
1
}{
x
_
2
}
:
\{
(u
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\cup\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
}
}
{
}
\\
\Infer
[AppL*]
{
\Gamma
(x
_
1)
\equiv\textstyle\bigvee
_{
i
\in
I
}
t
_
i
\leq\arrow
{
\Empty
}{
\Any
}
\\
\forall
i
\in
I.
\ \Gamma\subst
{
x
_
1
}{
t
_
i
}
\vdash
_
\ct
\ct
[{x_1}{x_2}]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
_
i
}
\forall
i
\in
I.
\ \Gamma\subst
{
x
_
1
}{
t
_
i
}
\vdash
_
{
[]
}
\ct
[{x_1}{x_2}]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
_
i
}
}
{
\Gamma
\vdash
_
\ct
{
x
_
1
}{
x
_
2
}
:
\{
(u
_
j,
\Gamma
_
j)
\,\alt\,
i
\in
I,
\
j
\in
J
_
i
\}
}
{
}
\\
\Infer
[AppLDom]
{
\Gamma
(x
_
1) = t
\\
t
\land
(
\arrow
{
\Empty
}{
\Any
}
)
\neq\Empty\\
t
\land
\neg
(
\arrow
{
\Empty
}{
\Any
}
)
\neq\Empty\\
\Gamma\subst
{
x
_
1
}{
t
\land
(
\arrow
{
\Empty
}{
\Any
}
)
}
\vdash
_
\ct
\ct
[{x_1}{x_2}]
:
\{
(u
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\\
\Gamma\subst
{
x
_
1
}{
t
\land\neg
(
\arrow
{
\Empty
}{
\Any
}
)
}
\vdash
_
\ct
\ct
[{x_1}{x_2}]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
}
\Gamma\subst
{
x
_
1
}{
t
\land
(
\arrow
{
\Empty
}{
\Any
}
)
}
\vdash
_
{
[]
}
\ct
[{x_1}{x_2}]
:
\{
(u
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\\
\Gamma\subst
{
x
_
1
}{
t
\land\neg
(
\arrow
{
\Empty
}{
\Any
}
)
}
\vdash
_
{
[]
}
\ct
[{x_1}{x_2}]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
}
}
{
\Gamma
\vdash
_
\ct
{
x
_
1
}{
x
_
2
}
:
\{
(u
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\cup\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
}}
{
}
...
...
@@ -224,8 +224,8 @@ t\land\neg(\pair{\Any}{\Any})\neq\Empty\\
\\
\Infer
[Case*]
{
\Gamma
(x) = t
_
\circ\\
\Gamma\subst
{
x
}{
t
_
\circ\land
t
}
\vdash
_
\ct
\ct
[\tcase {x} t {e_1}{e_2}]
:
\{
(u
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\\
\Gamma\subst
{
x
}{
t
_
\circ\land\neg
t
}
\vdash
_
\ct
\ct
[\tcase {x} t {e_1}{e_2}]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
}
\Gamma\subst
{
x
}{
t
_
\circ\land
t
}
\vdash
_
{
[]
}
\ct
[\tcase {x} t {e_1}{e_2}]
:
\{
(u
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\\
\Gamma\subst
{
x
}{
t
_
\circ\land\neg
t
}
\vdash
_
{
[]
}
\ct
[\tcase {x} t {e_1}{e_2}]
:
\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
}
}
{
\Gamma\vdash
_
\ct
\tcase
{
x
}
t
{
e
_
1
}{
e
_
2
}
:
\{
(u
_
i,
\Gamma
_
i)
\}
_{
i
\in
I
}
\cup\{
(u
_
j,
\Gamma
_
j)
\}
_{
j
\in
J
}}
{
}
...
...
Write
Preview
Markdown
is supported
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