{ 
[p:IdLnk List]. [i:
||p||]. [j:i + 1].
lconnects(l_interval(p;j;i);source(p[j]);source(p[i])) supposing lpath(p) }
{ Proof }
Definitions occuring in Statement :
lconnects: lconnects(p;i;j),
lpath: lpath(p),
lsrc: source(l),
IdLnk: IdLnk,
select: l[i],
length: ||as||,
int_seg: {i..j
},
uimplies: b supposing a,
uall: [x:A]. B[x],
list: type List,
add: n + m,
natural_number: $n,
l_interval: l_interval(l;j;i)
Definitions :
uall: [x:A]. B[x],
int_seg: {i..j},
uimplies: b supposing a,
lpath: lpath(p),
lconnects: lconnects(p;i;j),
member: t 
T,
and: P 
Q,
implies: P 
Q,
not: 
A,
all: x:A. B[x],
false: False,
le: A 
B,
lelt: i j < k,
prop: 
,
true: True,
rev_implies: P 
Q,
iff: P Q,
squash: 
T,
Id: Id,
sq_type: SQType(T),
guard: {T}
Lemmas :
IdLnk_wf,
select_wf,
l_interval_wf,
length_wf1,
le_wf,
lnk-inv_wf,
int_seg_wf,
not_wf,
lpath_wf,
Id_wf,
ldst_wf,
length_l_interval,
squash_wf,
true_wf,
select_l_interval,
lsrc_wf,
subtype_base_sq,
int_subtype_base,
hd_l_interval,
last_l_interval,
atom2_subtype_base
\mforall{}[p:IdLnk List]. \mforall{}[i:\mBbbN{}||p||]. \mforall{}[j:\mBbbN{}i + 1].
lconnects(l\_interval(p;j;i);source(p[j]);source(p[i])) supposing lpath(p)
Date html generated:
2011_08_10-AM-07_47_07
Last ObjectModification:
2011_06_18-AM-08_12_31
Home
Index