Nuprl Lemma : mu_ex_v6_State_nlp
initial_token:Id. NormalLProgrammable'(
;mu_ex_v6_State(initial_token))
Proof not projected
Definitions occuring in Statement :
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
Id: Id,
bool: ,
all: x:A. B[x],
product: x:A B[x]
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),
unit: Unit,
so_lambda: 
x.t[x],
member: t T,
Accum-loc-class: Accum-loc-class(f;init;X),
Memory-loc-class: Memory-loc-class(f;init;X),
Memory4: Memory4(init;tr1;X1;tr2;X2;tr3;X3;tr4;X4),
mu_ex_v6_State: mu_ex_v6_State(initial_token),
bool: ,
all: x:A. B[x],
uimplies: b supposing a,
so_apply: x[s],
implies: P 
Q,
uall: [x:A]. B[x]
Lemmas :
mu_ex_v6_useSR'base_nlp,
mu_ex_v6_token'base_nlp,
mu_ex_v6_leaveCS'base_nlp,
mu_ex_v6_request'base_nlp,
disjoint-union-comb-nlp,
Id_wf,
bag_wf,
empty-bag_wf,
lifting-loc-2_wf,
rec-combined-loc-class-opt-1-nlp,
mu_ex_v6_useSR'base_wf,
mu_ex_v6_token'base_wf,
mu_ex_v6_leaveCS'base_wf,
mu_ex_v6_request'base_wf,
disjoint-union-comb_wf,
mu_ex_v6_initState_wf,
mu_ex_v6_onUseSR_wf,
mu_ex_v6_onToken_wf,
mu_ex_v6_onLeaveCS_wf,
mu_ex_v6_onRequest_wf,
disjoint-union-tr_wf,
Message_wf,
Accum-loc-class_wf,
valueall-type_wf,
equal-valueall-type,
unit_wf2,
union-valueall-type,
product-valueall-type,
bool_wf,
primed-class-opt-nlp
\mforall{}initial$_{token}$:Id. NormalLProgrammable'(\mBbbB{} \mtimes{} \mBbbB{} \mtimes{} \mBbbB{};mu\_ex\_v6\_State(initial\mbackslash{}ff2\000C4_{token}$))
Date html generated:
2012_02_20-PM-07_10_23
Last ObjectModification:
2012_02_02-PM-03_06_31
Home
Index