Nuprl Lemma : es-pplus-trivial
∀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 ≤loc e2  
⇒ Q[e1;e2] 
⇒ [e1,e2]~([a,b].Q[a;b])+)
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 : 
es-pplus: [e1,e2]~([a,b].p[a; b])+
, 
all: ∀x:A. B[x]
, 
member: t ∈ T
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
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  \mleq{}loc  e2    {}\mRightarrow{}  Q[e1;e2]  {}\mRightarrow{}  [e1,e2]\msim{}([a,b].Q[a;b])+)
Date html generated:
2016_05_16-AM-09_57_31
Last ObjectModification:
2015_12_28-PM-09_30_24
Theory : new!event-ordering
Home
Index