Nuprl Lemma : until-class-locally-programmable-ext
[Info:{Info:Type| 
Info} ]
A,B:{B:Type| valueall-type(B)} .
[X:EClass(A)]. [Y:EClass(B)].
(NormalLProgrammable(A;X) 
NormalLProgrammable(B;Y) NormalLProgrammable(A;(X until Y)))
Proof not projected
Definitions occuring in Statement :
normal-locally-programmable: NormalLProgrammable(A;X),
until-class: (X until 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 :
null: null(as),
bfalse: ff,
btrue: tt,
it: 
,
bag-null: bag-null(bs),
ifthenelse: if b then t else f fi ,
empty-bag: {},
evalall: evalall(t),
unit: Unit,
until-class-locally-programmable,
until-prog: until-prog(A;S;T;sx;sy;nxtx;nxty),
spreadn: spread4,
member: t 
T
Lemmas :
isect_subtype_base,
all_wf,
uall_wf,
normal-locally-programmable_wf,
until-class_wf,
eclass_wf,
valueall-type_wf,
squash_wf,
subtype_base_sq,
until-class-locally-programmable
\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ]
\mforall{}A,B:\{B:Type| valueall-type(B)\} .
\mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)].
(NormalLProgrammable(A;X) {}\mRightarrow{} NormalLProgrammable(B;Y) {}\mRightarrow{} NormalLProgrammable(A;(X until Y)))
Date html generated:
2012_02_20-PM-02_49_23
Last ObjectModification:
2012_01_31-PM-05_33_14
Home
Index