Nuprl Lemma : mu_ex_v4_State_nlp
initial_token:Id. NormalLProgrammable'(
;mu_ex_v4_State(initial_token))
Proof not projected
Definitions occuring in Statement :
mu_ex_v4_State: mu_ex_v4_State(initial_token),
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
Id: Id,
bool: ,
all: x:A. B[x],
product: x:A B[x]
Definitions :
all: x:A. B[x],
bool: ,
mu_ex_v4_State: mu_ex_v4_State(initial_token),
SM4-class-du: SM4-class-du(init;trX1;trX2;trX3;trX4),
Accum-loc-class: Accum-loc-class(f;init;X),
lifting-loc-2: lifting-loc-2(f),
uall: [x:A]. B[x],
empty-bag: {},
implies: P 
Q,
unit: Unit,
member: t 
T,
so_lambda: 
x.t[x],
prop: 
,
lifting-gen-list-rev: lifting-gen-list-rev(n;bags),
select: l[i],
lifting2-loc: lifting2-loc(f;loc;abag;bbag),
lifting-loc-gen-rev: lifting-loc-gen-rev(n;bags;loc;f),
lifting-gen-rev: lifting-gen-rev(n;f;bags),
ifthenelse: if b then t else f fi ,
eq_int: (i =
j),
bag-combine: 
xbs.f[x],
ycomb: Y,
map: map(f;as),
bfalse: ff,
bag-union: bag-union(bbs),
concat: concat(ll),
reduce: reduce(f;k;as),
bag-map: bag-map(f;bs),
le_int: i 
z j,
bnot: 
b,
lt_int: i <z j,
btrue: tt,
uimplies: b supposing a,
so_apply: x[s]
Lemmas :
rec-combined-loc-class-opt-1-nlp,
unit_wf2,
Id_wf,
bool_wf,
product-valueall-type,
union-valueall-type,
equal-valueall-type,
valueall-type_wf,
lifting-loc-2_wf,
disjoint-union-tr_wf,
mu_ex_v4_onRequest_wf,
mu_ex_v4_onToken_wf,
uall_wf,
all_wf,
equal_wf,
mu_ex_v4_onUseCS_wf,
mu_ex_v4_onLeaveCS_wf,
mu_ex_v4_initState_wf,
disjoint-union-class_wf,
Message_wf,
mu_ex_v4_Request_wf,
mu_ex_v4_Token_wf,
mu_ex_v4_UseCS_wf,
mu_ex_v4_LeaveCS_wf,
empty-bag_wf,
bag_wf,
disjoint-union-class-nlp,
int-valueall-type,
Id-valueall-type,
mu_ex_v4_Request_nlp,
mu_ex_v4_Token_nlp,
mu_ex_v4_UseCS_nlp,
mu_ex_v4_LeaveCS_nlp
\mforall{}initial$_{token}$:Id. NormalLProgrammable'(\mBbbB{} \mtimes{} \mBbbB{} \mtimes{} \mBbbB{};mu\_ex\_v4\_State(initial\mbackslash{}ff2\000C4_{token}$))
Date html generated:
2012_02_20-PM-06_31_05
Last ObjectModification:
2012_02_02-PM-02_53_01
Home
Index