Nuprl Lemma : mu_ex_v4_PrState_wf
[initial_token:Id]. (mu_ex_v4_PrState(initial_token) 
EClass'(
))
Proof not projected
Definitions occuring in Statement :
mu_ex_v4_PrState: mu_ex_v4_PrState(initial_token),
Message: Message,
eclass: EClass(A[eo; e]),
Id: Id,
bool: ,
uall: [x:A]. B[x],
member: t T,
product: x:A B[x]
Definitions :
uall: [x:A]. B[x],
member: t T,
mu_ex_v4_PrState: mu_ex_v4_PrState(initial_token)
Lemmas :
primed-class-opt_wf,
Message_wf,
bool_wf,
mu_ex_v4_initState_wf,
mu_ex_v4_State_wf,
Id_wf
\mforall{}[initial$_{token}$:Id]. (mu\_ex\_v4\_PrState(initial$_{token}$\000C) \mmember{} EClass'(\mBbbB{} \mtimes{} \mBbbB{} \mtimes{} \mBbbB{}))
Date html generated:
2012_02_20-PM-06_31_16
Last ObjectModification:
2012_02_02-PM-02_53_08
Home
Index