---

Step * of Lemma rel_exp_one

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x R^1 y ⇐⇒ x R y)
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "rel_exp_iff" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN SplitOrHyps
   THEN Auto
   THEN ExRepD) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. y : T
5. z : T
6. 0 < 1
7. x R^0 z
8. z R y
⊢ x R y

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. y : T
5. x R y
⊢ (∃z:T. (0 < 1 c∧ ((x R^0 z) ∧ (z R y)))) ∨ ((1 = 0 ∈ ℤ) ∧ (x = y ∈ T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y:T.    (x  rel\_exp(T;  R;  1)  y  \mLeftarrow{}{}\mRightarrow{}  x  R  y)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "rel\_exp\_iff"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  ExRepD)

---

Home Index