---

Step * of Lemma ancestral-logic-lemma1

∀x,y:Dom.  (TC(λa,b.R a b)(x,y) ⇒ ((R x y) ∨ (∃z:Dom. ((R x z) ∧ TC(λa,b.R a b)(z,y)))))
BY
{ StartFO }

1
⊢ ∀x,y:Dom.  (TC(λa,b.R a b)(x,y) ⇒ ((R x y) ∨ (∃z:Dom. ((R x z) ∧ TC(λa,b.R a b)(z,y)))))

---

Latex:


\mforall{}x,y:Dom.    (TC(\mlambda{}a,b.R  a  b)(x,y)  {}\mRightarrow{}  ((R  x  y)  \mvee{}  (\mexists{}z:Dom.  ((R  x  z)  \mwedge{}  TC(\mlambda{}a,b.R  a  b)(z,y)))))


By

StartFO

---

Home Index