Nuprl Definition : es-quiet-until

es-quiet-until(es;i;e.P[e]) ==
  e:E. ((loc(e) = i)  (e':E. (((loc(e') = i))  (e < e')  (e'':E. ((e'' < e')  P[e''])))))


Proof not projected



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
FDL editor aliases :  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: 2011_10_20-PM-03_16_59
Last ObjectModification: 2011_10_11-PM-12_10_02

Home Index