Nuprl Lemma : ler2_Nbr_nlp
NormalLProgrammable'(
Id;ler2_Nbr())
Proof not projected
Definitions occuring in Statement :
ler2_Nbr: ler2_Nbr(),
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
Id: Id,
product: x:A B[x],
int:
Definitions :
btrue: tt,
lt_int: i <z j,
bnot: 
b,
le_int: i 
z j,
bag-map: bag-map(f;bs),
reduce: reduce(f;k;as),
concat: concat(ll),
bag-union: bag-union(bbs),
bfalse: ff,
map: map(f;as),
ycomb: Y,
bag-combine: 
x
bs.f[x],
eq_int: (i =
j),
ifthenelse: if b then t else f fi ,
lifting-gen-rev: lifting-gen-rev(n;f;bags),
lifting-loc-gen-rev: lifting-loc-gen-rev(n;bags;loc;f),
lifting2-loc: lifting2-loc(f;loc;abag;bbag),
select: l[i],
lifting-gen-list-rev: lifting-gen-list-rev(n;bags),
empty-bag: {},
lifting-loc-2: lifting-loc-2(f),
so_lambda: 
x.t[x],
member: t T,
all: 
x:A. B[x],
Accum-loc-class: Accum-loc-class(f;init;X),
Memory-loc-class: Memory-loc-class(f;init;X),
Memory1: Memory1(init;tr;X),
ler2_Nbr: ler2_Nbr(),
uimplies: b supposing a,
so_apply: x[s],
implies: P 
Q,
uall: [x:A]. B[x]
Lemmas :
ler2_config'base_nlp,
bag_wf,
empty-bag_wf,
lifting-loc-2_wf,
rec-combined-loc-class-opt-1-nlp,
ler2_config'base_wf,
single-bag_wf,
ler2_new_conf_wf,
Message_wf,
Accum-loc-class_wf,
valueall-type_wf,
Id-valueall-type,
int-valueall-type,
product-valueall-type,
Id_wf,
primed-class-opt-nlp
NormalLProgrammable'(\mBbbZ{} \mtimes{} Id;ler2\_Nbr())
Date html generated:
2012_02_20-PM-06_13_17
Last ObjectModification:
2012_02_02-PM-02_42_08
Home
Index