Nuprl Lemma : mu_ex_v5_State-single-val
es:EO'. init:Id. single-valued-classrel(es;mu_ex_v5_State(init);
)
Proof not projected
Definitions occuring in Statement :
mu_ex_v5_State: mu_ex_v5_State(initial_token),
Message: Message,
single-valued-classrel: single-valued-classrel(es;X;T),
event-ordering+: EO+(Info),
Id: Id,
bool: ,
all: x:A. B[x],
product: x:A B[x]
Definitions :
all: x:A. B[x],
mu_ex_v5_State: mu_ex_v5_State(initial_token),
SM4-class-du: SM4-class-du(init;trX1;trX2;trX3;trX4),
mu_ex_v5_initState: mu_ex_v5_initState(initial_token),
mu_ex_v5_Request: mu_ex_v5_Request(),
mu_ex_v5_Token: mu_ex_v5_Token(),
mu_ex_v5_UseSR: mu_ex_v5_UseSR(),
mu_ex_v5_LeaveCS: mu_ex_v5_LeaveCS(),
uall: [x:A]. B[x],
implies: P 
Q,
le: A 
B,
member: t 
T,
prop: 
,
so_lambda: 
x.t[x],
name: Name,
not: 
A,
false: False,
so_apply: x[s]
Lemmas :
Accum-loc-class-single-val,
unit_wf2,
bool_wf,
disjoint-union-class_wf,
Message_wf,
mu_ex_v5_Request_wf,
mu_ex_v5_Token_wf,
mu_ex_v5_UseSR_wf,
mu_ex_v5_LeaveCS_wf,
mu_ex_v5_initState_wf,
disjoint-union-tr_wf,
mu_ex_v5_onRequest_wf,
Id_wf,
mu_ex_v5_onToken_wf,
uall_wf,
all_wf,
mu_ex_v5_onUseSR_wf,
mu_ex_v5_onLeaveCS_wf,
disjoint-union-class-single-val,
single-valued-classrel-base,
event-ordering+_wf
\mforall{}es:EO'. \mforall{}init:Id. single-valued-classrel(es;mu\_ex\_v5\_State(init);\mBbbB{} \mtimes{} \mBbbB{} \mtimes{} \mBbbB{})
Date html generated:
2012_02_20-PM-07_00_02
Last ObjectModification:
2012_02_02-PM-03_01_39
Home
Index