Nuprl Lemma : member-rcvs-on
∀tg:Id. ∀links:IdLnk List. ∀k:Knd. ((k ∈ Rcvs(tg) on links) ⇐⇒ (↑isrcv(k)) ∧ (tag(k) = tg ∈ Id) ∧ (lnk(k) ∈ links))
Proof
Definitions occuring in Statement :
rcvs-on: Rcvs(tg) on links,
tagof: tag(k),
lnk: lnk(k),
isrcv: isrcv(k),
Knd: Knd,
IdLnk: IdLnk,
Id: Id,
l_member: (x ∈ l),
list: T List,
assert: ↑b,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
Lemmas :
Knd_wf,
list_wf,
IdLnk_wf,
Id_wf,
member_map,
rcv_wf,
l_member_wf,
map_wf,
iff_wf,
exists_wf,
assert_wf,
isrcv_wf,
tagof_wf,
lnk_wf,
subtype_base_sq,
union_subtype_base,
product_subtype_base,
atom2_subtype_base,
isrcv_rcv_lemma,
tag_rcv_lemma,
lnk_rcv_lemma
\mforall{}tg:Id. \mforall{}links:IdLnk List. \mforall{}k:Knd.
((k \mmember{} Rcvs(tg) on links) \mLeftarrow{}{}\mRightarrow{} (\muparrow{}isrcv(k)) \mwedge{} (tag(k) = tg) \mwedge{} (lnk(k) \mmember{} links))
Date html generated:
2015_07_17-AM-09_12_25
Last ObjectModification:
2015_01_28-AM-07_56_38
Home
Index