Nuprl Lemma : decidable__exists_bag-member
∀[T:Type]. ∀b:bag(T). Dec(↓∃x:T. x ↓∈ b)
Proof
Definitions occuring in Statement :
decidable: Dec(P),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
universe: Type,
bag-member: x ↓∈ bs,
bag: bag(T)
Lemmas :
decidable__lt,
bag-size_wf,
nat_wf,
bag-size-bag-member,
not_wf,
squash_wf,
exists_wf,
bag-member_wf,
bag_wf
\mforall{}[T:Type]. \mforall{}b:bag(T). Dec(\mdownarrow{}\mexists{}x:T. x \mdownarrow{}\mmember{} b)
Date html generated:
2015_07_17-PM-00_17_56
Last ObjectModification:
2015_01_28-AM-00_02_51
Home
Index