{ 
p,q:IdLnk List. i,j,k:Id.
(
r:IdLnk List. lconnects(r;i;k)) supposing
(lconnects(q;j;k) and
lconnects(p;i;j)) }
{ Proof }
Definitions occuring in Statement :
lconnects: lconnects(p;i;j),
IdLnk: IdLnk,
Id: Id,
uimplies: b supposing a,
all: x:A. B[x],
exists: x:A. B[x],
list: type List
Definitions :
all: x:A. B[x],
member: t 
T,
uimplies: b supposing a,
lconnects: lconnects(p;i;j),
exists: x:A. B[x],
and: P 
Q,
lpath: lpath(p),
implies: P 
Q,
not: 
A,
false: False,
le: A 
B,
prop: 
,
squash: 
T,
true: True,
top: Top,
subtype: S 
T,
length: ||as||,
ycomb: Y,
hd: hd(l),
IdLnk: IdLnk,
Id: Id,
so_lambda: 
x.t[x],
iff: P 
Q,
assert: 
b,
null: null(as),
bfalse: ff,
ifthenelse: if b then t else f fi ,
rev_implies: P Q,
last: last(L),
select: l[i],
le_int: i z j,
bnot: 
b,
lt_int: i <z j,
btrue: tt,
int_seg: {i..j
},
uall: [x:A]. B[x],
lelt: i j < k,
sq_type: SQType(T),
so_apply: x[s],
guard: {T},
decidable: Dec(P),
or: P 
Q
Lemmas :
IdLnk_wf,
select_wf,
length_wf2,
lnk-inv_wf,
int_seg_wf,
not_wf,
length_wf1,
lconnects_wf,
squash_wf,
true_wf,
Id_wf,
non_neg_length,
length_wf_nat,
top_wf,
ldst_wf,
subtype_base_sq,
product_subtype_base,
atom2_subtype_base,
last_cons,
false_wf,
decidable__equal_IdLnk,
ldst-inv
\mforall{}p,q:IdLnk List. \mforall{}i,j,k:Id.
(\mexists{}r:IdLnk List. lconnects(r;i;k)) supposing (lconnects(q;j;k) and lconnects(p;i;j))
Date html generated:
2011_08_10-AM-07_48_28
Last ObjectModification:
2011_06_18-AM-08_13_07
Home
Index