Lvc.Coherence.DelocationValidator
Require
Import
AllInRel
Util
Map
Env
EnvTy
Exp
IL
Annotation
Coherence
Bisim
DecSolve
Liveness
Restrict
Delocation
.
Set Implicit Arguments
.
Lemma
trs_dec
DL
ZL
s
ans_lv
ans
:
{
trs
DL
ZL
s
ans_lv
ans
}
+
{
¬
trs
DL
ZL
s
ans_lv
ans
}
.
Instance
trs_dec_inst
DL
ZL
s
lv
Y
:
Computable
(
trs
DL
ZL
s
lv
Y
).