Nuprl Lemma : local_or_rcv
∀k:Knd. ((↑islocal(k)) ∨ (↑isrcv(k)))
Proof
Definitions occuring in Statement :
islocal: islocal(k),
isrcv: isrcv(k),
Knd: Knd,
assert: ↑b,
all: ∀x:A. B[x],
or: P ∨ Q
Lemmas :
IdLnk_wf,
Id_wf,
false_wf
\mforall{}k:Knd. ((\muparrow{}islocal(k)) \mvee{} (\muparrow{}isrcv(k)))
Date html generated:
2015_07_17-AM-09_11_50
Last ObjectModification:
2015_01_28-AM-07_57_03
Home
Index