---

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


9. ∀x,y:Dom.  ((P x y) ⇒ (Q x y))@i
10. ∀x,y:Dom.  ((P x y) ⇒ TC(λa,b.Q a b)(x,y))
11. [x] : Dom
12. [y] : Dom
13. [z] : Dom
14. TC(λa,b.Q a b)(x,y)@i
15. TC(λa,b.Q a b)(y,z)@i
⊢ TC(λa,b.Q a b)(x,z)
BY
{ TCTrans (-1) (-2) }

---

Latex:



9.  \mforall{}x,y:Dom.    ((P  x  y)  {}\mRightarrow{}  (Q  x  y))@i
10.  \mforall{}x,y:Dom.    ((P  x  y)  {}\mRightarrow{}  TC(\mlambda{}a,b.Q  a  b)(x,y))
11.  [x]  :  Dom
12.  [y]  :  Dom
13.  [z]  :  Dom
14.  TC(\mlambda{}a,b.Q  a  b)(x,y)@i
15.  TC(\mlambda{}a,b.Q  a  b)(y,z)@i
\mvdash{}  TC(\mlambda{}a,b.Q  a  b)(x,z)


By

TCTrans  (-1)  (-2)

---

Home Index