---

Step * 1 of Lemma TC-min-uniform


1. [Dom] : Type
2. [R] : Dom ─→ Dom ─→ ℙ
3. [Q] : Dom ─→ Dom ─→ ℙ
4. ∀[x,y,z:Dom].  ((Q x y) ⇒ (Q y z) ⇒ (Q x z))@i
5. ∀x,y:Dom.  ((R x y) ⇒ (Q x y))@i
6. x : Dom@i
7. y : Dom@i
8. TC(λa,b. (R a b)) x y@i
9. TC(λx,y. (R x y)) => λx,y. (Q x y)
⊢ Q x y
BY
{ (((With ⌈x⌉ (D (-1))⋅ THENM (Reduce (-1) THEN BHyp -1 )) THENA Auto) THEN Unfold `infix_ap` 0 THEN Auto)⋅ }

---

Latex:



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


By

(((With  \mkleeneopen{}x\mkleeneclose{}  (D  (-1))\mcdot{}  THENM  (Reduce  (-1)  THEN  BHyp  -1  ))  THENA  Auto)
  THEN  Unfold  `infix\_ap`  0
  THEN  Auto)\mcdot{}

---

Home Index