Nuprl Lemma : SM2-class-nlp
[Info:{Info:Type| 
Info} ]
S:{S:Type| valueall-type(S)}
[A,B:Type].
tr1:Id 
A S S. X1:EClass(A). tr2:Id B S S. X2:EClass(B). init:Id bag(S).
(NormalLProgrammable(A;X1)
NormalLProgrammable(B;X2)
NormalLProgrammable(S;SM2-class(init;<tr1, X1>;<tr2, X2>)))
Proof not projected
Definitions occuring in Statement :
SM2-class: SM2-class(init;trX1;trX2),
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,
SM2-class: SM2-class(init;trX1;trX2),
ifthenelse: if b then t else f fi ,
eq_int: (i =
j),
nat_plus: 
,
int_seg: {i..j
},
pi2: snd(t),
member: t 
T,
lelt: i 
j < k,
btrue: tt,
bfalse: ff,
prop: 
,
and: P 
Q,
subtype: S 
T,
suptype: suptype(S; T),
exists: 
x:A. B[x],
false: False,
so_lambda: 
x y.t[x; y],
bool: 
,
decidable: Dec(P),
or: P 
Q,
not: 
A,
sq_type: SQType(T),
uimplies: b supposing a,
guard: {T},
unit: Unit,
uiff: uiff(P;Q),
le: A B,
so_apply: x[s1;s2],
it: 
Lemmas :
SM-gen-class-locally-programmable,
ifthenelse_wf,
eq_int_wf,
int_seg_wf,
decidable__equal_int,
subtype_base_sq,
int_subtype_base,
bfalse_wf,
bool_wf,
uiff_transitivity,
assert_wf,
eqtt_to_assert,
assert_of_eq_int,
bnot_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff,
le_wf,
int_seg_properties,
btrue_wf,
Id_wf,
normal-locally-programmable_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,B:Type].
\mforall{}tr1:Id {}\mrightarrow{} A {}\mrightarrow{} S {}\mrightarrow{} S. \mforall{}X1:EClass(A). \mforall{}tr2:Id {}\mrightarrow{} B {}\mrightarrow{} S {}\mrightarrow{} S. \mforall{}X2:EClass(B).
\mforall{}init:Id {}\mrightarrow{} bag(S).
(NormalLProgrammable(A;X1)
{}\mRightarrow{} NormalLProgrammable(B;X2)
{}\mRightarrow{} NormalLProgrammable(S;SM2-class(init;<tr1, X1><tr2, X2>)))
Date html generated:
2011_10_20-PM-04_05_58
Last ObjectModification:
2011_08_22-PM-02_24_58
Home
Index