Nuprl Lemma : Threshold-Combinator-locally-programmable
S:{S:
'| valueall-type(S)}
[A:']
B:{B:'| valueall-type(B)}
[X:EClass'(A)]
R:A 
S 
. init_state:Id bag(S). accum:A S S. f:Id A S bag(B).
(NormalLProgrammable'(A;X) 
NormalLProgrammable'(B;Threshold-Combinator(R;X;init_state;accum;f)))
Proof not projected
Definitions occuring in Statement :
Threshold-Combinator: Threshold-Combinator(R;X;init_state;accum;f),
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
eclass: EClass(A[eo; e]),
Id: Id,
bool: ,
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
set: {x:A| B[x]} ,
function: x:A B[x],
universe: Type,
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
all: x:A. B[x],
uall: [x:A]. B[x],
eclass: EClass(A[eo; e]),
implies: P Q,
Threshold-Combinator: Threshold-Combinator(R;X;init_state;accum;f),
let: let,
member: t 
T,
or: P 
Q,
squash: 
T,
and: P 
Q,
concat-lifting-loc-2: f@Loc,
ifthenelse: if b then t else f fi ,
guard: {T},
concat-lifting2-loc: concat-lifting2-loc(f;abag;bbag;loc),
concat-lifting-loc: concat-lifting-loc(n;bags;loc;f),
select: l[i],
concat-lifting: concat-lifting(n;f;bags),
concat-lifting-list: concat-lifting-list(n;bags),
lifting-gen-list-rev: lifting-gen-list-rev(n;bags),
ycomb: Y,
eq_int: (i =
j),
btrue: tt,
bfalse: ff,
le_int: i 
z j,
bnot: 
b,
lt_int: i <z j,
true: True,
prop: 
,
so_lambda: 
x.t[x],
cand: A c B,
so_apply: x[s],
subtype: S 
T
Lemmas :
simple-loc-comb-2-nlp,
concat-lifting-loc-2_wf,
ifthenelse_wf,
bag_wf,
empty-bag_wf,
Id_wf,
primed-class-opt_wf,
Accum-class_wf,
normal-locally-programmable_wf,
Message_wf,
bool_wf,
event-ordering+_wf,
es-E_wf,
event-ordering+_inc,
valueall-type_wf,
squash_wf,
all_wf,
equal_wf,
Accum-class-locally-programmable,
primed-class-opt-nlp
\mforall{}S:\{S:\mBbbU{}'| valueall-type(S)\}
\mforall{}[A:\mBbbU{}']
\mforall{}B:\{B:\mBbbU{}'| valueall-type(B)\}
\mforall{}[X:EClass'(A)]
\mforall{}R:A {}\mrightarrow{} S {}\mrightarrow{} \mBbbB{}. \mforall{}init$_{state}$:Id {}\mrightarrow{} bag(S). \mforall{}accum:A {}\mrightarrow{} S {}\mrightarrow{} S. \mforall{}f:Id \000C{}\mrightarrow{} A {}\mrightarrow{} S {}\mrightarrow{} bag(B).
(NormalLProgrammable'(A;X)
{}\mRightarrow{} NormalLProgrammable'(B;Threshold-Combinator(R;X;init$_{state}$;accu\000Cm;f)))
Date html generated:
2012_01_23-PM-01_05_26
Last ObjectModification:
2011_12_30-PM-08_13_11
Home
Index