---

Step * 1 1 of Lemma cond_equiv_to_causl

.....antecedent..... 
1. es : EO@i'
2. [R] : E ─→ E ─→ ℙ
3. [P] : E ─→ ℙ
4. R => λe,e'. (e < e')@i
5. ∀x,y:E.  (((P x) ∧ (P y)) ⇒ (((R x y) ∨ (x = y ∈ E)) ∨ (R y x)))@i
6. x : E@i
⊢ Trans(E;x,y.(λe,e'. (e < e')) x y)
BY
{ (RepUR ``trans`` 0 THEN Auto) }

---

Latex:


.....antecedent..... 
1.  es  :  EO@i'
2.  [R]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
3.  [P]  :  E  {}\mrightarrow{}  \mBbbP{}
4.  R  =>  \mlambda{}e,e'.  (e  <  e')@i
5.  \mforall{}x,y:E.    (((P  x)  \mwedge{}  (P  y))  {}\mRightarrow{}  (((R  x  y)  \mvee{}  (x  =  y))  \mvee{}  (R  y  x)))@i
6.  x  :  E@i
\mvdash{}  Trans(E;x,y.(\mlambda{}e,e'.  (e  <  e'))  x  y)


By

(RepUR  ``trans``  0  THEN  Auto)

---

Home Index