Nuprl Lemma : mu_ex_v4_main-single-val
es:EO'. cs,p1,p2,init:Id. single-valued-classrel(es;mu_ex_v4_main(cs;init;p1;p2);Id 
Message)
Proof not projected
Definitions occuring in Statement :
mu_ex_v4_main: mu_ex_v4_main(cs;initial_token;proc1;proc2),
Message: Message,
single-valued-classrel: single-valued-classrel(es;X;T),
event-ordering+: EO+(Info),
Id: Id,
all: x:A. B[x],
product: x:A B[x]
Definitions :
all: x:A. B[x],
member: t 
T,
mu_ex_v4_Exec: mu_ex_v4_Exec(),
mu_ex_v4_EnterCS: mu_ex_v4_EnterCS(),
so_lambda: 
x.t[x],
prop: 
,
mu_ex_v4_LeaveCS: mu_ex_v4_LeaveCS(),
mu_ex_v4_UseCS: mu_ex_v4_UseCS(),
SM4-class-du: SM4-class-du(init;trX1;trX2;trX3;trX4),
mu_ex_v4_State: mu_ex_v4_State(initial_token),
false: False,
implies: P 
Q,
mu_ex_v4_Token: mu_ex_v4_Token(),
le: A 
B,
mu_ex_v4_PrState: mu_ex_v4_PrState(initial_token),
mu_ex_v4_PrToken: mu_ex_v4_PrToken(),
mu_ex_v4_Request: mu_ex_v4_Request(),
let: let,
mu_ex_v4_HandleLeaveCS: mu_ex_v4_HandleLeaveCS(initial_token;proc1;proc2),
mu_ex_v4_HandleToken: mu_ex_v4_HandleToken(cs;initial_token),
mu_ex_v4_HandleUseCS: mu_ex_v4_HandleUseCS(cs;initial_token;proc1;proc2),
mu_ex_v4_HandleRequests: mu_ex_v4_HandleRequests(initial_token;proc1;proc2),
not: 
A,
and: P 
Q,
uall: [x:A]. B[x],
mu_ex_v4_CS: mu_ex_v4_CS(),
mu_ex_v4_P: mu_ex_v4_P(cs;initial_token;proc1;proc2),
mu_ex_v4_main: mu_ex_v4_main(cs;initial_token;proc1;proc2),
name: Name,
label: ...$L... t,
spreadn: spread3,
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
mu_ex_v4_initState: mu_ex_v4_initState(initial_token),
pi1: fst(t),
eq_atom: x =a y,
atom-deq: AtomDeq,
band: p 
q,
list-deq: list-deq(eq),
name-deq: NameDeq,
uiff: uiff(P;Q),
guard: {T},
or: P 
Q,
name_eq: name_eq(x;y),
assert: 
b,
lt_int: i <z j,
bnot: b,
le_int: i z j,
eq_int: (i =
j),
ycomb: Y,
select: l[i],
lifting-gen-list-rev: lifting-gen-list-rev(n;bags),
so_apply: x[s],
uimplies: b supposing a,
bool: 
,
unit: Unit,
pMsg: pMsg(P.M[P]),
decidable: Dec(P),
Message: Message,
sq_type: SQType(T),
exists: 
x:A. B[x],
squash: 
T,
concat-lifting-list: concat-lifting-list(n;bags),
concat-lifting: concat-lifting(n;f;bags),
concat-lifting-loc: concat-lifting-loc(n;bags;loc;f),
simple-loc-comb: F|Loc; Xs|,
concat-lifting-loc-3: concat-lifting-loc-3(f),
simple-loc-comb-3: F|Loc, X, Y, Z|,
classrel: v X(e),
rev_uimplies: rev_uimplies(P;Q),
sq_or: a b,
iff: P 
Q,
subtype: S 
T,
it: 
,
eclass: EClass(A[eo; e]),
es-header: es-header(es;e)
Lemmas :
Id_wf,
event-ordering+_wf,
Message_wf,
event-ordering+_inc,
es-E_wf,
simple-loc-comb-1-concat-single-val,
mu_ex_v4_Exec_wf,
it_wf,
mu_ex_v4_send_leave_cs_wf,
mu_ex_v4_EnterCS_wf,
mu_ex_v4_send_exec_wf,
concat-lifting-loc-1_wf,
simple-loc-comb-1_wf,
mu_ex_v4_send_enter_cs_wf,
simple-loc-comb-2-concat-single-val,
disjoint-union-class-single-val,
mu_ex_v4_onLeaveCS_wf,
mu_ex_v4_onUseCS_wf,
equal_wf,
all_wf,
uall_wf,
mu_ex_v4_onToken_wf,
mu_ex_v4_onRequest_wf,
disjoint-union-tr_wf,
mu_ex_v4_LeaveCS_wf,
mu_ex_v4_UseCS_wf,
disjoint-union-class_wf,
Accum-loc-class-single-val,
mu_ex_v4_initState_wf,
mu_ex_v4_State_wf,
mu_ex_v4_Token_wf,
primed-class-opt-single-val,
single-valued-classrel-base,
mu_ex_v4_PrState_wf,
mu_ex_v4_PrToken_wf,
mu_ex_v4_Request_wf,
bool_wf,
unit_wf2,
simple-loc-comb-3-concat-single-val,
mu_ex_v4_HandleLeaveCS_wf,
mu_ex_v4_HandleToken_wf,
mu_ex_v4_HandleRequests_wf,
parallel-class_wf,
on-loc-class-single-val,
class-at-single-val,
single-bag_wf,
mu_ex_v4_CS_wf,
empty-bag_wf,
cons-bag_wf,
mu_ex_v4_P_wf,
on-loc-class_wf,
class-at_wf,
parallel-class-single-val,
eclass_wf2,
mu_ex_v4_HandleUseCS_wf,
mu_ex_v4_otherProc_wf,
mu_ex_v4_send_token_wf,
bag_wf,
ifthenelse_wf,
assert_of_bnot,
eqff_to_assert,
uiff_transitivity,
eqtt_to_assert,
not_wf,
bnot_wf,
assert_wf,
mu_ex_v4_send_request_wf,
mu_ex_v4_send_busy_wf,
es-info_wf,
name_eq_wf,
decidable__assert,
classrel_wf,
atom_subtype_base,
list_subtype_base,
name_wf,
base-noloc-classrel,
assert-name_eq,
bag-member-single,
bool_subtype_base,
subtype_base_sq,
bool_cases,
ifthenelse-wf,
simple-loc-comb-2-concat-classrel,
bag-member-union,
bag-combine_wf,
bag-member-combine,
not_functionality_wrt_uiff,
es-header_wf,
parallel-classrel,
simple-loc-comb-1-concat-classrel,
es-loc_wf,
on-loc-classrel,
classrel-at
\mforall{}es:EO'. \mforall{}cs,p1,p2,init:Id. single-valued-classrel(es;mu\_ex\_v4\_main(cs;init;p1;p2);Id \mtimes{} Message)
Date html generated:
2012_02_20-PM-06_36_05
Last ObjectModification:
2012_02_02-PM-02_56_02
Home
Index