Nuprl Lemma : mu_ex_v6_initState_wf
[initial_token:Id]. (mu_ex_v6_initState(initial_token) 
Id 
bag(
))
Proof not projected
Definitions occuring in Statement :
mu_ex_v6_initState: mu_ex_v6_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 :
mu_ex_v6_initState: mu_ex_v6_initState(initial_token),
member: t T,
uall: [x:A]. B[x],
deq: EqDecider(T),
all: x:A. B[x]
Lemmas :
Id_wf,
deq_wf,
id-deq_wf,
bfalse_wf,
bool_wf,
single-bag_wf
\mforall{}[initial$_{token}$:Id]. (mu\_ex\_v6\_initState(initial$_{token}\mbackslash{}ff\000C24) \mmember{} Id {}\mrightarrow{} bag(\mBbbB{} \mtimes{} \mBbbB{} \mtimes{} \mBbbB{}))
Date html generated:
2012_02_20-PM-07_10_02
Last ObjectModification:
2012_02_02-PM-03_06_19
Home
Index