sig-release-thread(s;es;A;thr) ==
i:
||thr||. j:i.
((
thr[j] 
Sign)
(k:{j + 1..i
}. (
thr[k] Send))
(e:E. (((loc(e) = A)) (e has signature(thr[j])) (thr[i] < e))))
Definitions :
length: ||as||,
ses-sign: Sign,
int_seg: {i..j},
add: n + m,
natural_number: $n,
assert: b,
in-eclass: e X,
ses-send: Send,
all: x:A. B[x],
es-E: E,
not: A,
equal: s = t,
Id: Id,
es-loc: loc(e),
implies: P Q,
event-has: (e has a),
ses-sig: signature(e),
es-causl: (e < e'),
select: l[i]
FDL editor aliases :
sig-release-thread
sig-release-thread(s;es;A;thr) ==
\mforall{}i:\mBbbN{}||thr||. \mforall{}j:\mBbbN{}i.
((\muparrow{}thr[j] \mmember{}\msubb{} Sign)
{}\mRightarrow{} (\mforall{}k:\{j + 1..i\msupminus{}\}. (\mneg{}\muparrow{}thr[k] \mmember{}\msubb{} Send))
{}\mRightarrow{} (\mforall{}e:E. ((\mneg{}(loc(e) = A)) {}\mRightarrow{} (e has signature(thr[j])) {}\mRightarrow{} (thr[i] < e))))
Date html generated:
2010_08_28-AM-03_16_36
Last ObjectModification:
2010_03_19-PM-12_03_14
Home
Index