# HG changeset patch
# User kono
# Date 1585287428 -32400
# Node ID e35d729efd5859c925f5281f723b1be34894a961
# Parent  61a889d975e1f996803a5419afeadb187d33c8cd
fix

diff -r 61a889d975e1 -r e35d729efd58 nat.agda
--- a/nat.agda	Wed Nov 27 18:44:28 2019 +0900
+++ b/nat.agda	Fri Mar 27 14:37:08 2020 +0900
@@ -8,7 +8,7 @@
 open import  Relation.Binary.PropositionalEquality
 open import  Relation.Binary.Core
 open import  logic
-
+open import Relation.Binary.Definitions
 
 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
 nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
diff -r 61a889d975e1 -r e35d729efd58 prob1.agda
--- a/prob1.agda	Wed Nov 27 18:44:28 2019 +0900
+++ b/prob1.agda	Fri Mar 27 14:37:08 2020 +0900
@@ -9,7 +9,7 @@
 open import Data.Empty
 open import Data.Product
 open import Relation.Nullary
-
+open import Relation.Binary.Definitions
 
 -- All variables are positive integer
 -- A = -M*n + i +k*M  - M
@@ -37,6 +37,8 @@
 problem : ( A M k : ℕ ) → Set 
 problem A M k =  (suc A <  k * M ) → Cond1 A M k
 
+
+
 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 ))
@@ -148,19 +150,18 @@
 --      range-i : i < M
 --      rule1 : i + k * M  ≡ M * (suc n) + A    -- A ≡ (i + k * M ) - (M * (suc n)) 
 
-problem1-0 : (A M k : ℕ ) 
-    → (c1 : Cond1 A M k ) → (c2 : Cond1 A M k )
-    →  (  Cond1.n c1  ≡ Cond1.n c2 ) ∧ ( Cond1.i c1  ≡ Cond1.i c2 )
-problem1-0 A (suc m) (suc k) c1 c2 = cc k a<sa (start-range k) where
+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
      M = suc m
-     cck :  ( n : ℕ ) →  n < suc k  → (suc A >  ((k - n) ) * M )  → A - ((k - n) * M) < M →  (  Cond1.n c1  ≡ Cond1.n c2 ) ∧ ( Cond1.i c1  ≡ Cond1.i c2 ) 
+     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 = {!!} }  
         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.n c1  ≡ Cond1.n c2 ) ∧ ( Cond1.i c1  ≡ Cond1.i c2 )
+     cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → ( Cond1.i c1  ≡ Cond1.i (problem0-k=k k A M {!!}) )
      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 {!!}
@@ -171,8 +172,3 @@
      start-range zero = s≤s z≤n
      start-range (suc k) = start-range k
 
-problem1 : (A1 A2 M k : ℕ ) 
-    → (c1 : Cond1 A1 M k ) → (c2 : Cond1 A2 M k )
-    → ( A1 ≡ A2 ) → (  Cond1.n c1  ≡ Cond1.n c2 ) ∧ ( Cond1.i c1  ≡ Cond1.i c2 )
-problem1 = {!!}
-