Nuprl Definition : es-quiet-until
es-quiet-until(es;i;e.P[e]) ==
∃e:E. ((loc(e) = i ∈ Id) ∧ (∀e':E. ((¬(loc(e') = i ∈ Id)) ⇒ (e < e') ⇒ (∃e'':E. ((e'' < e') ∧ P[e''])))))
Definitions occuring in Statement :
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
es-quiet-until
es-quiet-until
es-quiet-until(es;i;e.P[e]) ==
\mexists{}e:E. ((loc(e) = i) \mwedge{} (\mforall{}e':E. ((\mneg{}(loc(e') = i)) {}\mRightarrow{} (e < e') {}\mRightarrow{} (\mexists{}e'':E. ((e'' < e') \mwedge{} P[e''])))))
Date html generated:
2015_07_17-AM-09_10_14
Last ObjectModification:
2013_03_25-PM-01_59_37
Home
Index