---

Step * 1 of Lemma TC-ind


1. [Dom] : Type
2. [B] : Dom ─→ ℙ
3. [R] : Dom ─→ Dom ─→ ℙ
4. ∀x,y:Dom.  ((R x y) ⇒ (B x) ⇒ (B y))@i
5. x : Dom@i
6. y : Dom@i
7. TC(λa,b.R a b)(x,y)@i
8. B x@i
⊢ B y
BY
{ Unfold `TC` (-2) }

1
1. [Dom] : Type
2. [B] : Dom ─→ ℙ
3. [R] : Dom ─→ Dom ─→ ℙ
4. ∀x,y:Dom.  ((R x y) ⇒ (B x) ⇒ (B y))@i
5. x : Dom@i
6. y : Dom@i
7. TC(λa,b. (R a b)) x y@i
8. B x@i
⊢ B y

---

Latex:



1.  [Dom]  :  Type
2.  [B]  :  Dom  {}\mrightarrow{}  \mBbbP{}
3.  [R]  :  Dom  {}\mrightarrow{}  Dom  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x,y:Dom.    ((R  x  y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y))@i
5.  x  :  Dom@i
6.  y  :  Dom@i
7.  TC(\mlambda{}a,b.R  a  b)(x,y)@i
8.  B  x@i
\mvdash{}  B  y


By

Unfold  `TC`  (-2)

---

Home Index