Nuprl Lemma : once-once-class
[Info,A:Type]. [X:EClass(A)]. (once-class(once-class(X)) = once-class(X))
Proof not projected
Definitions occuring in Statement :
once-class: once-class(X),
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
eclass: EClass(A[eo; e]),
once-class: once-class(X),
until-class: (X until Y),
member: t 
T,
all: x:A. B[x],
so_lambda: 
x y.t[x; y],
implies: P 
Q,
prop: 
,
false: False,
so_apply: x[s1;s2],
or: P 
Q,
and: P 
Q,
existse-before: 
e<e'.P[e],
exists: x:A. B[x],
cand: A c B,
squash: 
T,
alle-lt: e<e'.P[e],
iff: P 
Q,
not: 
A,
subtype: S 
T,
guard: {T}
Lemmas :
es-E_wf,
event-ordering+_inc,
class-pred_wf,
until-class_wf,
top_wf,
es-interface-top,
empty-bag_wf,
eclass_wf,
event-ordering+_wf,
class-pred-cases,
bag_wf,
until-classrel
\mforall{}[Info,A:Type]. \mforall{}[X:EClass(A)]. (once-class(once-class(X)) = once-class(X))
Date html generated:
2011_10_20-PM-03_22_06
Last ObjectModification:
2011_08_15-PM-04_51_59
Home
Index