---

Step * of Lemma rel_plus_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))))
BY
{ (Auto
   THEN (Unfold `rel_plus` (-1))
   THEN (Reduce (-1))
   THEN ExRepD
   THEN (PromoteHyp (-2) (-4))
   THEN RepeatFor 4 ((MoveToConcl (-1)))
   THEN InductionOnNat
   THEN Auto
   THEN Try (((RW (RelExp1C) (-1)) THEN Auto))) }

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 : ℤ
7. 0 < n
8. ∀x,y:T.  ((x R^n y) ⇒ (x R2 y))
9. x : T
10. y : T
11. x R^n + 1 y
⊢ x R2 y

---

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  R\000C2  y)))  {}\mRightarrow{}  (\mforall{}x,y:T.    ((x  R\msupplus{}  y)  {}\mRightarrow{}  (x  R2  y))))


By

---

Latex:
(Auto
  THEN  (Unfold  `rel\_plus`  (-1))
  THEN  (Reduce  (-1))
  THEN  ExRepD
  THEN  (PromoteHyp  (-2)  (-4))
  THEN  RepeatFor  4  ((MoveToConcl  (-1)))
  THEN  InductionOnNat
  THEN  Auto
  THEN  Try  (((RW  (RelExp1C)  (-1))  THEN  Auto)))

---

Home Index