---

Step * 2 of Lemma cond_rel_exp_monotone

.....upcase..... 
1. n : ℤ
2. [%1] : 0 < n
3. ∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (when P, R1 => R2 ⇒ R1 preserves P ⇒ when P, R1^n - 1 => R2^n - 1)
⊢ ∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (when P, R1 => R2 ⇒ R1 preserves P ⇒ when P, R1^n => R2^n)
BY
{ ((((((Auto THEN RecUnfold `rel_exp` 0) THEN SplitOnConclITE) THEN Auto) THEN All (Unfold `cond_rel_implies`))
    THEN All Reduce
    )
   THEN Auto
   ) }

---

Latex:

---

Latex:
.....upcase..... 
1.  n  :  \mBbbZ{}
2.  [\%1]  :  0  <  n
3.  \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\_exp(T;  R1;  n  -  1)  =>  rel\_exp(T;  R2;  n  -  1))
\mvdash{}  \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\_exp(T;  R1;  n)  =>  rel\_exp(T;  R2;  n))


By

---

Latex:
((((((Auto  THEN  RecUnfold  `rel\_exp`  0)  THEN  SplitOnConclITE)  THEN  Auto)
      THEN  All  (Unfold  `cond\_rel\_implies`)
      )
    THEN  All  Reduce
    )
  THEN  Auto
  )

---

Home Index