Mercurial > hg > Members > kono > Proof > prob1
changeset 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 |
| files | prob1.agda |
| diffstat | 1 files changed, 6 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/prob1.agda Mon Mar 30 17:03:01 2020 +0900 +++ b/prob1.agda Mon Mar 30 17:25:06 2020 +0900 @@ -37,10 +37,8 @@ record UCond1 (A M k : ℕ ) : Set where field c1 : Cond1 A M k - u1 : {j m : ℕ} → j < Cond1.i c1 → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) - u2 : {j m : ℕ} → Cond1.i c1 < j → j < M → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) - u3 : {j m : ℕ} → j < M → m < Cond1.n c1 → ¬ ( j + k * M ≡ M * (suc m) + A ) - u4 : {j m : ℕ} → j < M → Cond1.n c1 < m → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) + unique-i : {j : ℕ} {m1 : ℕ} → j < M → m1 < k → j + k * M ≡ M * suc m1 + A → Cond1.i c1 ≡ j + unique-n : {j : ℕ} {m1 : ℕ} → j < M → m1 < k → j + k * M ≡ M * suc m1 + A → Cond1.n c1 ≡ m1 problem1-0 : (k A M : ℕ ) → (A<kM : suc A < k * M ) → UCond1 A M k @@ -140,11 +138,11 @@ 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 lemma-u4 : {j : ℕ} {m₁ : ℕ} → j < M → n < m₁ → m₁ < suc k → ¬ j + suc k * M ≡ M * suc m₁ + A 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 + unique-n : {j m1 : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → n ≡ m1 + unique-n {j} {m1} j<M m1<k eq = unique-m (unique-i j<M m1<k eq ) (Cond1.rule1 c1) eq c0 = record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = i<M; rule1 = Cond1.rule1 c1 } - ; u1 = lemma-u1 - ; u2 = lemma-u2 - ; u3 = lemma-u3 - ; u4 = lemma-u4 + ; unique-i = unique-i + ; unique-n = unique-n } -- loop on range of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M)