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