--- a/automaton-in-agda/src/gcd.agda	Mon Jun 21 22:34:59 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 21 23:19:51 2021 +0900
@@ -234,32 +234,25 @@
    k + 0 ≡⟨ +-comm _ 0 ⟩
    k  ∎ where open ≡-Reasoning
 
-decD : {k m : ℕ} → k > 1 → Dec (Dividable k m ∧ (0 < m))
-decD {k} {m} k>1 = n-induction {_} {_} {ℕ} {λ m → Dec (Dividable k m ∧ ( 0 < m)) } F I m where
+decD : {k m : ℕ} → k > 1 → Dec (Dividable k m )
+decD {k} {m} k>1 = n-induction {_} {_} {ℕ} {λ m → Dec (Dividable k m ) } F I m where
         F : ℕ → ℕ
         F m = m
-        F0 : ( m : ℕ ) → F (m - k) ≡ 0 →  Dec  (Dividable k m  ∧ (0 < m ))
-        F0 0 eq =   no (λ d → ⊥-elim ( nat-≡< refl (proj2 d)))
+        F0 : ( m : ℕ ) → F (m - k) ≡ 0 →  Dec  (Dividable k m  )
+        F0 0 eq = yes record { factor = 0 ; is-factor = refl }
         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 ) (sym (i-j=0→i=j (<to≤ a) eq )) div1*k+0=k }  , s≤s z≤n  ⟫ where -- (suc m - k) ≡ 0 → k ≡ suc m, k ≤ suc m
-        ... | tri≈ ¬a refl ¬c =  yes  ⟪ record { factor = 1 ; is-factor = div1*k+0=k } ,  s≤s z≤n ⟫
-        ... | tri> ¬a ¬b c = no ( λ d →  ⊥-elim (div<k k>1 (s≤s z≤n ) c (proj1 d)) )
+        ... | tri< a ¬b ¬c = yes  record { factor = 1 ; is-factor =
+            subst (λ g → 1 * k + 0 ≡ g ) (sym (i-j=0→i=j (<to≤ a) eq )) div1*k+0=k }  where -- (suc m - k) ≡ 0 → k ≡ suc m, k ≤ suc m
+        ... | tri≈ ¬a refl ¬c =  yes   record { factor = 1 ; is-factor = div1*k+0=k } 
+        ... | tri> ¬a ¬b c = no ( λ d →  ⊥-elim (div<k k>1 (s≤s z≤n ) c d) )
         decl : {m  : ℕ } → 0 < m → m - k < m
         decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m 
-        ind : (p : ℕ ) → Dec (Dividable k (p - k) ∧ ( 0 < p - k)) → Dec (Dividable k p ∧ ( 0 < p))
-        ind p (yes y) = yes ⟪ (subst (λ g → Dividable k g) (minus+n (<-trans k<p a<sa)) (proj1 ( div+div (proj1 y) div= ))) , <-trans (<-trans a<sa k>1) k<p ⟫ where
-           k<p :  k < p -- k * factor y + 0 ≡ p - k , 0 < p - k
-           k<p with <-cmp k p
-           ... | tri< a ¬b ¬c = a 
-           ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< (sym ( minus<=0 {k} ≤-refl )) (proj2 y)) 
-           ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym ( minus<=0 {p} {k} (≤-trans refl-≤s c ))) (proj2 y)) 
-        ind p (no n) = no (λ d → n ⟪ proj1 (div-div k>1 (proj1 d) div=) , 0<pk (Dividable.factor (proj1 d)) (proj2 d) (Dividable.is-factor (proj1 d)  ) ⟫ ) where
-           -- Dividable k p ∧ (0 < p) → Dividable k (p - k) ∧ (0 < (p - k))
-           0<pk : (f : ℕ) →  0 < p → f * k + 0 ≡ p  → 0 < p - k  
-           0<pk f 0<p eq with <-cmp 0 (p - k)
-           ... | tri< a ¬b ¬c = a
-           ... | tri≈ ¬a b ¬c = {!!}  -- f * k + 0 ≡ p → p ≡ 0 ∨ k ≤ p
+        ind : (p : ℕ ) → Dec (Dividable k (p - k) ) → Dec (Dividable k p )
+        ind p (yes y) with <-cmp p k
+        ... | tri< a ¬b ¬c = no  {!!}
+        ... | tri≈ ¬a refl ¬c = yes (subst (λ g → Dividable k g) (minus+n ≤-refl ) (proj1 ( div+div y div= ))) 
+        ... | tri> ¬a ¬b k<p  = yes (subst (λ g → Dividable k g) (minus+n (<-trans k<p a<sa)) (proj1 ( div+div y div= ))) 
+        ind p (no n) = no (λ d → n (proj1 (div-div k>1 d div=))  ) 
         I : Ninduction ℕ  _  F
         I = record {
               pnext = λ p → p - k