Step * 1 of Lemma TC-min-uniform


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