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