Nuprl Lemma : assert-hasloc
∀[i:Id]. ∀[k:Knd]. uiff(↑hasloc(k;i);destination(lnk(k)) = i ∈ Id supposing ↑isrcv(k))
Proof
Definitions occuring in Statement :
hasloc: hasloc(k;i),
ldst: destination(l),
lnk: lnk(k),
isrcv: isrcv(k),
Knd: Knd,
Id: Id,
assert: ↑b,
uiff: uiff(P;Q),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Lemmas :
assert_wf,
isrcv_wf,
hasloc_wf,
assert_witness,
isect_wf,
equal_wf,
Id_wf,
ldst_wf,
lnk_wf,
Knd_wf,
bnot_wf,
eq_id_wf,
not_wf,
iff_transitivity,
iff_weakening_uiff,
assert_of_bnot,
assert-eq-id,
decidable__equal_Id
\mforall{}[i:Id]. \mforall{}[k:Knd]. uiff(\muparrow{}hasloc(k;i);destination(lnk(k)) = i supposing \muparrow{}isrcv(k))
Date html generated:
2015_07_17-AM-09_13_59
Last ObjectModification:
2015_01_28-AM-07_55_24
Home
Index