Step
*
1
2
of Lemma
fun-connected_transitivity
1. [T] : Type
2. f : T ⟶ T
3. x : T
4. y : T
5. z : T
6. u : T
7. v : T List
8. y=f*(x) via [u / v]
9. L : T List
10. z=f*(y) via L
⊢ ∃L:T List. z=f*(x) via L
BY
{ ((InstLemma `last_lemma` [⌜T⌝;⌜L⌝]⋅ THENA (Auto THEN DVar `L' THEN RepUR ``fun-path`` -1 THEN Reduce 0 THEN Auto'))
THEN ExRepD
) }
1
1. [T] : Type
2. f : T ⟶ T
3. x : T
4. y : T
5. z : T
6. u : T
7. v : T List
8. y=f*(x) via [u / v]
9. L : T List
10. z=f*(y) via L
11. L' : T List
12. L = (L' @ [last(L)]) ∈ (T List)
⊢ ∃L:T List. z=f*(x) via L
Latex:
Latex:
1. [T] : Type
2. f : T {}\mrightarrow{} T
3. x : T
4. y : T
5. z : T
6. u : T
7. v : T List
8. y=f*(x) via [u / v]
9. L : T List
10. z=f*(y) via L
\mvdash{} \mexists{}L:T List. z=f*(x) via L
By
Latex:
((InstLemma `last\_lemma` [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
THENA (Auto THEN DVar `L' THEN RepUR ``fun-path`` -1 THEN Reduce 0 THEN Auto')
)
THEN ExRepD
)
Home
Index