---

Step * of Lemma TC-base

∀[Dom:Type]. ∀[R:Dom ─→ Dom ─→ ℙ].  ∀x,y:Dom.  ((R x y) ⇒ TC(λa,b.R a b)(x,y))
BY
{ (Auto
   THEN All (Unfold `TC`)
   THEN (InstLemma `transitive-closure-contains` [⌈Dom⌉;⌈λ2x y.R x y⌉]⋅ THENA Auto)
   THEN Unfold `so_lambda` (-1)
   THEN All (Fold `infix_ap`)
   THEN Auto) }

---

Latex:


\mforall{}[Dom:Type].  \mforall{}[R:Dom  {}\mrightarrow{}  Dom  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y:Dom.    ((R  x  y)  {}\mRightarrow{}  TC(\mlambda{}a,b.R  a  b)(x,y))


By

(Auto
  THEN  All  (Unfold  `TC`)
  THEN  (InstLemma  `transitive-closure-contains`  [\mkleeneopen{}Dom\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.R  x  y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `so\_lambda`  (-1)
  THEN  All  (Fold  `infix\_ap`)
  THEN  Auto)

---

Home Index