Nuprl Lemma : parallel-class-locally-programmable-ext
[Info:{Info:Type| 
Info} ]
A:{A:Type| valueall-type(A)}
[X,Y:EClass(A)]. (NormalLProgrammable(A;X) 
NormalLProgrammable(A;Y) NormalLProgrammable(A;X || Y))
Proof not projected
Definitions occuring in Statement :
normal-locally-programmable: NormalLProgrammable(A;X),
parallel-class: X || Y,
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
all: x:A. B[x],
squash: T,
implies: P Q,
set: {x:A| B[x]} ,
universe: Type,
valueall-type: valueall-type(T)
Definitions :
member: t 
T,
select-tuple: x.n,
parallel-df-program-case1: parallel-df-program-case1(B;F;dfps),
bag-append: as + bs,
parallel-class-locally-programmable,
upto: upto(n),
parallel-df-prog: parallel-df-prog,
bl-all: (xL.P[x])_b,
bnot: 
b,
isl: isl(x),
length: ||as||,
ycomb: Y,
from-upto: [n, m),
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
btrue: tt,
bfalse: ff,
tuple-type: tuple-type(L),
map: map(f;as),
tuple: tuple(n;i.F[i]),
select: l[i],
spreadn: spread4,
empty-bag: {},
it: 
,
ap2-tuple: ap2-tuple(len;f;x;t),
evalall: evalall(t),
map-tuple: map-tuple(len;f;t),
pi1: fst(t),
pi2: snd(t),
null: null(as),
le_int: i 
z j,
band: p 
q,
reduce: reduce(f;k;as),
eq_int: (i =
j),
append: as @ bs,
spreadn: spread3
Lemmas :
parallel-class-locally-programmable,
subtype_base_sq,
parallel-class_wf,
normal-locally-programmable_wf,
eclass_wf,
uall_wf,
valueall-type_wf,
squash_wf,
isect_subtype_base
\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ]
\mforall{}A:\{A:Type| valueall-type(A)\}
\mforall{}[X,Y:EClass(A)].
(NormalLProgrammable(A;X) {}\mRightarrow{} NormalLProgrammable(A;Y) {}\mRightarrow{} NormalLProgrammable(A;X || Y))
Date html generated:
2011_10_20-PM-03_24_59
Last ObjectModification:
2011_09_22-PM-01_11_01
Home
Index