Mercurial > hg > Members > kono > Proof > prob1
annotate prob1.agda @ 29:24864ed3b6d3
change to uniquness
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 30 Mar 2020 17:25:06 +0900 |
| parents | 8ef3eecd159f |
| children | 7256d3d032e4 |
| rev | line source |
|---|---|
|
0
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 module prob1 where |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import Relation.Binary.PropositionalEquality |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import Relation.Binary.Core |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import Data.Nat |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import Data.Nat.Properties |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import logic |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import nat |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import Data.Empty |
| 14 | 10 open import Data.Product |
|
0
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 open import Relation.Nullary |
| 20 | 12 -- open import Relation.Binary.Definitions |
| 19 | 13 |
|
0
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 -- All variables are positive integer |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 -- A = -M*n + i +k*M - M |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 -- where n is in range (0,…,k-1) and i is in range(0,…,M-1) |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 -- Goal: Prove that A can take all values of (0,…,k*M-1) |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 -- A1 = -M*n1 + i1 +k*M M, A2 = -M*n2 + i2 +k*M - M |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 -- (1) If n1!=n2 or i1!=i2 then A1!=A2 |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 -- Or its contraposition: (2) if A1=A2 then n1=n2 and i1=i2 |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 -- Proof by contradiction: Suppose A1=A2 and (n1!=n2 or i1!=i2) becomes |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 -- contradiction |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 -- Induction on n and i |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 record Cond1 (A M k : ℕ ) : Set where |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 field |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 n : ℕ |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 i : ℕ |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 range-n : n < k |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 range-i : i < M |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 rule1 : i + k * M ≡ M * (suc n) + A -- A ≡ (i + k * M ) - (M * (suc n)) |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 -- k = 1 → n = 0 → ∀ M → A = i |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 -- k = 2 → n = 1 → |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 -- i + 2 * M = M * (suc n) + A i = suc n → A = 0 |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 |
| 26 | 37 record UCond1 (A M k : ℕ ) : Set where |
| 38 field | |
| 39 c1 : Cond1 A M k | |
| 29 | 40 unique-i : {j : ℕ} {m1 : ℕ} → j < M → m1 < k → j + k * M ≡ M * suc m1 + A → Cond1.i c1 ≡ j |
| 41 unique-n : {j : ℕ} {m1 : ℕ} → j < M → m1 < k → j + k * M ≡ M * suc m1 + A → Cond1.n c1 ≡ m1 | |
| 18 | 42 |
| 26 | 43 problem1-0 : (k A M : ℕ ) → (A<kM : suc A < k * M ) |
| 44 → UCond1 A M k | |
| 45 problem1-0 zero A M () | |
| 46 problem1-0 (suc k) A zero A<kM = ⊥-elim ( nat-<> A<kM (subst (λ x → x < suc A) (*-comm _ k ) 0<s )) | |
| 47 problem1-0 (suc k) A (suc m) A<kM = cc k a<sa (start-range k) where | |
| 13 | 48 M = suc m |
| 14 | 49 cck : ( n : ℕ ) → n < suc k → (suc A > ((k - n) ) * M ) → A - ((k - n) * M) < M → Cond1 A M (suc k) |
| 50 cck n n<k gt lt = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = lt ; rule1 = lemma2 } where | |
| 51 lemma2 : A - ((k - n) * M) + suc k * M ≡ M * suc n + A | |
| 5 | 52 lemma2 = begin |
| 14 | 53 A - ((k - n) * M) + suc k * M ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (sym (minus+n {k} {n} n<k )) ⟩ |
| 54 A - ((k - n) * M) + (suc (((k - n) ) + n )) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (+-comm _ n) ⟩ | |
| 55 A - ((k - n) * M) + (suc (n + ((k - n) ) )) * M ≡⟨⟩ | |
| 56 A - ((k - n) * M) + (suc n + ((k - n) ) ) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + x * M ) (+-comm (suc n) _) ⟩ | |
| 57 A - ((k - n) * M) + (((k - n) ) + suc n ) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + x ) (((proj₂ *-distrib-+)) M ((k - n)) _ ) ⟩ | |
| 58 A - ((k - n) * M) + (((k - n) * M) + (suc n) * M) ≡⟨ sym (+-assoc (A - ((k - n) * M)) _ ((suc n) * M)) ⟩ | |
| 59 A - ((k - n) * M) + ((k - n) * M) + (suc n) * M ≡⟨ cong ( λ x → x + (suc n) * M ) ( minus+n {A} {(k - n) * M} gt ) ⟩ | |
| 5 | 60 A + (suc n) * M ≡⟨ cong ( λ k → A + k ) (*-comm (suc n) _ ) ⟩ |
| 61 A + M * (suc n) ≡⟨ +-comm A _ ⟩ | |
| 62 M * (suc n) + A | |
| 63 ∎ where open ≡-Reasoning | |
| 26 | 64 cck-u : ( n : ℕ ) → n < suc k → (suc A > ((k - n) ) * M ) → A - ((k - n) * M) < M → UCond1 A M (suc k) |
| 65 cck-u n n<k k<A i<M = c0 where | |
| 21 | 66 c1 : Cond1 A M (suc k) |
| 26 | 67 c1 = cck n n<k k<A i<M |
| 24 | 68 lemma4 : {i j x y z : ℕ} → j + x ≡ y → i + x ≡ z → j < i → y < z |
| 69 lemma4 {i} {j} {x} refl refl (s≤s z≤n) = s≤s (subst (λ k → x ≤ k ) (+-comm x _) x≤x+y) | |
| 70 lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) ) | |
| 27 | 71 lemma5 : {m1 n : ℕ} → M * suc m1 + A < M * suc n + A |
| 24 | 72 → M + (M * suc m1 + A) ≤ M * suc n + A |
| 27 | 73 lemma5 {m1} {n} lt with <-cmp m1 n |
| 74 lemma5 {m1} {n} lt | tri< a ¬b ¬c = begin | |
| 25 | 75 M + (M * suc m1 + A) |
| 76 ≡⟨ sym (+-assoc M _ _ ) ⟩ | |
| 77 (M + M * suc m1) + A | |
| 78 ≡⟨ sym ( cong (λ k → (k + M * suc m1) + A) ((proj₂ *-identity) M )) ⟩ | |
| 79 (M * suc zero + M * suc m1) + A | |
| 80 ≡⟨ sym ( cong (λ k → k + A) (( proj₁ *-distrib-+ ) M (suc zero) _ )) ⟩ | |
| 81 M * suc (suc m1) + A | |
| 82 ≤⟨ ≤-plus {_} {_} {A} (subst₂ (λ x y → x ≤ y ) (*-comm _ M ) (*-comm _ M ) (*≤ (s≤s a))) ⟩ | |
| 83 M * suc n + A | |
| 84 ∎ where open ≤-Reasoning | |
| 27 | 85 lemma5 {m1} {n} lt | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<≡ lt ) |
| 86 lemma5 {m1} {n} lt | tri> ¬a ¬b c = ⊥-elim ( nat-<> lt (<-plus {_} {_} {A} (<≤+ (s≤s c) | |
| 25 | 87 (subst₂ (λ x y → x ≤ y ) (*-comm _ m ) (*-comm _ m ) (*≤ (s≤s (≤to< c))))))) |
| 24 | 88 lemma6 : {i j x : ℕ} → M + (j + x ) ≤ i + x → M ≤ i |
| 89 lemma6 {i} {j} {x} lt = ≤-minus {M} {i} {x} (x+y≤z→x≤z ( begin | |
| 90 M + x + j | |
| 91 ≡⟨ +-assoc M _ _ ⟩ | |
| 92 M + (x + j ) | |
| 93 ≡⟨ cong (λ k → M + k ) (+-comm x _ ) ⟩ | |
| 94 M + (j + x) | |
| 95 ≤⟨ lt ⟩ | |
| 96 i + x | |
| 97 ∎ )) where open ≤-Reasoning | |
| 27 | 98 i : ℕ |
| 99 i = A - ((k - n) * M) | |
| 100 lemma-u1 : {j : ℕ} {m1 : ℕ} → j < i → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A | |
| 23 | 101 lemma-u1 {j} {m1} j<akM m1<k eq with <-cmp j M |
| 24 | 102 lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c = |
| 103 ⊥-elim (nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym eq) (sym (Cond1.rule1 c1 )) (lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM ))) ) i<M ) where | |
| 27 | 104 lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A -- M + j ≤ i |
| 24 | 105 lemma3 = lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM) |
| 23 | 106 lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) |
| 107 lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM ) | |
| 27 | 108 lemma-u2 : {j : ℕ} {m1 : ℕ} → (A - ((k - n) * M)) < j → |
| 109 j < M → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A | |
| 110 lemma-u2 {j} {m1} i<j j<M m1<k eq = ⊥-elim ( nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym (Cond1.rule1 c1)) (sym eq) lemma3-2)) j<M ) where | |
| 111 lemma3-2 : M + (M * suc n + A) ≤ M * suc m1 + A -- M + i ≤ j | |
| 112 lemma3-2 = lemma5 (lemma4 (Cond1.rule1 c1) eq i<j) | |
| 28 | 113 unique-i : {j : ℕ} {m1 : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → i ≡ j |
| 114 unique-i {j} {m1} j<M m1<k eq with <-cmp i j | |
| 115 unique-i {j} {m1} j<M m1<k eq | tri< a ¬b ¬c = ⊥-elim ( lemma-u2 a j<M m1<k eq ) | |
| 116 unique-i {j} {m1} j<M m1<k eq | tri≈ ¬a b ¬c = b | |
| 117 unique-i {j} {m1} j<M m1<k eq | tri> ¬a ¬b c = ⊥-elim ( lemma-u1 c m1<k eq ) | |
| 118 lemma7 : {n m1 m A : ℕ} → n < m1 → suc (n + m * suc n + A) < suc (m1 + m * suc m1 + A) | |
| 119 lemma7 {n} {m1} {m} {A} n<m1 = begin | |
| 120 suc (suc (n + m * suc n + A)) | |
| 121 ≡⟨ +-assoc _ (m * suc n) A ⟩ | |
| 122 suc (suc n + (m * suc n + A)) | |
| 123 ≤⟨ s≤s (<-plus n<m1) ⟩ | |
| 124 suc (m1 + (m * suc n + A)) | |
| 125 ≡⟨ sym ( +-assoc _ (m * suc n) A) ⟩ | |
| 126 suc (m1 + m * suc n + A) | |
| 127 ≤⟨ ≤-plus {_} {_} {A} (≤-plus-0 {_} {_} {suc m1} (≤* {suc n} {suc m1} {m} (s≤s (≤to< n<m1 )))) ⟩ | |
| 128 suc (m1 + m * suc m1 + A) | |
| 129 ∎ where open ≤-Reasoning | |
| 130 unique-m : {i j : ℕ} {n m1 : ℕ} → i ≡ j → i + suc k * M ≡ M * suc n + A → j + suc k * M ≡ M * suc m1 + A → n ≡ m1 | |
| 131 unique-m {i} {_} {n} {m1} refl eqn eqm with <-cmp n m1 | |
| 132 unique-m {i} {_} {n} {m1} refl eqn eqm | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym (trans (sym eqm) eqn )) (lemma7 {n} {m1} {m} {A} a )) | |
| 133 unique-m {i} {_} {n} {m1} refl eqn eqm | tri≈ ¬a b ¬c = b | |
| 134 unique-m {i} {_} {n} {m1} refl eqn eqm | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (trans (sym eqm) eqn ) (lemma7 {m1} {n} {m} {A} c )) | |
| 135 m1<sk : {m1 : ℕ} → m1 < n → n < suc k → m1 < suc k | |
| 136 m1<sk {m1} m1<n n<k = <-trans m1<n n<k | |
| 137 lemma-u3 : {j : ℕ} {m₁ : ℕ} → j < M → m₁ < n → ¬ j + suc k * M ≡ M * suc m₁ + A | |
| 138 lemma-u3 {j} {m1} j<M m1<n eq = nat-≡< (unique-m (sym (unique-i j<M (m1<sk m1<n (Cond1.range-n c1) ) eq)) eq (Cond1.rule1 c1)) m1<n | |
| 139 lemma-u4 : {j : ℕ} {m₁ : ℕ} → j < M → n < m₁ → m₁ < suc k → ¬ j + suc k * M ≡ M * suc m₁ + A | |
| 140 lemma-u4 {j} {m1} j<M n<m1 m<sk eq = nat-≡< (unique-m (unique-i j<M m<sk eq) (Cond1.rule1 c1) eq ) n<m1 | |
| 29 | 141 unique-n : {j m1 : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → n ≡ m1 |
| 142 unique-n {j} {m1} j<M m1<k eq = unique-m (unique-i j<M m1<k eq ) (Cond1.rule1 c1) eq | |
| 27 | 143 c0 = record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = i<M; rule1 = Cond1.rule1 c1 } |
| 29 | 144 ; unique-i = unique-i |
| 145 ; unique-n = unique-n | |
| 27 | 146 } |
| 26 | 147 -- loop on range of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M |
| 148 nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M) | |
| 149 nextc n n<k with k - n | inspect (_-_ k) n | |
| 150 nextc n n<k | 0 | record { eq = e } = ⊥-elim ( nat-≡< (sym e) (minus>0 n<k) ) | |
| 151 nextc n n<k | suc n0 | _ = s≤s (s≤s lemma) where | |
| 152 lemma : m ≤ m + n0 * suc m | |
| 153 lemma = x≤x+y | |
| 20 | 154 cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → UCond1 A M (suc k) |
| 26 | 155 cc zero n<k k<A = cck-u 0 n<k k<A lemma where |
| 21 | 156 a<m : suc A < M + k * M |
| 157 a<m = A<kM | |
| 158 lemma : A - ((k - 0) * M) < M | |
| 159 lemma = <-minus {_} {_} {k * M} (subst (λ x → x < M + k * M) (sym (minus+n {A} {k * M} k<A )) (less-1 a<m) ) | |
| 17 | 160 cc (suc n) n<k k<A with <-cmp (A - ((k - (suc n)) * M)) M |
| 26 | 161 cc (suc n) n<k k<A | tri< a ¬b ¬c = cck-u (suc n) n<k k<A a |
| 20 | 162 cc (suc n) n<k k<A | tri≈ ¬a b ¬c = |
| 22 | 163 cc n (less-1 n<k) (lemma1 b) where |
| 164 a=mk0 : (A - ((k - (suc n)) * M)) ≡ M → A ≡ (k - n) * M | |
| 165 a=mk0 a=mk = sym ( begin | |
| 166 (k - n) * M | |
| 26 | 167 ≡⟨ sym ( minus+n {(k - n) * M} {M} (nextc n n<k )) ⟩ |
| 22 | 168 ((k - n) * M ) - M + M |
| 169 ≡⟨ +-comm _ M ⟩ | |
| 170 M + (((k - n) * M ) - M) | |
| 171 ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k} (<-minus-0 n<k ))) ⟩ | |
| 172 M + (k - (suc n) * M) | |
| 173 ≡⟨ cong (λ x → x + (k - (suc n)) * M) (sym a=mk) ⟩ | |
| 174 A - ((k - (suc n)) * M) + ((k - (suc n)) * M) | |
| 175 ≡⟨ minus+n {A} {(k - (suc n)) * M} k<A ⟩ | |
| 176 A | |
| 177 ∎ ) where open ≡-Reasoning | |
| 178 lemma1 : (A - ((k - (suc n)) * M)) ≡ M → suc A > (k - n) * M | |
| 179 lemma1 a=mk = subst (λ x → (k - n) * M < suc x ) (sym (a=mk0 a=mk )) a<sa | |
| 20 | 180 cc (suc n) n<k k<A | tri> ¬a ¬b c = |
| 22 | 181 cc n (less-1 n<k) (lemma3 c) where |
| 182 lemma3 : (A - ((k - (suc n)) * M)) > M → suc A > (k - n) * M | |
| 183 lemma3 mk<a = <-trans lemma5 a<sa where | |
| 184 lemma6 : M + (k - (suc n)) * M ≡ (k - n) * M | |
| 185 lemma6 = begin | |
| 186 M + (k - (suc n)) * M | |
| 187 ≡⟨ cong (λ x → M + x) (minus-* {M} {k} (<-minus-0 n<k)) ⟩ | |
| 188 M + (((k - n) * M ) - M ) | |
| 189 ≡⟨ +-comm M _ ⟩ | |
| 190 ((k - n) * M ) - M + M | |
| 26 | 191 ≡⟨ minus+n {_} {M} (nextc n n<k ) ⟩ |
| 22 | 192 (k - n) * M |
| 193 ∎ where open ≡-Reasoning | |
| 194 lemma4 : (M + (k - (suc n)) * M) < A | |
| 195 lemma4 = subst (λ x → (M + (k - (suc n)) * M) < x ) (minus+n {A}{(k - (suc n)) * M} k<A ) ( <-plus mk<a ) | |
| 196 lemma5 : (k - n) * M < A | |
| 197 lemma5 = subst (λ x → x < A ) lemma6 lemma4 | |
| 17 | 198 start-range : (k : ℕ ) → suc A > (k - k) * M |
| 199 start-range zero = s≤s z≤n | |
| 200 start-range (suc k) = start-range k | |
| 201 |