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


9. ∀x,y:Dom.  (TC(λa,b.P b)(x,y)  TC(λa,b.P b)(x,y))
⊢ ∀[x,y,z:Dom].  (TC(λa,b.P b)(x,y)  TC(λa,b.P b)(y,z)  TC(λa,b.P b)(x,z))
BY
RepeatFor ((FOAllIntro ORELSE FOImpliesIntro)) }

1
9. ∀x,y:Dom.  (TC(λa,b.P b)(x,y)  TC(λa,b.P b)(x,y))
10. [x] Dom
11. [y] Dom
12. [z] Dom
13. TC(λa,b.P b)(x,y)@i
14. TC(λa,b.P b)(y,z)@i
⊢ TC(λa,b.P 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