---

Step * 1 2 1 1 4 1 2 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)))))
10. x : Dom@i
11. y : Dom@i
12. z : Dom@i
13. z1 : Dom@i
14. R x z1@i
15. TC(λa,b.R a b)(z1,y)@i
16. z@0 : Dom@i
17. R y z@0@i
18. TC(λa,b.R a b)(z@0,z)@i
⊢ TC(λa,b.R a b)(z1,z)
BY
{ Assert ⌈TC(λa,b.R a b)(y,z@0)⌉⋅ }

1
.....assertion..... 
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. z1 : Dom@i
14. R x z1@i
15. TC(λa,b.R a b)(z1,y)@i
16. z@0 : Dom@i
17. R y z@0@i
18. TC(λa,b.R a b)(z@0,z)@i
⊢ TC(λa,b.R a b)(y,z@0)

2
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. z1 : Dom@i
14. R x z1@i
15. TC(λa,b.R a b)(z1,y)@i
16. z@0 : Dom@i
17. R y z@0@i
18. TC(λa,b.R a b)(z@0,z)@i
19. TC(λa,b.R a b)(y,z@0)
⊢ TC(λa,b.R a b)(z1,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)))))
10.  x  :  Dom@i
11.  y  :  Dom@i
12.  z  :  Dom@i
13.  z1  :  Dom@i
14.  R  x  z1@i
15.  TC(\mlambda{}a,b.R  a  b)(z1,y)@i
16.  z@0  :  Dom@i
17.  R  y  z@0@i
18.  TC(\mlambda{}a,b.R  a  b)(z@0,z)@i
\mvdash{}  TC(\mlambda{}a,b.R  a  b)(z1,z)


By

Assert  \mkleeneopen{}TC(\mlambda{}a,b.R  a  b)(y,z@0)\mkleeneclose{}\mcdot{}

---

Home Index