Nuprl Definition : cs-inning-committed
in state s, inning i has committed 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)))
Definitions occuring in Statement :
cs-archived: by state s, a archived v in inning i,
Id: Id,
l_member: (x ∈ l),
list: T List,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]}
FDL editor aliases :
cs-inning-committed
Latex:
in state s, inning i has committed 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)))
Date html generated:
2016_05_16-AM-11_59_23
Last ObjectModification:
2012_02_25-AM-11_43_12
Theory : event-ordering
Home
Index