--- a/automaton-in-agda/src/gcd.agda	Mon Jun 21 09:40:52 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 21 11:04:37 2021 +0900
@@ -30,9 +30,6 @@
 FtoD : {n m : ℕ} → (fc : Factor n m) → remain fc ≡ 0 → Dividable n m 
 FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } refl = record { factor = f ; is-factor = fa }
 
---decD : {n m : ℕ} → Dec (Dividable n m)
---decD = {!!}
-
 --divdable^2 : ( n k : ℕ ) → Dividable k ( n * n ) → Dividable k n
 --divdable^2 n k dn2 = {!!}
 
@@ -216,6 +213,57 @@
 
 open _∧_
 
+div+1 : { i k : ℕ } → k > 1 →  Dividable k i →  ¬ Dividable k (suc i)  
+div+1 {i} {k} k>1 d d1 = div1 k>1 div+11 where
+   div+11 : Dividable k 1
+   div+11 = subst (λ g → Dividable k g) (minus+y-y {1} {i} ) ( proj2 (div-div k>1 d d1  ) )
+
+div<k : { m k : ℕ } → k > 1 → m > 0 →  m < k →  ¬ Dividable k m
+div<k {m} {k} k>1 m>0 m<k d = ⊥-elim ( nat-≤> (div<k1 (Dividable.factor d) (Dividable.is-factor d)) m<k ) where
+    div<k1 : (f : ℕ ) → f * k + 0 ≡ m → k ≤ m
+    div<k1 zero eq = ⊥-elim (nat-≡< eq m>0 )
+    div<k1 (suc f) eq = begin
+          k ≤⟨ x≤x+y ⟩
+          k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩
+          k + f * k + 0 ≡⟨ eq ⟩
+          m ∎  where open ≤-Reasoning  
+
+div1*k+0=k : {k : ℕ } → 1 * k + 0 ≡ k
+div1*k+0=k {k} =  begin
+   1 * k + 0 ≡⟨ cong (λ g → g + 0) (+-comm _ 0) ⟩
+   k + 0 ≡⟨ +-comm _ 0 ⟩
+   k  ∎ where open ≡-Reasoning
+
+decD : {k m : ℕ} → k > 1 → Dec (Dividable k m)
+decD {k} {m} k>1 = f-induction {_} {_} {ℕ} {λ m → Dec (Dividable k m)} F I m where
+        record FF (m : ℕ ) : Set where
+           field
+              diff : ℕ
+              is-diff :  k < m  → diff  ≡ m - k
+        ff : (m : ℕ ) → FF m
+        ff 0  = record { diff = 0 ; is-diff = λ () }
+        ff m with <-cmp k m
+        ... | tri< a ¬b ¬c = record { diff = m - k ; is-diff = λ _ → refl }
+        ... | tri≈ ¬a b ¬c = record { diff = 0 ; is-diff = λ lt → ⊥-elim (¬a lt) }
+        ... | tri> ¬a ¬b c = record { diff = 0 ; is-diff = λ lt → ⊥-elim (¬a lt) }
+        F : ℕ → ℕ
+        F m = FF.diff (ff m)
+        F0 : ( m : ℕ ) → F m ≡ 0 →  Dec  (Dividable k m )
+        F0 0 eq =  yes div0
+        F0 (suc m) eq with <-cmp k (suc m)
+        ... | tri< a ¬b ¬c = yes record { factor = 1 ; is-factor = subst (λ g → 1 * k + 0 ≡ g ) m=k div1*k+0=k }  where
+            m=k : k ≡ suc m
+            m=k = sym (i-j=0→i=j (≤-trans refl-≤s a ) (subst (λ k → k ≡ 0) (FF.is-diff (ff (suc m)) a ) {!!}))
+        ... | tri≈ ¬a refl ¬c = yes record { factor = 1 ; is-factor = div1*k+0=k }
+        ... | tri> ¬a ¬b c = no (div<k k>1 {!!} c )
+        I : Finduction ℕ  _  F
+        I = record {
+              fzero = {!!}
+            ; pnext = λ p → {!!}
+            ; decline = λ {p} lt → {!!}
+            ; ind = λ {p} prev → {!!}
+          } 
+
 gcd-gt : ( i i0 j j0 k : ℕ ) → k > 1 → (if : Factor k i) (i0f : Dividable k i0 ) (jf : Factor k j ) (j0f : Dividable k j0)
    → Dividable k (i - j) ∧ Dividable k (j - i)
    → Dividable k ( gcd1 i i0 j j0 ) 
@@ -413,11 +461,6 @@
       gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩
       1 ∎ where open ≡-Reasoning
 
-div+1 : { i k : ℕ } → k > 1 →  Dividable k i →  ¬ Dividable k (suc i)  
-div+1 {i} {k} k>1 d d1 = div1 k>1 div+11 where
-   div+11 : Dividable k 1
-   div+11 = subst (λ g → Dividable k g) (minus+y-y {1} {i} ) ( proj2 (div-div k>1 d d1  ) )
-
 gcd>0 : ( i j : ℕ ) → 0 < i → 0 < j → 0 < gcd i j  
 gcd>0 i j 0<i 0<j = gcd>01 i i j j 0<i 0<j where
      gcd>01 : ( i i0 j j0 : ℕ ) → 0 < i0 → 0 < j0  → gcd1 i i0 j j0 > 0