---

Step * of 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)))))
BY
{ RepeatFor 6 ((D 0 THENA Auto)) }

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

---

Latex:

---

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


By

---

Latex:
RepeatFor  6  ((D  0  THENA  Auto))

---

Home Index