Nuprl Lemma : es-pred?_property

es:EO. ∀e:E.
  case es-pred?(es;e)
   of inl(p) =>
   (loc(p) loc(e) ∈ Id) ∧ (p < e) ∧ (∀e':E. (e' < e)  ((e' p ∈ E) ∨ (e' < p)) supposing loc(e') loc(e) ∈ Id)
   inr(z) =>
   ∀e':E. ¬(e' < e) supposing loc(e') loc(e) ∈ Id


Proof




Definitions occuring in Statement :  es-pred?: es-pred?(es;e) es-causl: (e < e') es-loc: loc(e) es-E: E event_ordering: EO Id: Id uimplies: supposing a all: x:A. B[x] not: ¬A implies:  Q or: P ∨ Q and: P ∧ Q decide: case of inl(x) => s[x] inr(y) => t[y] equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] es-pred?: es-pred?(es;e) member: t ∈ T uall: [x:A]. B[x] es-E: E es-base-E: es-base-E(es) implies:  Q exposed-bfalse: exposed-bfalse bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False not: ¬A

Latex:
\mforall{}es:EO.  \mforall{}e:E.
    case  es-pred?(es;e)
      of  inl(p)  =>
      (loc(p)  =  loc(e))
      \mwedge{}  (p  <  e)
      \mwedge{}  (\mforall{}e':E.  (e'  <  e)  {}\mRightarrow{}  ((e'  =  p)  \mvee{}  (e'  <  p))  supposing  loc(e')  =  loc(e))
      |  inr(z)  =>
      \mforall{}e':E.  \mneg{}(e'  <  e)  supposing  loc(e')  =  loc(e)



Date html generated: 2016_05_16-AM-09_17_17
Last ObjectModification: 2015_12_28-PM-09_56_49

Theory : new!event-ordering


Home Index