Nuprl Lemma : until-class-locally-programmable
[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 :
uall: [x:A]. B[x],
squash: T,
all: x:A. B[x],
implies: P Q,
normal-locally-programmable: NormalLProgrammable(A;X),
member: t 
T,
prop: 
,
so_apply: x[s],
so_lambda: 
x.t[x],
so_apply: x[s1;s2],
so_lambda: x y.t[x; y],
subtype: S 
T,
top: Top,
sq_exists: 
x:{A| B[x]},
spreadn: spread4,
suptype: suptype(S; T),
df-program-type: df-program-type(dfp),
pi1: fst(t),
true: True,
local-program-at: local-program-at{i:l}(Info;A;X;dfp;x),
until-prog: until-prog(A;S;T;sx;sy;nxtx;nxty),
and: P 
Q,
cand: A c B,
not: 
A,
assert: 
b,
bfalse: ff,
ifthenelse: if b then t else f fi ,
exists: x:A. B[x],
pi2: snd(t),
spreadn: spread3,
until-class-lpg1-ext,
df-program-statetype: df-program-statetype(dfp),
df-prog-equiv: df-prog-equiv(A;p;q;s1,s2.R[s1; s2]),
bag-null: bag-null(bs),
or: P 
Q,
isl: isl(x),
df-program-state: df-program-state(dfp),
evalall: evalall(t),
df-program-in-state-ap': df-program-in-state-ap'(dfp;s;m),
btrue: tt,
df-program-in-state-ap: df-program-in-state-ap(dfp;s;m),
outl: outl(x),
null: null(as),
false: False,
unit: Unit,
has-valueall: has-valueall(a),
guard: {T},
lt_int: i <z j,
bag-size: bag-size(bs),
eq_int: (i =
j),
it: 
,
empty-bag: {},
exposed-bfalse: exposed-bfalse,
uiff: uiff(P;Q),
bool: 
,
le: A 
B,
uimplies: b supposing a,
dataflow-program: DataflowProgram(A),
sq_type: SQType(T),
sq_stable: SqStable(P),
nat: 
,
ycomb: Y,
length: ||as||,
rev_uimplies: rev_uimplies(P;Q),
decidable: Dec(P)
Lemmas :
uall_wf,
squash_wf,
all_wf,
eclass_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
normal-locally-programmable_wf,
until-class_wf,
es-interface-subtype_rel2,
top_wf,
equal_wf,
dataflow-program_wf,
until-prog_wf,
df-program-type_wf,
subtype_rel-equal,
bag_wf,
subtype_rel_dep_function,
unit_wf2,
subtype_rel_self,
subtype_rel_simple_product,
subtype_rel_bag,
subtype_top,
Id_wf,
local-program-at_wf,
valueall-type_wf,
true_wf,
last_wf,
not_wf,
assert_wf,
null_wf3,
data-stream_wf,
dataflow_wf,
map_wf,
es-loc_wf,
es-info_wf,
es-le-before_wf,
null-data-stream,
null-map,
es-le-before_wf2,
es-le_wf,
es-le-before-not-null,
subtype_base_sq,
bool_wf,
bool_subtype_base,
false_wf,
bfalse_wf,
df-program-meaning-equal,
and_wf,
isl_wf,
or_wf,
bag-null_wf,
empty-bag_wf,
ifthenelse_wf,
it_wf,
product-valueall-type,
union-valueall-type,
sq_stable__valueall-type,
equal-valueall-type,
bag-valueall-type,
bag-size_wf,
nat_wf,
pi1_wf_top,
pi2_wf,
bnot_wf,
bool_cases,
uiff_transitivity,
eqtt_to_assert,
assert-bag-null,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff,
outl_wf,
equal-empty-bag,
assert_of_le_int,
bnot_of_lt_int,
assert_functionality_wrt_uiff,
assert_of_lt_int,
le_wf,
le_int_wf,
less_than_wf,
lt_int_wf,
empty-bag-iff-size,
assert_of_eq_int,
eq_int_wf,
int-valueall-type,
isect-valueall-type,
list-valueall-type,
btrue_wf,
decidable__assert,
decidable__not,
not_assert_elim,
df-program-statetype_wf,
df-prog-equiv_wf
\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_01_23-PM-12_33_03
Last ObjectModification:
2012_01_06-AM-10_39_55
Home
Index