Step
*
1
of Lemma
strict-sorted
1. T : Type
2. T ⊆r ℤ
3. as : T List
4. sorted(as)
5. no_repeats(T;as)
6. i : ℕ||as||
7. j : ℕi
⊢ as[j] < as[i]
BY
{ xxx(Unfold `sorted` 4
THEN (InstHyp [⌜i⌝; ⌜j⌝] 4)⋅
THEN Auto
THEN Unfold `no_repeats` 5
THEN (InstHyp [⌜i⌝; ⌜j⌝] 5)⋅
THEN Auto')xxx }
1
1. T : Type
2. T ⊆r ℤ
3. as : T List
4. ∀i:ℕ||as||. ∀j:ℕi. (as[j] ≤ as[i])
5. ∀[i,j:ℕ]. (¬(as[i] = as[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||as|| and i < ||as||)
6. i : ℕ||as||
7. j : ℕi
8. as[j] ≤ as[i]
9. ¬(as[i] = as[j] ∈ T)
⊢ as[j] < as[i]
Latex:
Latex:
1. T : Type
2. T \msubseteq{}r \mBbbZ{}
3. as : T List
4. sorted(as)
5. no\_repeats(T;as)
6. i : \mBbbN{}||as||
7. j : \mBbbN{}i
\mvdash{} as[j] < as[i]
By
Latex:
xxx(Unfold `sorted` 4
THEN (InstHyp [\mkleeneopen{}i\mkleeneclose{}; \mkleeneopen{}j\mkleeneclose{}] 4)\mcdot{}
THEN Auto
THEN Unfold `no\_repeats` 5
THEN (InstHyp [\mkleeneopen{}i\mkleeneclose{}; \mkleeneopen{}j\mkleeneclose{}] 5)\mcdot{}
THEN Auto')xxx
Home
Index