Nuprl Definition : sig-release-thread
sig-release-thread(s;es;A;thr) ==
∀i:ℕ||thr||. ∀j:ℕi.
((↑thr[j] ∈b Sign)
⇒ (∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send))
⇒ (∀e:E. ((¬(loc(e) = A ∈ Id)) ⇒ (e has signature(thr[j])) ⇒ (thr[i] < e))))
Definitions occuring in Statement :
event-has: (e has a),
ses-sig: signature(e),
ses-sign: Sign,
ses-send: Send,
in-eclass: e ∈b X,
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
select: L[n],
length: ||as||,
int_seg: {i..j-},
assert: ↑b,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
add: n + m,
natural_number: $n,
equal: s = t ∈ T
FDL editor aliases :
sig-release-thread
Latex:
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:
2015_07_23-PM-00_19_38
Last ObjectModification:
2012_08_30-PM-04_34_24
Home
Index