Nuprl Lemma : mu_ex_v5_State-prior-single-val
es:EO'. init:Id. single-valued-classrel(es;Prior(mu_ex_v5_State(init))?mu_ex_v5_initState(init);
)
Proof not projected
Definitions occuring in Statement :
mu_ex_v5_State: mu_ex_v5_State(initial_token),
mu_ex_v5_initState: mu_ex_v5_initState(initial_token),
Message: Message,
primed-class-opt: Prior(X)?b,
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_initState: mu_ex_v5_initState(initial_token),
member: t 
T,
le: A 
B,
not: 
A,
implies: P 
Q,
false: False,
name: Name,
mu_ex_v5_State: mu_ex_v5_State(initial_token),
uall: [x:A]. B[x],
SM4-class-du: SM4-class-du(init;trX1;trX2;trX3;trX4),
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(),
prop: 
,
so_lambda: 
x.t[x],
so_apply: x[s]
Lemmas :
Id_wf,
event-ordering+_wf,
Message_wf,
primed-class-opt-single-val,
bool_wf,
mu_ex_v5_State_wf,
mu_ex_v5_initState_wf,
Accum-loc-class-single-val,
unit_wf2,
disjoint-union-class_wf,
mu_ex_v5_Request_wf,
mu_ex_v5_Token_wf,
mu_ex_v5_UseSR_wf,
mu_ex_v5_LeaveCS_wf,
disjoint-union-tr_wf,
mu_ex_v5_onRequest_wf,
mu_ex_v5_onToken_wf,
uall_wf,
all_wf,
equal_wf,
mu_ex_v5_onUseSR_wf,
mu_ex_v5_onLeaveCS_wf,
disjoint-union-class-single-val,
single-valued-classrel-base
\mforall{}es:EO'. \mforall{}init:Id.
single-valued-classrel(es;Prior(mu\_ex\_v5\_State(init))?mu\_ex\_v5\_initState(init);\mBbbB{} \mtimes{} \mBbbB{} \mtimes{} \mBbbB{})
Date html generated:
2012_02_20-PM-07_00_09
Last ObjectModification:
2012_02_02-PM-03_01_43
Home
Index