---

Step * 1 of Lemma ancestral-logic-example2


⊢ ∀x,y:Dom.  (TC(λa,b.TC(λi,j.P i j)(a,b))(x,y) ⇒ TC(λa,b.P a b)(x,y))
BY
{ Assert ⌈∀x,y:Dom.  (TC(λa,b.P a b)(x,y) ⇒ TC(λa,b.P a b)(x,y))⌉⋅ }

1
.....assertion..... 
⊢ ∀x,y:Dom.  (TC(λa,b.P a b)(x,y) ⇒ TC(λa,b.P a b)(x,y))

2
9. ∀x,y:Dom.  (TC(λa,b.P a b)(x,y) ⇒ TC(λa,b.P a b)(x,y))
⊢ ∀x,y:Dom.  (TC(λa,b.TC(λi,j.P i j)(a,b))(x,y) ⇒ TC(λa,b.P a b)(x,y))

---

Latex:



\mvdash{}  \mforall{}x,y:Dom.    (TC(\mlambda{}a,b.TC(\mlambda{}i,j.P  i  j)(a,b))(x,y)  {}\mRightarrow{}  TC(\mlambda{}a,b.P  a  b)(x,y))


By

Assert  \mkleeneopen{}\mforall{}x,y:Dom.    (TC(\mlambda{}a,b.P  a  b)(x,y)  {}\mRightarrow{}  TC(\mlambda{}a,b.P  a  b)(x,y))\mkleeneclose{}\mcdot{}

---

Home Index