Nuprl Lemma : mu_ex_v5_decidable-prior-token
es:EO'. e:E.
((
e':E. (e' 
loc e 
mu_ex_v5_Token()(e'))) 
(e':E. (e' loc e 
(
mu_ex_v5_Token()(e')))))
Proof not projected
Definitions occuring in Statement :
mu_ex_v5_Token: mu_ex_v5_Token(),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-le: e loc e' ,
es-E: E,
it: ,
all: x:A. B[x],
exists: x:A. B[x],
not: A,
implies: P Q,
or: P Q,
and: P Q,
unit: Unit
Definitions :
name: Name,
true: True,
squash: 
T,
false: False,
le: A B,
ge: i 
j ,
nat: 
,
member: t T,
not: A,
implies: P Q,
or: P Q,
all: x:A. B[x],
so_lambda: 
x.t[x],
msg-has-type: msg-has-type(m;T),
cand: A c B,
es-header: es-header(es;e),
prop: 
,
guard: {T},
mu_ex_v5_Token: mu_ex_v5_Token(),
es-le: e loc e' ,
and: P Q,
exists: x:A. B[x],
decidable: Dec(P),
uall: [x:A]. B[x],
strongwellfounded: SWellFounded(R[x; y]),
uimplies: b supposing a,
so_apply: x[s],
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
rev_implies: P 
Q,
iff: P Q,
subtype: S 
T,
msg-header: msg-header(m)
Lemmas :
event-ordering+_wf,
es-E_wf,
equal_wf,
es-info_wf,
msg-header_wf,
decidable__equal_name,
es-causl_wf,
le_wf,
nat_wf,
less_than_wf,
ge_wf,
nat_properties,
Message_wf,
event-ordering+_inc,
es-causl-swellfnd,
type-valueall-type,
unit_wf2,
msg-type_wf,
eq_term_wf,
decidable__assert,
not_wf,
es-le_wf,
all_wf,
mu_ex_v5_Token_wf,
classrel_wf,
and_wf,
msg-body_wf2,
equal-unit,
it_wf,
base-noloc-classrel,
es-locl_wf,
es-first_wf,
exists_wf,
es-first-implies,
es-pred-causl,
es-pred_wf,
es-le_weakening,
es-locl_transitivity1,
es-pred-locl,
es-le-pred,
assert_elim,
es-locl-first,
btrue_neq_bfalse
\mforall{}es:EO'. \mforall{}e:E.
((\mexists{}e':E. (e' \mleq{}loc e \mwedge{} \mcdot{} \mmember{} mu\_ex\_v5\_Token()(e')))
\mvee{} (\mforall{}e':E. (e' \mleq{}loc e {}\mRightarrow{} (\mneg{}\mcdot{} \mmember{} mu\_ex\_v5\_Token()(e')))))
Date html generated:
2012_02_20-PM-07_03_14
Last ObjectModification:
2012_02_02-PM-03_02_55
Home
Index