---

Step * 2 of Lemma rel_exp_monotone

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

---

Latex:

---

Latex:
.....upcase..... 
1.  n  :  \mBbbZ{}
2.  [\%1]  :  0  <  n
3.  \mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (R1  =>  R2  {}\mRightarrow{}  rel\_exp(T;  R1;  n  -  1)  =>  rel\_exp(T;  R2;  n  -  1))
\mvdash{}  \mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (R1  =>  R2  {}\mRightarrow{}  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  `rel\_implies`)
      )
    THEN  All  Reduce
    )
  THEN  Auto
  )

---

Home Index