Nuprl Lemma : mu_ex_v5_PrState_nlp
initial_token:Id. NormalLProgrammable'(
;mu_ex_v5_PrState(initial_token))
Proof not projected
Definitions occuring in Statement :
mu_ex_v5_PrState: mu_ex_v5_PrState(initial_token),
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
Id: Id,
bool: ,
all: x:A. B[x],
product: x:A B[x]
Definitions :
all: x:A. B[x],
bool: ,
mu_ex_v5_PrState: mu_ex_v5_PrState(initial_token),
member: t 
T,
so_lambda: 
x.t[x],
unit: Unit,
uall: [x:A]. B[x],
implies: P 
Q,
so_apply: x[s]
Lemmas :
primed-class-opt-nlp,
bool_wf,
product-valueall-type,
union-valueall-type,
unit_wf2,
equal-valueall-type,
valueall-type_wf,
mu_ex_v5_State_wf,
mu_ex_v5_initState_wf,
mu_ex_v5_State_nlp,
Id_wf
\mforall{}initial$_{token}$:Id. NormalLProgrammable'(\mBbbB{} \mtimes{} \mBbbB{} \mtimes{} \mBbbB{};mu\_ex\_v5\_PrState(initial\mbackslash{}f\000Cf24_{token}$))
Date html generated:
2012_02_20-PM-06_55_13
Last ObjectModification:
2012_02_02-PM-02_58_42
Home
Index