---

Step * 1 2 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
⊢ ∀x,y:E.  (((λe,e'. (e < e')) x y) ⇒ (¬((λe,e'. (e < e')) y x)))
BY
{ ((Reduce 0 THEN Auto) THEN RelRST 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{}  \mforall{}x,y:E.    (((\mlambda{}e,e'.  (e  <  e'))  x  y)  {}\mRightarrow{}  (\mneg{}((\mlambda{}e,e'.  (e  <  e'))  y  x)))


By

((Reduce  0  THEN  Auto)  THEN  RelRST  THEN  Auto)

---

Home Index