Nuprl Lemma : locknd_wf
∀[i:Id]. ∀[k:Knd]. (locknd(i;k) ∈ LocKnd)
Proof
Definitions occuring in Statement :
locknd: locknd(i;k),
LocKnd: LocKnd,
Knd: Knd,
Id: Id,
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas :
kindcase_wf,
Id_wf,
ldst_wf,
IdLnk_wf,
assert-hasloc,
rcv_wf,
lnk_rcv_lemma,
assert_wf,
isrcv_wf,
locl_wf,
isrcv_locl_lemma,
hasloc_wf,
Knd_wf
\mforall{}[i:Id]. \mforall{}[k:Knd]. (locknd(i;k) \mmember{} LocKnd)
Date html generated:
2015_07_17-AM-09_14_41
Last ObjectModification:
2015_01_28-AM-07_54_21
Home
Index