---

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


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

---

Latex:



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


By

TCTrans  (-1)  (-2)

---

Home Index