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 :
exists: x:A. B[x],
and: P Q,
le: A B,
cs-inning: Inning(s;a),
all: x:A. B[x],
implies: P Q,
list: type List,
set: {x:A| B[x]} ,
l_member: (x l),
Id: Id,
not: A,
cs-archive-blocked: in state s, ws' blocks ws from archiving v in inning i
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:
2010_08_27-AM-12_29_16
Last ObjectModification:
2009_12_23-PM-03_23_43
Home
Index