Mercurial > hg > Members > kono > Proof > prob1

changeset 30:7256d3d032e4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
minor fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Mar 2020 17:51:52 +0900
parents 24864ed3b6d3
children 908409975a5e
files prob1.agda
diffstat 1 files changed, 1 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/prob1.agda	Mon Mar 30 17:25:06 2020 +0900
+++ b/prob1.agda	Mon Mar 30 17:51:52 2020 +0900
@@ -100,7 +100,7 @@
         lemma-u1 : {j : ℕ} {m1 : ℕ} → j < i → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A
         lemma-u1 {j} {m1} j<akM m1<k eq with <-cmp j M
         lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c =
-            ⊥-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
+            ⊥-elim (nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym eq) (sym (Cond1.rule1 c1 )) lemma3) ) i<M ) where
              lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A   -- M + j ≤ i
              lemma3 = lemma5 (lemma4  eq (Cond1.rule1 c1) j<akM)
         lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) 
@@ -132,12 +132,6 @@
         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 ))
         unique-m {i} {_} {n} {m1} refl eqn eqm | tri≈ ¬a b ¬c = b
         unique-m {i} {_} {n} {m1} refl eqn eqm | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (trans (sym eqm) eqn ) (lemma7 {m1} {n} {m} {A} c ))
-        m1<sk : {m1 : ℕ} → m1 < n → n < suc k  → m1 < suc k
-        m1<sk {m1} m1<n n<k = <-trans m1<n n<k
-        lemma-u3 : {j : ℕ} {m₁ : ℕ} → j < M → m₁ < n → ¬ j + suc k * M ≡ M * suc m₁ + A
-        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 }