Nuprl Definition : cs-inning-committable
in state s, inning i could commit v ==
∃ws:{a:Id| (a ∈ A)} List
((ws ∈ W)
∧ (∀a:{a:Id| (a ∈ A)}
((a ∈ ws)
⇒ (by state s, a archived v in inning i ∨ in state s, a has not completed inning i))))
Definitions occuring in Statement :
cs-archived: by state s, a archived v in inning i
,
cs-not-completed: in state s, a has not completed inning i
,
Id: Id
,
l_member: (x ∈ l)
,
list: T List
,
all: ∀x:A. B[x]
,
exists: ∃x:A. B[x]
,
implies: P
⇒ Q
,
or: P ∨ Q
,
and: P ∧ Q
,
set: {x:A| B[x]}
FDL editor aliases :
cs-inning-committable
in state s, inning i could commit v ==
\mexists{}ws:\{a:Id| (a \mmember{} A)\} List
((ws \mmember{} W)
\mwedge{} (\mforall{}a:\{a:Id| (a \mmember{} A)\}
((a \mmember{} ws)
{}\mRightarrow{} (by state s, a archived v in inning i \mvee{} in state s, a has not completed inning i))))
Date html generated:
2015_07_17-AM-11_28_10
Last ObjectModification:
2012_02_25-AM-11_43_25
Home
Index