Nuprl Lemma : mu_ex_v5_tok-dec_wf
es:EO'. m1,m2,init,p1,p2,p:Id. e:E.
(mu_ex_v5_tok-dec{i:l}(es;m1;m2;init;p1;p2;p;e) 
{b:
|
b
<p, make-Msg([token];Unit;
)>
mu_ex_v5_main(init;m1;m2;p1;p2)(e)} )
Proof not projected
Definitions occuring in Statement :
mu_ex_v5_tok-dec: mu_ex_v5_tok-dec{i:l}(es;m1;m2;init;p1;p2;p;e),
mu_ex_v5_main: mu_ex_v5_main(initial_token;m1;m2;proc1;proc2),
make-Msg: make-Msg(hdr;typ;val),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-E: E,
Id: Id,
assert: b,
bool: ,
it: ,
all: x:A. B[x],
iff: P Q,
unit: Unit,
member: t T,
set: {x:A| B[x]} ,
pair: <a, b>,
product: x:A 
B[x],
cons: [car / cdr],
nil: [],
token: "$token"
Definitions :
all: x:A. B[x],
member: t T,
iff: P Q,
unit: Unit,
mu_ex_v5_tok-dec: mu_ex_v5_tok-dec{i:l}(es;m1;m2;init;p1;p2;p;e),
and: P 
Q,
implies: P Q,
rev_implies: P Q,
prop: 
,
so_lambda: 
x.t[x],
squash: 
T,
bag-member: x bs,
not: 
A,
or: P 
Q,
classrel: v X(e),
decidable: Dec(P),
exists: 
x:A. B[x],
cand: A c B,
ifthenelse: if b then t else f fi ,
bfalse: ff,
btrue: tt,
isl: isl(x),
assert: b,
true: True,
uall: [x:A]. B[x],
so_apply: x[s],
uimplies: b supposing a,
false: False,
subtype: S 
T,
eclass: EClass(A[eo; e])
Lemmas :
assert_wf,
classrel_wf,
Message_wf,
Id_wf,
mu_ex_v5_main_wf,
make-Msg_wf,
unit_wf2,
equal-valueall-type,
valueall-type_wf,
it_wf,
iff_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
isl_wf,
true_wf,
all_wf,
decidable_wf,
subtype_rel_dep_function,
subtype_rel_set_simple,
subtype_rel_sum,
not_wf,
exists_wf,
bag_wf,
bag_qinc,
l_member_wf,
false_wf,
equal_wf
\mforall{}es:EO'. \mforall{}m1,m2,init,p1,p2,p:Id. \mforall{}e:E.
(mu\_ex\_v5\_tok-dec\{i:l\}(es;m1;m2;init;p1;p2;p;e) \mmember{} \{b:\mBbbB{}|
\muparrow{}b
\mLeftarrow{}{}\mRightarrow{} <p, make-Msg([token];Unit;\mcdot{})> \mmember{}
mu\_ex\_v5\_main(init;m1;m2;p1;p2)(e)\} )
Date html generated:
2012_02_20-PM-07_03_43
Last ObjectModification:
2012_02_02-PM-03_03_06
Home
Index