Step
*
3
of Lemma
rel-star-iff-rel-plus-or
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T@i
4. y : T@i
5. x = y ∈ T@i
⊢ ∃n:ℕ. (x R^n y)
BY
{ ((InstConcl [⌜0⌝])⋅ THEN Auto THEN RecUnfold `rel_exp` 0 THEN Reduce 0 THEN Auto) }
Latex:
Latex:
1. [T] : Type
2. [R] : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
3. x : T@i
4. y : T@i
5. x = y@i
\mvdash{} \mexists{}n:\mBbbN{}. (x rel\_exp(T; R; n) y)
By
Latex:
((InstConcl [\mkleeneopen{}0\mkleeneclose{}])\mcdot{} THEN Auto THEN RecUnfold `rel\_exp` 0 THEN Reduce 0 THEN Auto)
Home
Index