Nuprl Lemma : rcvs-on-links-from-to
∀tg1,tg2:Id. ∀srclocs,dstlocs:Id List.
(∀d∈dstlocs.(∀s∈srclocs.(∃k∈Rcvs(tg1) on links(tg2) from srclocs to dstlocs. (source(lnk(k)) = s ∈ Id)
∧ (destination(lnk(k)) = d ∈ Id))))
Proof
Definitions occuring in Statement :
rcvs-on: Rcvs(tg) on links,
links-from-to: links(tg) from srclocs to dstlocs,
ldst: destination(l),
lsrc: source(l),
lnk: lnk(k),
Id: Id,
l_exists: (∃x∈L. P[x]),
l_all: (∀x∈L.P[x]),
list: T List,
all: ∀x:A. B[x],
and: P ∧ Q,
equal: s = t ∈ T
Lemmas :
assert_wf,
isrcv_wf,
l_member_wf,
lsrc_wf,
lnk_wf,
assert_elim,
subtype_base_sq,
bool_wf,
bool_subtype_base,
ldst_wf,
l_exists_iff,
set_wf,
l_all_iff,
l_exists_wf,
Knd_wf,
rcvs-on_wf,
links-from-to_wf,
l_all_wf2,
all_wf,
exists_wf,
list_wf,
Id_wf,
tag_rcv_lemma,
member-links-from-to,
rcv_wf,
mk_lnk_wf,
member-rcvs-on,
IdLnk_wf,
lname_wf,
lnk_rcv_lemma,
lsrc_mk_lnk_lemma,
ldst_mk_lnk_lemma,
lname_mk_lnk_lemma,
l_member-settype
\mforall{}tg1,tg2:Id. \mforall{}srclocs,dstlocs:Id List.
(\mforall{}d\mmember{}dstlocs.(\mforall{}s\mmember{}srclocs.(\mexists{}k\mmember{}Rcvs(tg1) on links(tg2) from srclocs to dstlocs. (source(lnk(k)) = s)
\mwedge{} (destination(lnk(k)) = d))))
Date html generated:
2015_07_17-AM-09_12_27
Last ObjectModification:
2015_01_28-AM-07_58_13
Home
Index