Nuprl Lemma : mu_ex_v5_initState_wf
[initial_token:Id]. (mu_ex_v5_initState(initial_token) 
Id 
bag(
))
Proof not projected
Definitions occuring in Statement :
mu_ex_v5_initState: mu_ex_v5_initState(initial_token),
Id: Id,
bool: ,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
member: t T,
mu_ex_v5_initState: mu_ex_v5_initState(initial_token),
all: x:A. B[x],
deq: EqDecider(T)
Lemmas :
single-bag_wf,
bool_wf,
bfalse_wf,
id-deq_wf,
deq_wf,
Id_wf
\mforall{}[initial$_{token}$:Id]. (mu\_ex\_v5\_initState(initial$_{token}\mbackslash{}ff\000C24) \mmember{} Id {}\mrightarrow{} bag(\mBbbB{} \mtimes{} \mBbbB{} \mtimes{} \mBbbB{}))
Date html generated:
2012_02_20-PM-06_54_29
Last ObjectModification:
2012_02_02-PM-02_58_18
Home
Index