---

Step * of Lemma rel_star_monotone

∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (R1 => R2 ⇒ R1^* => R2^*)
BY
{ (((((((Unfolds ``rel_star rel_implies`` 0 THEN Reduce 0) THEN Auto) THEN ParallelOp (-1)) THEN MoveToConcl (-1))
     THEN MoveToConcl (-2)
     )
    THEN MoveToConcl (-2)
    )
   THEN All (Fold `rel_implies`)
   ) }

1
1. [T] : Type
2. [R1] : T ⟶ T ⟶ ℙ
3. [R2] : T ⟶ T ⟶ ℙ
4. R1 => R2
5. n : ℕ
⊢ R1^n => R2^n

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (R1  =>  R2  {}\mRightarrow{}  rel\_star(T;  R1)  =>  rel\_star(T;  R2))


By

---

Latex:
(((((((Unfolds  ``rel\_star  rel\_implies``  0  THEN  Reduce  0)  THEN  Auto)  THEN  ParallelOp  (-1))
        THEN  MoveToConcl  (-1)
        )
      THEN  MoveToConcl  (-2)
      )
    THEN  MoveToConcl  (-2)
    )
  THEN  All  (Fold  `rel\_implies`)
  )

---

Home Index