Nuprl Lemma : cond_equiv_to_causl
∀es:EO
  ∀[R:E ⟶ E ⟶ ℙ]. ∀[P:E ⟶ ℙ].
    (R => λe,e'. (e < e')
    
⇒ (∀x,y:E.  (((P x) ∧ (P y)) 
⇒ (((R x y) ∨ (x = y ∈ E)) ∨ (R y x))))
    
⇒ (∀x,y:E.  (((P x) ∧ (P y)) 
⇒ (R x y 
⇐⇒ (x < y)))))
Proof
Definitions occuring in Statement : 
es-causl: (e < e')
, 
es-E: E
, 
event_ordering: EO
, 
rel_implies: R1 => R2
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
all: ∀x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
implies: P 
⇒ Q
, 
or: P ∨ Q
, 
and: P ∧ Q
, 
apply: f a
, 
lambda: λx.A[x]
, 
function: x:A ⟶ B[x]
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
uall: ∀[x:A]. B[x]
, 
implies: P 
⇒ Q
, 
member: t ∈ T
, 
prop: ℙ
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
uimplies: b supposing a
, 
and: P ∧ Q
, 
iff: P 
⇐⇒ Q
, 
cand: A c∧ B
, 
es-causl: (e < e')
, 
squash: ↓T
, 
rev_implies: P 
⇐ Q
, 
trans: Trans(T;x,y.E[x; y])
, 
guard: {T}
, 
not: ¬A
, 
false: False
Latex:
\mforall{}es:EO
    \mforall{}[R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:E  {}\mrightarrow{}  \mBbbP{}].
        (R  =>  \mlambda{}e,e'.  (e  <  e')
        {}\mRightarrow{}  (\mforall{}x,y:E.    (((P  x)  \mwedge{}  (P  y))  {}\mRightarrow{}  (((R  x  y)  \mvee{}  (x  =  y))  \mvee{}  (R  y  x))))
        {}\mRightarrow{}  (\mforall{}x,y:E.    (((P  x)  \mwedge{}  (P  y))  {}\mRightarrow{}  (R  x  y  \mLeftarrow{}{}\mRightarrow{}  (x  <  y)))))
Date html generated:
2016_05_16-AM-10_34_28
Last ObjectModification:
2016_01_17-PM-01_21_52
Theory : new!event-ordering
Home
Index