---

Step * of Lemma TC-min

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

1
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

---

Latex:


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


By

(Auto
  THEN  Unfold  `TC`  -1
  THEN  (InstLemma  `transitive-closure-minimal`  [\mkleeneopen{}Dom\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.R  x  y\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.Q  x  y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  All  (Unfold  `so\_lambda`)
  THEN  Try  ((D  0  THEN  Reduce  0  THEN  Auto)\mcdot{}))

---

Home Index