Step
*
1
1
of Lemma
ranked-eo-locl
1. i : Id
2. L : Id ─→ (Top List)
3. rk : (i:Id × ℕ||L i||) ─→ ℕ
4. ∀i:Id. ∀j:ℕ||L i||. ∀k:ℕj. rk <i, k> < rk <i, j>
5. i1 : Id
6. a1 : ℕ||L i||
7. True
8. b1 : ℕ||L i||
9. True
10. i1 = i ∈ Id
11. rk <i, a1> < rk <i, b1>
12. b1 < a1
⊢ a1 < b1
BY
{ ((Assert rk <i, b1> < rk <i, a1> BY Auto) THEN Auto') }
Latex:
Latex:
1. i : Id
2. L : Id {}\mrightarrow{} (Top List)
3. rk : (i:Id \mtimes{} \mBbbN{}||L i||) {}\mrightarrow{} \mBbbN{}
4. \mforall{}i:Id. \mforall{}j:\mBbbN{}||L i||. \mforall{}k:\mBbbN{}j. rk <i, k> < rk <i, j>
5. i1 : Id
6. a1 : \mBbbN{}||L i||
7. True
8. b1 : \mBbbN{}||L i||
9. True
10. i1 = i
11. rk <i, a1> < rk <i, b1>
12. b1 < a1
\mvdash{} a1 < b1
By
Latex:
((Assert rk <i, b1> < rk <i, a1> BY Auto) THEN Auto')
Home
Index