{ 
tg1,tg2:Id. srclocs,dstlocs:Id List.
(d
dstlocs.
(ssrclocs.
(
kRcvs(tg1) on links(tg2) from srclocs to dstlocs. (source(lnk(k))
= s)
(destination(lnk(k)) = d)))) }
{ 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),
isrcv: isrcv(k),
Knd: Knd,
Id: Id,
assert: 
b,
all: x:A. B[x],
and: P Q,
set: {x:A| B[x]} ,
list: type List,
equal: s = t,
l_exists: (xL. P[x]),
l_all: (xL.P[x])
Definitions :
member: t T,
l_member: (x l),
Id: Id,
set: {x:A| B[x]} ,
equal: s = t,
assert: b,
Knd: Knd,
function: x:A 
B[x],
all: x:A. B[x],
isrcv: isrcv(k),
list: type List,
lnk: lnk(k),
lsrc: source(l),
bool: 
,
implies: P 
Q,
exists: x:A. B[x],
btrue: tt,
true: True,
guard: {T},
sq_type: SQType(T),
product: x:A 
B[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
atom: Atom$n,
isl: isl(x),
IdLnk: IdLnk,
ldst: destination(l),
universe: Type,
cand: A c B,
and: P Q,
links-from-to: links(tg) from srclocs to dstlocs,
rcvs-on: Rcvs(tg) on links,
prop: 
,
less_than: a < b,
ldst_mk_lnk: ldst_mk_lnk{ldst_mk_lnk_compseq_tag_def:o}(n; j; i),
lnk_rcv: lnk_rcv{lnk_rcv_compseq_tag_def:o}(tg; l),
lsrc_mk_lnk: lsrc_mk_lnk{lsrc_mk_lnk_compseq_tag_def:o}(n; j; i),
lname_mk_lnk: lname_mk_lnk{lname_mk_lnk_compseq_tag_def:o}(n; j; i),
isrcv_rcv: isrcv_rcv{isrcv_rcv_compseq_tag_def:o}(tg; l),
tag_rcv: tag_rcv{tag_rcv_compseq_tag_def:o}(tg; l),
append: as @ bs,
union: left + right,
or: P 
Q,
cons: [car / cdr],
rev_implies: P 
Q,
iff: P Q,
so_lambda: 
x.t[x],
map: map(f;as),
hd: hd(l),
last: last(L),
remove-repeats: remove-repeats(eq;L),
select: l[i],
strong-subtype: strong-subtype(A;B),
subtype_rel: A 
r B,
nat: 
,
l_exists: (xL. P[x]),
l_all: (xL.P[x]),
MaAuto: Error :MaAuto,
mk_lnk: (link(n) from i to j),
rcv: rcv(l,tg),
CollapseTHEN: Error :CollapseTHEN,
Auto: Error :Auto,
D: Error :D,
RepeatFor: Error :RepeatFor,
tactic: Error :tactic,
tagof: tag(k),
lname: lname(l),
limited-type: LimitedType,
subtype: S T,
void: Void,
lambda: x.A[x]
Lemmas :
iff_transitivity,
member-rcvs-on,
and_functionality_wrt_iff,
iff_wf,
rev_implies_wf,
member-links-from-to,
member_wf,
Id_sq,
lname_wf,
tagof_wf,
btrue_wf,
guard_wf,
IdLnk_wf,
l_all_wf,
l_exists_wf,
l_member-settype,
l_member_subtype,
rcv_wf,
mk_lnk_wf,
l_member_wf,
Knd_wf,
rcvs-on_wf,
links-from-to_wf,
lsrc_wf,
Id_wf,
ldst_wf,
lnk_wf,
assert_wf,
bool_sq,
assert_elim,
isrcv_wf
\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:
2011_08_10-AM-07_46_47
Last ObjectModification:
2010_09_24-PM-09_19_51
Home
Index