---

Step * 1 1 of Lemma ancestral-logic-induction


9. ∀x,y:Dom.  ((R x y) ⇒ (B x) ⇒ (B y))@i
⊢ ∀x,y:Dom.  (TC(λa,b.R a b)(x,y) ⇒ (B x) ⇒ (B y))
BY
{ TCMinUniform 9 }

1
9. ∀x,y:Dom.  ((R x y) ⇒ (B x) ⇒ (B y))@i
⊢ ∀[x,y,z:Dom].  (((B x) ⇒ (B y)) ⇒ ((B y) ⇒ (B z)) ⇒ (B x) ⇒ (B z))

2
9. ∀x,y:Dom.  ((R x y) ⇒ (B x) ⇒ (B y))@i
10. ∀x,y:Dom.  (TC(λa,b.R a b)(x,y) ⇒ (B x) ⇒ (B y))
⊢ ∀x,y:Dom.  (TC(λa,b.R a b)(x,y) ⇒ (B x) ⇒ (B y))

---

Latex:



9.  \mforall{}x,y:Dom.    ((R  x  y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y))@i
\mvdash{}  \mforall{}x,y:Dom.    (TC(\mlambda{}a,b.R  a  b)(x,y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y))


By

TCMinUniform  9

---

Home Index