--- a/automaton-in-agda/src/gcd.agda	Thu Jun 17 10:01:26 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Thu Jun 17 11:13:58 2021 +0900
@@ -79,9 +79,12 @@
         (Dividable.factor div * suc k + 0) + remain if  ≡⟨ cong (λ g → g + remain if) (+-comm _ 0) ⟩
         Dividable.factor div * suc k + remain if ∎  )) ⟩ Dividable.factor div ∎   where open ≡-Reasoning
 
-decf-step : {i k : ℕ } → k > 1 → (if : Factor k (suc i)) 
-     → Dividable k (suc i - remain if)  → Dividable k (i - remain (decf {i} {k} if))
-decf-step {i} {suc k}  k>1 if div = decf-step1 {i} {suc k}  (factor if) (remain if) (is-factor if) div where
+div0 :  {k : ℕ} → Dividable k 0
+div0 {k} = record { factor = 0; is-factor = refl }
+
+decf-step : {i j k : ℕ } → k > 1 → (if : Factor k (suc i))  → (jf : Factor k (suc j)) 
+   → Dividable k (i - j) ∧ Dividable k (j - i)
+decf-step {i} {j} {suc k}  k>1 if jf = decf-step0 {i} {j} {suc k}  k>1 if jf where
    decf-step1 : {i k : ℕ } →  (f r : ℕ) → (fa : f * k + r ≡ suc i) 
         → Dividable k (suc i - r)  → Dividable k (i - remain (decf record {factor = f ; remain = r ; is-factor = fa}))
    decf-step1 {i} {k}   f (suc r) fa div = 
@@ -107,6 +110,13 @@
           k + (f * suc k + 0) ≡⟨ +-comm k _ ⟩
           f * suc k + 0 + k ∎ ))  ⟩ 
         i - k ∎ ) }  where open ≡-Reasoning
+   decf-step0 : {i j k : ℕ } → k > 1 → (if : Factor k (suc i))  → (jf : Factor k (suc j)) 
+           → Dividable k (i - j) ∧ Dividable k (j - i)
+   decf-step0 {i} {j} {suc k}  k>1 if jf with <-cmp i j
+   ... | tri< a ¬b ¬c = ⟪ subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {j} (<to≤ a))) div0 , {!!}  ⟫ 
+   ... | tri≈ ¬a refl ¬c = ⟪ subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {i} refl-≤)) div0 ,
+                             subst (λ g → Dividable (suc k) g) (sym (minus<=0 {i} {i} refl-≤)) div0 ⟫
+   ... | tri> ¬a ¬b c = ⟪ {!!} , subst (λ g → Dividable (suc k) g) (sym (minus<=0 {j} {i} (<to≤ c))) div0  ⟫ 
 
 ifk0 : (  i0 k : ℕ ) → (i0f : Factor k i0 )  → ( i0=0 : remain i0f ≡ 0 )  → factor i0f * k + 0 ≡ i0
 ifk0 i0 k i0f i0=0 = begin
@@ -139,32 +149,45 @@
 gcd : ( i j : ℕ ) → ℕ
 gcd i j = gcd1 i i j j 
 
-¬div : { i k : ℕ } → k > 1 →  Dividable k i → ¬ Dividable k (suc i)
-¬div = {!!}
+div1 : { k : ℕ } → k > 1 →  ¬  Dividable k 1
+div1 {k} k>1 record { factor = (suc f) ; is-factor = fa } = ⊥-elim ( nat-≡< (sym fa) ( begin
+    2 ≤⟨ k>1 ⟩
+    k ≡⟨ +-comm 0 _ ⟩
+    k + 0 ≡⟨ refl  ⟩
+    1 * k ≤⟨ *-mono-≤ {1} {suc f} (s≤s z≤n ) ≤-refl ⟩
+    suc f * k ≡⟨ +-comm 0 _ ⟩
+    suc f * k + 0 ∎  )) where open ≤-Reasoning  
+
+open _∧_
 
 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 - remain if) → Dividable k (j - remain jf) 
+   → Dividable k (i - j) ∧ Dividable k (j - i)
    → Dividable k ( gcd1 i i0 j j0 ) 
-gcd-gt zero i0 zero j0 k k>1 if i0f jf j0f i-r j-r with <-cmp i0 j0
+gcd-gt zero i0 zero j0 k k>1 if i0f jf j0f i-j with <-cmp i0 j0
 ... | tri< a ¬b ¬c = i0f 
 ... | tri≈ ¬a refl ¬c = i0f
 ... | tri> ¬a ¬b c = j0f
-gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f i-r j-r = {!!} -- can't happen
-gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f i-r j-r = j0f
-gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f i-r j-r =   
-    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k k>1 (decf (DtoF i0f)) i0f (decf jf) {!!} {!!} (decf-step k>1 jf j-r )
-gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f i-r j-r = {!!} -- can't happen
-gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f i-r j-r = i0f
-gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f i-r j-r = --   
-     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) {!!} (decf (DtoF j0f)) j0f (decf-step k>1 if i-r ) {!!}
-gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f i-r j-r =  
-     gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f (decf-step k>1 if i-r ) (decf-step k>1 jf j-r )
-gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f i-r j-r = 
-     gcd-gt (suc i) i0 j j0 k k>1 (decf if) i0f (decf jf) j0f (decf-step k>1 if i-r ) (decf-step k>1 jf j-r )
+gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f i-j = ⊥-elim (div1 k>1 (proj2 i-j)) -- can't happen
+gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f i-j = j0f
+gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f i-j =   
+    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k k>1 (decf (DtoF i0f)) i0f (decf jf) (proj2 i-j) {!!}
+     --  if  : Factor k zero
+     -- i0f : Dividable k (suc i0)
+     -- jf  : Factor k (suc (suc j))
+     -- j0f : Dividable k j0
+     --   Dividable k (zero - suc (suc j)) ∧ Dividable k (suc (suc j) - zero) → Dividable k (i0 - suc j) ∧ Dividable k (suc j - i0)
+gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f i-j  = ⊥-elim (div1 k>1 (proj1 i-j)) -- can't happen
+gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f i-j  = i0f
+gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f i-j  = --   
+     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) (proj1 i-j) (decf (DtoF j0f)) j0f {!!} 
+gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f i-j  =  
+     gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i-j
+gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f i-j  = 
+     gcd-gt (suc i) i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i-j 
 
 gcd-div : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j ) 
    → Dividable k ( gcd i  j ) 
-gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf {!!} {!!} 
+gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf {!!} 
 
 
 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m