Nuprl Lemma : parallel-class-loc-bounded
[T,Info:Type]. [X,Y:EClass(T)]. (LocBounded(T;X) 
LocBounded(T;Y) LocBounded(T;X || Y))
Proof not projected
Definitions occuring in Statement :
parallel-class: X || Y,
loc-bounded-class: LocBounded(T;X),
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
implies: P Q,
universe: Type
Definitions :
so_lambda: 
x y.t[x; y],
so_lambda: x.t[x],
prop: 
,
true: True,
squash: 
T,
sq_or: a 
b,
member: t 
T,
bag-member: x bs,
all: x:A. B[x],
class-loc-bound: class-loc-bound{i:l}(Info;T;X;L),
exists: 
x:A. B[x],
loc-bounded-class: LocBounded(T;X),
implies: P Q,
uall: [x:A]. B[x],
or: P Q,
so_apply: x[s1;s2],
so_apply: x[s],
iff: P 
Q,
rev_implies: P Q,
sq_stable: SqStable(P),
and: P 
Q,
uiff: uiff(P;Q),
uimplies: b supposing a,
subtype: S 
T
Lemmas :
event-ordering+_wf,
eclass_wf,
loc-bounded-class_wf,
bag-member_wf,
all_wf,
event-ordering+_inc,
es-E_wf,
parallel-class_wf,
classrel_wf,
bag-member-append,
es-loc_wf,
sq_stable__bag-member,
parallel-classrel,
Id_wf,
bag-append_wf
\mforall{}[T,Info:Type]. \mforall{}[X,Y:EClass(T)]. (LocBounded(T;X) {}\mRightarrow{} LocBounded(T;Y) {}\mRightarrow{} LocBounded(T;X || Y))
Date html generated:
2012_01_23-PM-12_23_31
Last ObjectModification:
2011_12_13-PM-01_36_45
Home
Index