---

Step * of Lemma cond_rel_star_monotone

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

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. [R1] : T ⟶ T ⟶ ℙ
4. [R2] : T ⟶ T ⟶ ℙ
5. when P, R1 => R2
6. R1 preserves P
7. n : ℕ
⊢ when P, R1^n => R2^n

---

Latex:

---

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


By

---

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

---

Home Index