{ 
t:
. A:Id List.
(
W:Id List List
((ws:Id List
((ws 
W)
(||ws|| = (t + 1)) 
no_repeats(Id;ws) (xws.(x A))))
(ws1W.(ws2W.a:Id. ((a ws1) (a ws2)))))) supposing
(no_repeats(Id;A) and
(||A|| = ((2 * t) + 1))) }
{ Proof }
Definitions occuring in Statement :
Id: Id,
length: ||as||,
nat: ,
uimplies: b supposing a,
all: x:A. B[x],
exists: x:A. B[x],
iff: P Q,
and: P Q,
list: type List,
multiply: n * m,
add: n + m,
natural_number: $n,
int: 
,
equal: s = t,
l_all: (xL.P[x]),
no_repeats: no_repeats(T;l),
l_member: (x l)
Definitions :
all: x:A. B[x],
iff: P Q,
and: P Q,
implies: P Q,
rev_implies: P Q,
member: t T,
prop: 
,
subtype: S 
T,
so_lambda: 
x.t[x],
Id: Id,
l_all: (xL.P[x]),
le: A 
B,
not: 
A,
false: False,
squash: 
T,
true: True,
cand: A c B,
l_member: (x l),
exists: x:A. B[x],
no_repeats: no_repeats(T;l),
uall: [x:A]. B[x],
uimplies: b supposing a,
int_seg: {i..j
},
lelt: i j < k,
nat: ,
so_apply: x[s],
sq_type: SQType(T),
guard: {T},
sq_stable: SqStable(P),
two-intersection: two-intersection(A;W)
Lemmas :
l_member_wf,
length_wf1,
no_repeats_wf,
l_all_wf2,
Id_wf,
subtype_base_sq,
list_subtype_base,
atom2_subtype_base,
select_wf,
sq_stable_from_decidable,
decidable__l_member,
decidable__equal_Id,
list-set-type2,
list-equal-set2,
nat_wf,
not_wf,
select_member,
le_wf,
l_member-settype
\mforall{}t:\mBbbN{}. \mforall{}A:Id List.
(\mexists{}W:Id List List
((\mforall{}ws:Id List. ((ws \mmember{} W) \mLeftarrow{}{}\mRightarrow{} (||ws|| = (t + 1)) \mwedge{} no\_repeats(Id;ws) \mwedge{} (\mforall{}x\mmember{}ws.(x \mmember{} A))))
\mwedge{} (\mforall{}ws1\mmember{}W.(\mforall{}ws2\mmember{}W.\mexists{}a:Id. ((a \mmember{} ws1) \mwedge{} (a \mmember{} ws2)))))) supposing
(no\_repeats(Id;A) and
(||A|| = ((2 * t) + 1)))
Date html generated:
2011_08_16-AM-10_00_44
Last ObjectModification:
2011_06_18-AM-08_58_35
Home
Index