Nuprl Lemma : es-pplus-le
∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[Q:{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ]. ([e1,e2]~([a,b].Q[a;b])+ 
⇒ e1 ≤loc e2 )
Proof
Definitions occuring in Statement : 
es-pplus: [e1,e2]~([a,b].p[a; b])+
, 
es-le: e ≤loc e' 
, 
es-loc: loc(e)
, 
es-E: E
, 
event_ordering: EO
, 
Id: Id
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
so_apply: x[s1;s2]
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
set: {x:A| B[x]} 
, 
function: x:A ⟶ B[x]
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
member: t ∈ T
, 
uall: ∀[x:A]. B[x]
, 
implies: P 
⇒ Q
, 
prop: ℙ
, 
so_lambda: λ2x y.t[x; y]
, 
so_apply: x[s1;s2]
, 
es-pplus: [e1,e2]~([a,b].p[a; b])+
Latex:
\mforall{}es:EO.  \mforall{}e1:E.  \mforall{}e2:\{e:E|  loc(e)  =  loc(e1)\}  .
    \mforall{}[Q:\{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}]
        ([e1,e2]\msim{}([a,b].Q[a;b])+  {}\mRightarrow{}  e1  \mleq{}loc  e2  )
Date html generated:
2016_05_16-AM-09_57_37
Last ObjectModification:
2015_12_28-PM-09_30_17
Theory : new!event-ordering
Home
Index