Nuprl Lemma : mu_ex_v5-ilf
HIDDEN 
HIDDEN HIDDEN
Proof not projected
Definitions occuring in Statement :
mu_ex_v5_main: mu_ex_v5_main(initial_token;m1;m2;proc1;proc2),
mu_ex_v5_State: mu_ex_v5_State(initial_token),
mu_ex_v5_initState: mu_ex_v5_initState(initial_token),
mu_ex_v5_onLeaveCS: mu_ex_v5_onLeaveCS(),
mu_ex_v5_onUseSR: mu_ex_v5_onUseSR(),
mu_ex_v5_onToken: mu_ex_v5_onToken(),
mu_ex_v5_onRequest: mu_ex_v5_onRequest(),
mu_ex_v5_getMachine: mu_ex_v5_getMachine(m1;m2;proc1),
mu_ex_v5_getOtherProc: mu_ex_v5_getOtherProc(proc1;proc2),
mu_ex_v5_UseSR: mu_ex_v5_UseSR(),
mu_ex_v5_LeaveCS: mu_ex_v5_LeaveCS(),
mu_ex_v5_Token: mu_ex_v5_Token(),
mu_ex_v5_Request: mu_ex_v5_Request(),
disjoint-union-tr: tr1 + tr2,
disjoint-union-class: X + Y,
Memory-loc-class: Memory-loc-class(f;init;X),
make-Msg: make-Msg(hdr;typ;val),
base-headers-msg-val: Base(hdr;typ),
Message: Message,
primed-class-opt: Prior(X)?b,
classrel: v 
X(e),
event-ordering+: EO+(Info),
es-loc: loc(e),
es-E: E,
Id: Id,
assert: 
b,
bool: 
,
sq_or: a 
b,
it: 
,
uall: 
[x:A]. B[x],
guard: {T},
all: x:A. B[x],
exists: 
x:A. B[x],
iff: P 
Q,
not: 
A,
squash: T,
or: P Q,
and: P Q,
unit: Unit,
apply: f a,
pair: <a, b>,
product: x:A 
B[x],
inr: inr x ,
inl: inl x ,
union: left + right,
cons: [car / cdr],
nil: [],
token: "$token",
equal: s = t,
hide: HIDDEN
Definitions :
and: P Q,
hide: HIDDEN,
uall: [x:A]. B[x],
guard: {T},
iff: P Q,
classrel: v X(e),
member: t T,
squash: T,
prop: 
,
name: Name,
cand: A c B,
implies: P Q,
rev_implies: P Q,
or: P Q,
true: True,
bag-member: x bs,
top: Top,
assert: b,
isl: isl(x),
outl: outl(x),
bnot: 
b,
outr: outr(x),
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(),
all: x:A. B[x],
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
so_lambda: 
x.t[x],
not: A,
false: False,
exists: x:A. B[x],
mu_ex_v5_onRequest: mu_ex_v5_onRequest(),
mu_ex_v5_onToken: mu_ex_v5_onToken(),
mu_ex_v5_onUseSR: mu_ex_v5_onUseSR(),
mu_ex_v5_onLeaveCS: mu_ex_v5_onLeaveCS(),
spreadn: spread3,
SM4-class-du: SM4-class-du(init;trX1;trX2;trX3;trX4),
mu_ex_v5_State: mu_ex_v5_State(initial_token),
sq_or: a b,
unit: Unit,
subtype: S 
T,
label: ...$L... t,
suptype: suptype(S; T),
mu_ex_v5_HandleUseSR: mu_ex_v5_HandleUseSR(initial_token;m1;m2;proc1;proc2),
mu_ex_v5_send_token: mu_ex_v5_send_token(),
mu_ex_v5_send_busy: mu_ex_v5_send_busy(),
mu_ex_v5_send_enter_cs: mu_ex_v5_send_enter_cs(),
mu_ex_v5_send_request: mu_ex_v5_send_request(),
mu_ex_v5_PrState: mu_ex_v5_PrState(initial_token),
let: let,
mu_ex_v5_HandleRequests: mu_ex_v5_HandleRequests(initial_token;proc1;proc2),
mu_ex_v5_HandleToken: mu_ex_v5_HandleToken(initial_token;m1;m2;proc1),
mu_ex_v5_HandleLeaveCS: mu_ex_v5_HandleLeaveCS(initial_token;proc1;proc2),
mu_ex_v5_P: mu_ex_v5_P(initial_token;m1;m2;proc1;proc2),
mu_ex_v5_main: mu_ex_v5_main(initial_token;m1;m2;proc1;proc2),
rev_uimplies: rev_uimplies(P;Q),
uiff: uiff(P;Q),
uimplies: b supposing a,
so_apply: x[s],
pi1: fst(t),
pi2: snd(t),
bool: ,
it:
Lemmas :
false_wf,
classrel_wf,
Message_wf,
unit_wf2,
base-headers-msg-val_wf,
it_wf,
squash_wf,
or_wf,
true_wf,
assert_wf,
bnot_wf,
not_wf,
disjoint-union-class_wf,
mu_ex_v5_Request_wf,
mu_ex_v5_Token_wf,
mu_ex_v5_UseSR_wf,
mu_ex_v5_LeaveCS_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
squash-classrel,
or_false_r,
and_true_l,
and_false_l,
disjoint-union-classrel-ite-weak2,
outr_wf,
all_wf,
and_functionality_wrt_iff,
iff_transitivity,
iff_weakening_uiff,
squash_functionality_wrt_uiff,
or_functionality_wrt_iff,
all-unit,
isl_wf,
outl_wf,
squash_and,
squash_squash,
squash_not,
or_false_l,
exists_wf,
bool_wf,
band_wf,
Memory-loc-class_wf,
disjoint-union-tr_wf,
mu_ex_v5_onRequest_wf,
Id_wf,
mu_ex_v5_onToken_wf,
uall_wf,
equal_wf,
mu_ex_v5_onUseSR_wf,
mu_ex_v5_onLeaveCS_wf,
mu_ex_v5_initState_wf,
btrue_wf,
ifthenelse_wf,
bfalse_wf,
Accum-loc-class_wf,
SM4-class-du_wf,
mu_ex_v5_State_wf,
exists-product2,
Accum-loc-classrel-Memory,
exists-union,
es-loc_wf,
exists-unit,
sq_or_wf,
equal-valueall-type,
valueall-type_wf,
mu_ex_v5_getOtherProc_wf,
make-Msg_wf,
primed-class-opt_wf,
mu_ex_v5_send_token_wf,
bag-member_wf,
bag_wf,
single-bag_wf,
empty-bag_wf,
mu_ex_v5_getMachine_wf,
mu_ex_v5_send_busy_wf,
mu_ex_v5_send_enter_cs_wf,
mu_ex_v5_send_request_wf,
simple-loc-comb-2_wf,
concat-lifting-loc-2_wf,
mu_ex_v5_PrState_wf,
let_wf,
top_wf,
eclass_wf2,
parallel-class_wf,
mu_ex_v5_HandleRequests_wf,
mu_ex_v5_HandleToken_wf,
mu_ex_v5_HandleLeaveCS_wf,
mu_ex_v5_P_wf,
class-at_wf,
on-loc-class_wf,
cons-bag_wf,
mu_ex_v5_main_wf,
sq_or_sq_or,
ifthenelse-prop,
assert_of_band,
and_functionality_wrt_uiff2,
assert_of_bnot,
not_functionality_wrt_iff,
pi1_wf_top,
pi2_wf,
and_false_r,
bag-member-ifthenelse,
and_wf,
eqtt_to_assert,
bag-member-single-weak,
bor_wf,
uiff_transitivity,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_thru_band,
assert_of_bor,
or_functionality_wrt_uiff,
not_functionality_wrt_uiff,
bag-member-empty-weak,
squash_equal,
and_functionality_wrt_uiff3,
sq_or_squash3,
sq_or_squash,
simple-loc-comb-2-concat-classrel-weak,
parallel-classrel-weak,
classrel-at,
bag-member-cons,
on-loc-classrel
HIDDEN \mwedge{} HIDDEN \mwedge{} HIDDEN
Date html generated:
2012_02_20-PM-06_58_34
Last ObjectModification:
2012_02_04-AM-10_26_28
Home
Index