---

Step * 1 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
{ (InstLemma `transitive-closure-induction` [⌈Dom⌉;⌈λ2x.B x⌉;⌈λ2x y.R x y⌉]⋅ THENA Auto) }

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
9. ∀x,y:Dom.  ((x TC(λ2x y.R x y) y) ⇒ (B x) ⇒ (B y))
⊢ 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

(InstLemma  `transitive-closure-induction`  [\mkleeneopen{}Dom\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.B  x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.R  x  y\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index