Nuprl Lemma : decidable__exists-single-valued-bag
[T:Type]. b:bag(T). (single-valued-bag(b;T) 
Dec(
v:T. v 
b))
Proof not projected
Definitions occuring in Statement :
decidable: Dec(P),
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
universe: Type,
single-valued-bag: single-valued-bag(b;T),
bag-member: x bs,
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
decidable: Dec(P),
member: t T,
or: P 
Q,
not: 
A,
so_lambda: 
x.t[x],
guard: {T},
exists: x:A. B[x],
nat: 
,
so_apply: x[s],
false: False,
uimplies: b supposing a,
prop: 
Lemmas :
decidable__lt,
bag-size_wf,
nat_wf,
not_wf,
exists_wf,
bag-member_wf,
single-valued-bag_wf,
bag_wf,
sv-bag-only_wf,
bag-member-sv-bag-only,
bag-member-size
\mforall{}[T:Type]. \mforall{}b:bag(T). (single-valued-bag(b;T) {}\mRightarrow{} Dec(\mexists{}v:T. v \mdownarrow{}\mmember{} b))
Date html generated:
2012_01_23-PM-12_18_33
Last ObjectModification:
2012_01_18-AM-03_08_13
Home
Index