---

Step * of Lemma rel_star_closure

∀[T:Type]. ∀[R,R2:T ⟶ T ⟶ ℙ].
  (Trans(T)(R2[_1;_2]) ⇒ (∀x,y:T.  ((x R y) ⇒ (x R2 y))) ⇒ (∀x,y:T.  ((x (R^*) y) ⇒ ((x R2 y) ∨ (x = y ∈ T)))))
BY
{ TACTIC:(Auto
          THEN RepUR ``rel_star`` (-1)
          THEN ExRepD
          THEN MoveToConcl (-1)
          THEN RepeatFor 2 (MoveToConcl (-2))
          THEN NatInd (-1)
          THEN Auto
          THEN Try ((ReduceExp (-1) THEN Auto))
          THEN ((MoveToConcl (-1) THEN RecUnfold `rel_exp` 0)
                THEN SplitOnConclITE
                THEN Auto
                THEN Reduce (-1)
                THEN ExRepD)⋅) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [R2] : T ⟶ T ⟶ ℙ
4. Trans(T)(R2[_1;_2])
5. ∀x,y:T.  ((x R y) ⇒ (x R2 y))
6. n : ℤ@i
7. [%3] : 0 < n@i
8. ∀x,y:T.  ((x R^n - 1 y) ⇒ ((x R2 y) ∨ (x = y ∈ T)))
9. x : T@i
10. y : T@i
11. ¬(n = 0 ∈ ℤ)
12. z : T@i
13. x R z
14. z R^n - 1 y
⊢ (x R2 y) ∨ (x = y ∈ T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (Trans(T)(R2[$_{1}$;$_{2}$])
    {}\mRightarrow{}  (\mforall{}x,y:T.    ((x  R  y)  {}\mRightarrow{}  (x  R2  y)))
    {}\mRightarrow{}  (\mforall{}x,y:T.    ((x  rel\_star(T;  R)  y)  {}\mRightarrow{}  ((x  R2  y)  \mvee{}  (x  =  y)))))


By

---

Latex:
TACTIC:(Auto
                THEN  RepUR  ``rel\_star``  (-1)
                THEN  ExRepD
                THEN  MoveToConcl  (-1)
                THEN  RepeatFor  2  (MoveToConcl  (-2))
                THEN  NatInd  (-1)
                THEN  Auto
                THEN  Try  ((ReduceExp  (-1)  THEN  Auto))
                THEN  ((MoveToConcl  (-1)  THEN  RecUnfold  `rel\_exp`  0)
                            THEN  SplitOnConclITE
                            THEN  Auto
                            THEN  Reduce  (-1)
                            THEN  ExRepD)\mcdot{})

---

Home Index