---

Step * 2 1 1 of Lemma rel_inverse_star


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. y : T
5. n : ℕ
6. x R^-1^n y
⊢ y R^n x
BY
{ ((((RWO "rel_inverse_exp<" (-1) THENA Auto{1,1000}-1) THEN Unfold `rel_inverse` (-1)) THEN Reduce (-1))
   THEN Auto{1,4}-1
   ) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  x  :  T
4.  y  :  T
5.  n  :  \mBbbN{}
6.  x  rel\_exp(T;  R\^{}-1;  n)  y
\mvdash{}  y  rel\_exp(T;  R;  n)  x


By

---

Latex:
((((RWO  "rel\_inverse\_exp<"  (-1)  THENA  Auto\{1,1000\}-1)  THEN  Unfold  `rel\_inverse`  (-1))
    THEN  Reduce  (-1)
    )
  THEN  Auto\{1,4\}-1
  )

---

Home Index