# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585388295 -32400
# Node ID 65f0efcc6dc7f649e1ba4ceea1850de3a8316d8d
# Parent  9cd63570c1baef85a8c030b68bf9574d026a76e3
...

diff -r 9cd63570c1ba -r 65f0efcc6dc7 prob1.agda
--- a/prob1.agda	Sat Mar 28 17:17:53 2020 +0900
+++ b/prob1.agda	Sat Mar 28 18:38:15 2020 +0900
@@ -42,7 +42,8 @@
 problem0-k=k : ( k A M : ℕ ) → problem A M k
 problem0-k=k zero A M ()
 problem0-k=k (suc k) A zero A<kM = ⊥-elim ( nat-<> A<kM (subst (λ x → x < suc A) (*-comm _ k ) 0<s ))
-problem0-k=k (suc k) A (suc m) A<kM = cc k a<sa (start-range k) where
+problem0-k=k (suc k) A (suc m) A<kM = cc k a<sa (start-range k)
+  module kk where
      M = suc m
      cck :  ( n : ℕ ) →  n < suc k  → (suc A >  ((k - n) ) * M )  → A - ((k - n) * M) < M →  Cond1 A M (suc k)
      cck n n<k gt lt =  record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = lt ; rule1 = lemma2 }  where
@@ -158,22 +159,27 @@
       -- 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    )
 
-problem1-0 : (A M k : ℕ )  → (x : suc A <  k * M )
+problem1-0 : (k A M : ℕ )  → (A<kM : suc A <  k * M )
     → UCond1 A M k 
-problem1-0 A zero _ _ = {!!}
-problem1-0 A (suc m) (suc k) x = cc k a<sa (start-range k) where
+problem1-0 zero A M () 
+problem1-0 (suc k) A zero A<kM = ⊥-elim ( nat-<> A<kM (subst (λ x → x < suc A) (*-comm _ k ) 0<s ))
+problem1-0 (suc k) A (suc m) A<kM = cc k a<sa (start-range k) where
      M = suc m
      cck :  ( n : ℕ ) →  n < suc k  → (suc A >  ((k - n) ) * M )  → A - ((k - n) * M) < M → UCond1 A M (suc k)
      cck n n<k k<A i<M = c0 where
-        c0  =  record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = {!!} ; rule1 = {!!} } ; u1 = {!!}  }
-        lemma-i :  (i : ℕ ) →  i < M  →  i + suc k * M ≡ M * suc n + A → i ≡  A - (k - n) * M
-        lemma-i = {!!}
-        lemma-n :  (n1 : ℕ ) → ¬ ( n1 ≡ n ) → ¬ ( ( i : ℕ ) → i < M  →  i + suc k * M ≡ M * suc n1 + A → i ≡  A - (k - n1) * M )
-        lemma-n = {!!}
+        c1 : Cond1 A M (suc k) 
+        c1 = kk.cck k A m A<kM n n<k k<A i<M 
+        lemma-u1 : {j : ℕ} {m1 : ℕ} → j < (A - ((k - n) * M)) → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A
+        lemma-u1 = {!!}
+        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 {!!}
+     cc zero n<k k<A = cck 0 n<k k<A lemma where
+        a<m : suc A < M + k * M 
+        a<m = A<kM
+        lemma : A - ((k - 0) * M) < M
+        lemma = <-minus {_} {_} {k * M} (subst (λ x → x < M + k * M) (sym (minus+n {A} {k * M} k<A )) (less-1 a<m) )
      cc (suc n) n<k k<A with <-cmp (A - ((k - (suc n)) * M))  M
-     cc (suc n) n<k k<A | tri< a ¬b ¬c = cck (suc n) n<k k<A {!!}
+     cc (suc n) n<k k<A | tri< a ¬b ¬c = cck (suc n) n<k k<A a
      cc (suc n) n<k k<A | tri≈ ¬a b ¬c = 
          record { c1 = UCond1.c1 (cc n {!!} {!!}) ; u1 = {!!}  }
      cc (suc n) n<k k<A | tri> ¬a ¬b c =