Nuprl Lemma : mu_ex_v6_Handle_nlp
initial_token:Id. x1:EClass'(Unit). x0:Id 
Unit 
bag(Id Message).
(NormalLProgrammable'(Unit;x1) 
NormalLProgrammable'(Id Message;mu_ex_v6_Handle(initial_token) x0 x1))
Proof not projected
Definitions occuring in Statement :
mu_ex_v6_Handle: mu_ex_v6_Handle(initial_token),
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
eclass: EClass(A[eo; e]),
Id: Id,
bool: ,
all: x:A. B[x],
implies: P Q,
unit: Unit,
apply: f a,
function: x:A B[x],
product: x:A B[x],
bag: bag(T)
Definitions :
top: Top,
true: True,
so_lambda: 
x.t[x],
member: t 
T,
and: P 
Q,
squash: 
T,
or: P 
Q,
mu_ex_v6_Handle: mu_ex_v6_Handle(initial_token),
implies: P Q,
eclass: EClass(A[eo; e]),
all: x:A. B[x],
uimplies: b supposing a,
so_apply: x[s],
uall: [x:A]. B[x],
subtype: S 
T,
prop: 
Lemmas :
event-ordering+_inc,
es-E_wf,
event-ordering+_wf,
normal-locally-programmable_wf,
mu_ex_v6_State_nlp,
equal_wf,
all_wf,
squash_wf,
bag_wf,
empty-bag_wf,
subtype_top,
top_wf,
subtype_rel_bag,
concat-lifting-loc-2-strict,
mu_ex_v6_State_wf,
concat-lifting-loc-2_wf,
valueall-type_wf,
Message-valueall-type,
Id-valueall-type,
product-valueall-type,
Message_wf,
Id_wf,
bool_wf,
unit_wf2,
simple-loc-comb-2-nlp
\mforall{}initial$_{token}$:Id. \mforall{}x1:EClass'(Unit). \mforall{}x0:Id {}\mrightarrow{} Unit {}\mrightarrow{} \mBbbB{} \mtimes{} \mBbbB{} \mtimes{} \mBbbB{} {}\mrightarrow{} bag(Id \000C\mtimes{} Message).
(NormalLProgrammable'(Unit;x1)
{}\mRightarrow{} NormalLProgrammable'(Id \mtimes{} Message;mu\_ex\_v6\_Handle(initial$_{token}$) x0 x1)\000C)
Date html generated:
2012_02_20-PM-07_10_43
Last ObjectModification:
2012_02_02-PM-03_06_43
Home
Index