---

Step * 1 2 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))
⊢ ∀[x,y,z:Dom].  (TC(λa,b.Q a b)(x,y) ⇒ TC(λa,b.Q a b)(y,z) ⇒ TC(λa,b.Q a b)(x,z))
BY
{ Repeat (First [FOAllIntro; FOImpliesIntro])⋅ }

1
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)

---

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))
\mvdash{}  \mforall{}[x,y,z:Dom].    (TC(\mlambda{}a,b.Q  a  b)(x,y)  {}\mRightarrow{}  TC(\mlambda{}a,b.Q  a  b)(y,z)  {}\mRightarrow{}  TC(\mlambda{}a,b.Q  a  b)(x,z))


By

Repeat  (First  [FOAllIntro;  FOImpliesIntro])\mcdot{}

---

Home Index