Nuprl Lemma : decidable__exists-single-valued-classrel

[Info,T:Type].

X:EClass(T).

es:EO+(Info). (single-valued-classrel(es;X;T)

(

e:E. Dec(

v:T. v

X(e))))

Proof not projected

Definitions occuring in Statement : single-valued-classrel: single-valued-classrel(es;X;T), classrel: v

X(e), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-E: E, decidable: Dec(P), uall:

[x:A]. B[x], all:

x:A. B[x], exists:

x:A. B[x], implies: P

Q, universe: Type
Definitions : uall:

[x:A]. B[x], all:

x:A. B[x], eclass: EClass(A[eo; e]), implies: P

Q, decidable: Dec(P), classrel: v

X(e), member: t

T, or: P

Q, not:

A, so_lambda:

x.t[x], guard: {T}, so_lambda:

x y.t[x; y], exists:

x:A. B[x], squash:

T, true: True, single-valued-classrel: single-valued-classrel(es;X;T), nat:

, so_apply: x[s], false: False, so_apply: x[s1;s2], uimplies: b supposing a, iff: P

Q, and: P

Q, rev_implies: P

Q, prop:

, subtype: S

T, single-valued-bag: single-valued-bag(b;T)
Lemmas : decidable__lt, bag-size_wf, nat_wf, not_wf, exists_wf, bag-member_wf, es-E_wf, event-ordering+_inc, single-valued-classrel_wf, event-ordering+_wf, eclass_wf, sv-bag-only_wf, bag-member-sv-bag-only, bag-size-bag-member

\mforall{}[Info,T:Type]. \mforall{}X:EClass(T). \mforall{}es:EO+(Info). (single-valued-classrel(es;X;T) {}\mRightarrow{} (\mforall{}e:E. Dec(\mexists{}v:T. v \mmember{} X(e)))) Date html generated: 2012_01_23-PM-12_18_41 Last ObjectModification: 2012_01_10-PM-06_53_43 Home Index