---

Step * 1 2 1 of Lemma ancestral-logic-lemma1


9. ∀x,y:Dom.  ((R x y) ⇒ ((R x y) ∨ (∃z:Dom. ((R x z) ∧ TC(λa,b.R a b)(z,y)))))
⊢ ∀x,y,z:Dom.
    (((R x y) ∨ (∃z:Dom. ((R x z) ∧ TC(λa,b.R a b)(z,y))))
    ⇒ ((R y z) ∨ (∃z@0:Dom. ((R y z@0) ∧ TC(λa,b.R a b)(z@0,z))))
    ⇒ ((R x z) ∨ (∃z@0:Dom. ((R x z@0) ∧ TC(λa,b.R a b)(z@0,z)))))
BY
{ RepeatFor 5 (First [FOAllIntro; FOImpliesIntro]) }

1
9. ∀x,y:Dom.  ((R x y) ⇒ ((R x y) ∨ (∃z:Dom. ((R x z) ∧ TC(λa,b.R a b)(z,y)))))
10. x : Dom@i
11. y : Dom@i
12. z : Dom@i
13. (R x y) ∨ (∃z:Dom. ((R x z) ∧ TC(λa,b.R a b)(z,y)))@i
14. (R y z) ∨ (∃z@0:Dom. ((R y z@0) ∧ TC(λa,b.R a b)(z@0,z)))@i
⊢ (R x z) ∨ (∃z@0:Dom. ((R x z@0) ∧ TC(λa,b.R a b)(z@0,z)))

---

Latex:



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


By

RepeatFor  5  (First  [FOAllIntro;  FOImpliesIntro])

---

Home Index