{ 
tg:Id. srclocs,dstlocs:Id List. l:IdLnk.
((l 
links(tg) from srclocs to dstlocs)
{(source(l) srclocs)
(destination(l) dstlocs)
(lname(l) = tg)}) }
{ Proof }
Definitions occuring in Statement :
links-from-to: links(tg) from srclocs to dstlocs,
lname: lname(l),
ldst: destination(l),
lsrc: source(l),
IdLnk: IdLnk,
Id: Id,
guard: {T},
all: x:A. B[x],
iff: P Q,
and: P Q,
list: type List,
equal: s = t,
l_member: (x l)
Definitions :
tactic: Error :tactic,
CollapseTHEN: Error :CollapseTHEN,
CollapseTHENA: Error :CollapseTHENA,
Unfold: Error :Unfold,
iff: P Q,
and: P Q,
product: x:A 
B[x],
IdLnk: IdLnk,
list: type List,
Id: Id,
all: x:A. B[x],
function: x:A 
B[x],
member: t T,
equal: s = t,
links-from-to: links(tg) from srclocs to dstlocs,
THENM: Error :THENM,
Auto: Error :Auto,
ExRepD: Error :ExRepD,
so_lambda: 
x.t[x],
concat: concat(ll),
apply: f a,
lsrc: source(l),
ldst: destination(l),
lname: lname(l),
rev_implies: P Q,
limited-type: LimitedType,
universe: Type,
prop: 
,
map: map(f;as),
implies: P Q,
combination: Combination(n;T),
listp: A List
,
lambda: x.A[x],
mk_lnk: (link(n) from i to j),
atom: Atom$n,
l_member: (x l),
subtype_rel: A 
r B,
strong-subtype: strong-subtype(A;B),
guard: {T},
exists: 
x:A. B[x],
p-outcome: Outcome,
real: 
,
rationals: 
,
set: {x:A| B[x]} ,
not: 
A,
less_than: a < b,
add: n + m,
natural_number: $n,
nil: [],
int: 
,
subtype: S T,
top: Top,
isect: 
x:A. B[x],
void: Void,
false: False,
length: ||as||,
ge: i 
j ,
le: A 
B,
nat: 
,
cons: [car / cdr],
sqequal: s ~ t,
sq_type: SQType(T),
lsrc_mk_lnk: lsrc_mk_lnk{lsrc_mk_lnk_compseq_tag_def:o}(n; j; i),
ldst_mk_lnk: ldst_mk_lnk{ldst_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),
MaAuto: Error :MaAuto,
select: l[i],
remove-repeats: remove-repeats(eq;L),
last: last(L),
hd: hd(l),
or: P 
Q,
union: left + right,
append: as @ bs,
bool: 
,
pair: <a, b>,
cand: A c B,
D: Error :D,
RepeatFor: Error :RepeatFor,
squash: 
T,
true: True
Lemmas :
true_wf,
squash_wf,
l_member_subtype,
IdLnk_sq,
cons_one_one,
nat_wf,
non_neg_length,
length_wf_nat,
false_wf,
top_wf,
member_wf,
length_wf1,
le_wf,
l_member_wf,
mk_lnk_wf,
map_wf,
guard_wf,
lname_wf,
ldst_wf,
lsrc_wf,
concat_wf,
rev_implies_wf,
iff_wf,
member_map,
and_functionality_wrt_iff,
exists_functionality_wrt_iff,
member-concat,
iff_transitivity,
iff_functionality_wrt_iff,
Id_wf,
IdLnk_wf
\mforall{}tg:Id. \mforall{}srclocs,dstlocs:Id List. \mforall{}l:IdLnk.
((l \mmember{} links(tg) from srclocs to dstlocs)
\mLeftarrow{}{}\mRightarrow{} \{(source(l) \mmember{} srclocs) \mwedge{} (destination(l) \mmember{} dstlocs) \mwedge{} (lname(l) = tg)\})
Date html generated:
2010_08_26-PM-11_34_05
Last ObjectModification:
2009_10_09-PM-05_51_27
Home
Index