Nuprl Lemma : mu_ex_v5_assert-tok-dec
es:EO'. m1,m2,init,p1,p2,p:Id. e:E.
uiff(
mu_ex_v5_tok-dec{i:l}(es;m1;m2;init;p1;p2;p;e);<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,
it: ,
uiff: uiff(P;Q),
all: x:A. B[x],
unit: Unit,
pair: <a, b>,
product: x:A 
B[x],
cons: [car / cdr],
nil: [],
token: "$token"
Definitions :
all: x:A. B[x],
uiff: uiff(P;Q),
classrel: v X(e),
unit: Unit,
member: t T,
iff: P 
Q,
prop: 
,
and: P 
Q,
implies: P Q,
rev_implies: P Q,
squash: 
T,
true: True,
uimplies: b supposing a,
bag-member: x bs,
guard: {T},
uall: [x:A]. B[x],
sq_stable: SqStable(P),
subtype: S 
T
Lemmas :
mu_ex_v5_tok-dec_wf,
bool_wf,
iff_wf,
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,
sq_stable__uiff,
sq_stable__assert,
sq_stable__classrel,
equal_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
uiff_functionality_wrt_uiff2
\mforall{}es:EO'. \mforall{}m1,m2,init,p1,p2,p:Id. \mforall{}e:E.
uiff(\muparrow{}mu\_ex\_v5\_tok-dec\{i:l\}(es;m1;m2;init;p1;p2;p;e);<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_51
Last ObjectModification:
2012_02_02-PM-03_03_10
Home
Index