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: 2016_05_17-PM-00_46_44 Last ObjectModification: 2012_08_30-PM-04_34_24 Theory : event-logic-applications Home Index