Mercurial > hg > Members > kono > Proof > prob1
changeset 23:f2db03a8af2c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 29 Mar 2020 23:36:18 +0900 |
| parents | c5ed490494bc |
| children | 0b53b08e7ae4 |
| files | prob1.agda |
| diffstat | 1 files changed, 5 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/prob1.agda Sun Mar 29 08:29:21 2020 +0900 +++ b/prob1.agda Sun Mar 29 23:36:18 2020 +0900 @@ -174,7 +174,11 @@ lemma3 : {i j : ℕ} → j + suc k * M + M < suc (i + suc k * M ) → j + M < suc i lemma3 = {!!} lemma-u1 : {j : ℕ} {m1 : ℕ} → j < (A - ((k - n) * M)) → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A - lemma-u1 {j} {m1} j<akM m1<k eq = {!!} + 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 = {!!} + lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) + -- (suc (minus A (minus k n * suc m))) !=< (minus A (minus k n * suc m)) + lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM ) 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 } cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → UCond1 A M (suc k) cc zero n<k k<A = cck 0 n<k k<A lemma where