Step
*
1
of Lemma
rel-star-iff-rel-plus-or
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T@i
4. y : T@i
5. ∃n:ℕ. (x R^n y)@i
⊢ (∃n:ℕ+. (x R^n y)) ∨ (x = y ∈ T)
BY
{ (((ExRepD THEN CaseNat 0 `n') THENL [OrRight; OrLeft]) THEN Auto) }
1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. x : T@i
4. y : T@i
5. n : ℕ@i
6. x R^n y@i
7. n = 0 ∈ ℤ
⊢ x = y ∈ T
Latex:
Latex:
1. [T] : Type
2. [R] : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
3. x : T@i
4. y : T@i
5. \mexists{}n:\mBbbN{}. (x rel\_exp(T; R; n) y)@i
\mvdash{} (\mexists{}n:\mBbbN{}\msupplus{}. (x rel\_exp(T; R; n) y)) \mvee{} (x = y)
By
Latex:
(((ExRepD THEN CaseNat 0 `n') THENL [OrRight; OrLeft]) THEN Auto)
Home
Index