Nuprl Lemma : decidable__classrel
[Info,T:Type]. ((x,y:T. Dec(x = y)) 
(X:EClass(T). es:EO+(Info). e:E. v:T. Dec(v 
X(e))))
Proof not projected
Definitions occuring in Statement :
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],
implies: P Q,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
implies: P Q,
all: x:A. B[x],
eclass: EClass(A[eo; e]),
classrel: v X(e),
member: t T,
so_lambda: 
x y.t[x; y],
prop: 
,
so_apply: x[s1;s2],
subtype: S 
T
Lemmas :
decidable__bag-member,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
eclass_wf,
decidable_wf
\mforall{}[Info,T:Type].
((\mforall{}x,y:T. Dec(x = y)) {}\mRightarrow{} (\mforall{}X:EClass(T). \mforall{}es:EO+(Info). \mforall{}e:E. \mforall{}v:T. Dec(v \mmember{} X(e))))
Date html generated:
2011_10_20-PM-03_18_31
Last ObjectModification:
2011_08_22-PM-05_35_48
Home
Index