---

Step * of Lemma cond_rel_star_monotonic

∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ].
  (when P, R1 => R2 ⇒ R1 preserves P ⇒ (∀x,y:T.  ((P x) ⇒ (x (R1^*) y) ⇒ (x (R2^*) y))))
BY
{ ((((Auto THEN (Assert when P, R1^* => R2^* BY (BackThruLemma `cond_rel_star_monotone` THEN Auto)))
     THEN Unfold `cond_rel_implies` (-1)
     )
    THEN BackThruHyp (-1)
    )
   THEN Auto
   ) }

---

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{}  (\mforall{}x,y:T.    ((P  x)  {}\mRightarrow{}  (x  (R1\^{}*)  y)  {}\mRightarrow{}  (x  (R2\^{}*)  y))))


By

---

Latex:
((((Auto  THEN  (Assert  when  P,  R1\^{}*  =>  R2\^{}*  BY  (BackThruLemma  `cond\_rel\_star\_monotone`  THEN  Auto)))
      THEN  Unfold  `cond\_rel\_implies`  (-1)
      )
    THEN  BackThruHyp  (-1)
    )
  THEN  Auto
  )

---

Home Index