Step
*
1
2
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))
⊢ ∀[x,y,z:Dom].  (TC(λa,b.P a b)(x,y) 
⇒ TC(λa,b.P a b)(y,z) 
⇒ TC(λa,b.P a b)(x,z))
BY
{ RepeatFor 5 ((FOAllIntro ORELSE FOImpliesIntro)) }
1
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)
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))
\mvdash{}  \mforall{}[x,y,z:Dom].    (TC(\mlambda{}a,b.P  a  b)(x,y)  {}\mRightarrow{}  TC(\mlambda{}a,b.P  a  b)(y,z)  {}\mRightarrow{}  TC(\mlambda{}a,b.P  a  b)(x,z))
By
RepeatFor  5  ((FOAllIntro  ORELSE  FOImpliesIntro))
Home
Index