# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585383473 -32400
# Node ID 9cd63570c1baef85a8c030b68bf9574d026a76e3
# Parent  9f5bf86fe6dd266fa242b239f0489e5ac132a008
add Uunique case

diff -r 9f5bf86fe6dd -r 9cd63570c1ba prob1.agda
--- a/prob1.agda	Sat Mar 28 13:38:56 2020 +0900
+++ b/prob1.agda	Sat Mar 28 17:17:53 2020 +0900
@@ -9,15 +9,8 @@
 open import Data.Empty
 open import Data.Product
 open import Relation.Nullary
-<<<<<<< working copy
-
-||||||| base
-
+-- open import Relation.Binary.Definitions
 
-=======
-open import Relation.Binary.Definitions
-
->>>>>>> destination
 -- All variables are positive integer
 -- A = -M*n + i +k*M  - M
 -- where n is in range (0,…,k-1) and i is in range(0,…,M-1)
@@ -157,23 +150,34 @@
 --      range-i : i < M
 --      rule1 : i + k * M  ≡ M * (suc n) + A    -- A ≡ (i + k * M ) - (M * (suc n)) 
 
+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    )
+
 problem1-0 : (A M k : ℕ )  → (x : suc A <  k * M )
-    → (c1 : Cond1 A M k ) → Cond1.i c1 ≡ Cond1.i (problem0-k=k k A M x)
-problem1-0 A (suc m) (suc k) x c1 = {!!} where -- cc k a<sa (start-range k) where
+    → UCond1 A M k 
+problem1-0 A zero _ _ = {!!}
+problem1-0 A (suc m) (suc k) x = 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 → ( Cond1.i c1  ≡ Cond1.i (problem0-k=k k A M {!!}) ) 
-     cck n n<k k<A i<M = {!!} where
-        c0  =  record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = {!!} ; rule1 = {!!} }  
+     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 = {!!}
-     cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → ( Cond1.i c1  ≡ Cond1.i (problem0-k=k k A M {!!}) )
+     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 (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 = {!!}
-     cc (suc n) n<k k<A | tri> ¬a ¬b c = {!!}
+     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 = 
+         record { c1 = UCond1.c1 (cc n {!!} {!!}) ; u1 = {!!}  }
 
      start-range : (k : ℕ ) → suc A > (k - k) * M
      start-range zero = s≤s z≤n