Step * of Lemma TC-min

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

1
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


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