---

Step * 1 of Lemma cond_equiv_to_causl


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
⊢ ∀y:E. (((P x) ∧ (P y)) ⇒ (R x y ⇐⇒ (x < y)))
BY
{ ((InstLemma `cond_rel_equivalent` [⌈E⌉; ⌈R⌉; ⌈λe,e'. (e < e')⌉; ⌈P⌉])⋅ THEN Try (Complete (Auto))) }

1
.....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)

2
.....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)))

---

Latex:



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{}y:E.  (((P  x)  \mwedge{}  (P  y))  {}\mRightarrow{}  (R  x  y  \mLeftarrow{}{}\mRightarrow{}  (x  <  y)))


By

((InstLemma  `cond\_rel\_equivalent`  [\mkleeneopen{}E\mkleeneclose{};  \mkleeneopen{}R\mkleeneclose{};  \mkleeneopen{}\mlambda{}e,e'.  (e  <  e')\mkleeneclose{};  \mkleeneopen{}P\mkleeneclose{}])\mcdot{}  THEN  Try  (Complete  (Auto)))

---

Home Index