Nuprl Lemma : SM1-class-nlp
[Info:{Info:Type| 
Info} ]
S:{S:Type| valueall-type(S)}
[A:Type]
tr:Id 
A S S. X:EClass(A). init:Id bag(S).
(NormalLProgrammable(A;X) 
NormalLProgrammable(S;SM1-class(init;<tr, X>)))
Proof not projected
Definitions occuring in Statement :
SM1-class: SM1-class(init;trX),
normal-locally-programmable: NormalLProgrammable(A;X),
eclass: EClass(A[eo; e]),
Id: Id,
uall: [x:A]. B[x],
all: x:A. B[x],
squash: T,
implies: P Q,
set: {x:A| B[x]} ,
function: x:A B[x],
pair: <a, b>,
universe: Type,
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
SM1-class: SM1-class(init;trX),
nat_plus: 
,
member: t 
T,
prop: 
,
so_lambda: 
x y.t[x; y],
pi2: snd(t),
so_apply: x[s1;s2],
subtype: S 
T
Lemmas :
SM-gen-class-locally-programmable,
int_seg_wf,
normal-locally-programmable_wf,
Id_wf,
bag_wf,
eclass_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
valueall-type_wf,
squash_wf
\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ]
\mforall{}S:\{S:Type| valueall-type(S)\}
\mforall{}[A:Type]
\mforall{}tr:Id {}\mrightarrow{} A {}\mrightarrow{} S {}\mrightarrow{} S. \mforall{}X:EClass(A). \mforall{}init:Id {}\mrightarrow{} bag(S).
(NormalLProgrammable(A;X) {}\mRightarrow{} NormalLProgrammable(S;SM1-class(init;<tr, X>)))
Date html generated:
2011_10_20-PM-04_05_47
Last ObjectModification:
2011_08_22-PM-02_10_34
Home
Index