Nuprl Definition : cs-precondition
state s may consider v in inning i ==
∃ws:{a:Id| (a ∈ A)} List
((ws ∈ W)
∧ (∀b:{a:Id| (a ∈ A)} . ((b ∈ ws) ⇒ (i ≤ Inning(s;b))))
∧ (∀ws':{a:Id| (a ∈ A)} List. ((ws' ∈ W) ⇒ (¬in state s, ws' blocks ws from archiving v in inning i))))
Definitions occuring in Statement :
cs-archive-blocked: in state s, ws' blocks ws from archiving v in inning i,
cs-inning: Inning(s;a),
Id: Id,
l_member: (x ∈ l),
list: T List,
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]}
FDL editor aliases :
cs-precondition
state s may consider v in inning i ==
\mexists{}ws:\{a:Id| (a \mmember{} A)\} List
((ws \mmember{} W)
\mwedge{} (\mforall{}b:\{a:Id| (a \mmember{} A)\} . ((b \mmember{} ws) {}\mRightarrow{} (i \mleq{} Inning(s;b))))
\mwedge{} (\mforall{}ws':\{a:Id| (a \mmember{} A)\} List
((ws' \mmember{} W) {}\mRightarrow{} (\mneg{}in state s, ws' blocks ws from archiving v in inning i))))
Date html generated:
2015_07_17-AM-11_26_02
Last ObjectModification:
2012_02_25-AM-11_42_05
Home
Index