--- a/automaton-in-agda/src/gcd.agda	Mon Jun 14 09:06:20 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 14 11:12:36 2021 +0900
@@ -37,17 +37,34 @@
         k + f * suc k ≡⟨ +-comm zero _ ⟩
         (k + f * suc k) + zero  ≡⟨ cong pred fa ⟩
         n ∎ ) }  where open ≡-Reasoning
-decf {n} {k} record { factor = f ; remain = (suc r) ; is-factor = fa } = 
+decf {n} {zero} record { factor = f ; remain = (suc r) ; is-factor = fa } = {!!}
+decf {n} {suc k} record { factor = f ; remain = (suc r) ; is-factor = fa } = 
      record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n
-        f * k + r ≡⟨ cong pred ( begin
-          suc ( f * k + r ) ≡⟨ +-comm _ r ⟩
-          r + suc (f * k)  ≡⟨ sym (+-assoc r 1 _) ⟩
-          (r + 1) + f * k ≡⟨ cong (λ t → t + f * k ) (+-comm r 1) ⟩
-          (suc r ) + f * k ≡⟨ +-comm (suc r) _ ⟩
-          f * k + suc r  ≡⟨ fa ⟩
+        f * (suc k) + r ≡⟨ cong pred ( begin
+          suc ( f * (suc k) + r ) ≡⟨ +-comm _ r ⟩
+          r + suc (f * (suc k))  ≡⟨ sym (+-assoc r 1 _) ⟩
+          (r + 1) + f * (suc k) ≡⟨ cong (λ t → t + f * (suc k) ) (+-comm r 1) ⟩
+          (suc r ) + f * (suc k) ≡⟨ +-comm (suc r) _ ⟩
+          f * (suc k) + suc r  ≡⟨ fa ⟩
           suc n ∎ ) ⟩ 
         n ∎ ) }  where open ≡-Reasoning
 
+decf-step : {i k i0 : ℕ } → (if : Factor k (suc i)) → (i0f : Factor k i0) → remain if + suc i ≡ i0 → remain (decf if) + i ≡ i0
+decf-step {i} {zero} {i0} record { factor = (suc f) ; remain = zero ; is-factor = fa } i0f eq = ⊥-elim (nat-≡< fa (
+        begin suc (suc f * zero + zero) ≡⟨ cong suc (+-comm _ zero)  ⟩
+        suc (f * 0) ≡⟨ cong suc (*-comm f zero)  ⟩
+        suc zero ≤⟨ s≤s z≤n ⟩
+        suc i ∎ )) where open ≤-Reasoning  -- suc (0 + i) ≡ i0
+decf-step {i} {suc k} {i0} record { factor = suc f ;  remain = zero ; is-factor = fa } i0f eq = begin
+        remain (decf (record { factor = suc f ; remain = zero ; is-factor = fa })) + i ≡⟨ refl ⟩
+        k + i  ≡⟨ {!!} ⟩
+        i0 ∎    where open ≡-Reasoning
+decf-step {i} {zero} {i0} record { factor = f ; remain = suc r ; is-factor = fa } i0f eq = {!!}
+decf-step {i} {suc k} {i0} record { factor = f ; remain = suc r ; is-factor = fa } i0f eq = begin
+        (remain (decf (record { factor = f ; remain = suc r ; is-factor = fa })) + i) ≡⟨ {!!} ⟩
+        suc (r + i) ≡⟨ {!!} ⟩
+        i0 ∎    where open ≡-Reasoning
+
 ifk0 : (  i0 k : ℕ ) → (i0f : Factor k i0 )  → ( i0=0 : remain i0f ≡ 0 )  → factor i0f * k + 0 ≡ i0
 ifk0 i0 k i0f i0=0 = begin
    factor i0f * k + 0  ≡⟨ cong (λ m → factor i0f * k + m) (sym i0=0)  ⟩
@@ -90,8 +107,7 @@
 gcd-gt zero i0 (suc zero) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
 gcd-gt zero zero (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor j0f ; is-factor = ifk0 j0 k j0f j0=0 } 
 gcd-gt zero (suc i0) (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =  
-    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k (decf i0f) i0f (decf jf)
-       record { factor = factor jf ; remain = remain jf ; is-factor = {!!} } i0=0 {!!} {!!} {!!}  
+    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k (decf i0f) i0f (decf jf) jf i0=0 {!!} {!!} {!!}  
 gcd-gt (suc zero) i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
 gcd-gt (suc (suc i)) i0 zero zero k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor i0f ; is-factor = ifk0 i0 k i0f i0=0 } 
 gcd-gt (suc (suc i)) i0 zero (suc j0) k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =
@@ -99,7 +115,7 @@
 gcd-gt (suc zero) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = 
      gcd-gt zero i0 j j0 k (decf if) i0f (decf jf) j0f i0=0 j0=0 {!!} {!!}
 gcd-gt (suc (suc i)) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = 
-     gcd-gt (suc i) i0 j j0 k (decf if) i0f (decf jf) j0f i0=0 j0=0 {!!} {!!}
+     gcd-gt (suc i) i0 j j0 k (decf if) i0f (decf jf) j0f i0=0 j0=0 (decf-step if i0f ir=i0 ) (decf-step jf j0f jr=j0 )
 
 gcd-div : ( i j k : ℕ ) → (if : Factor k i) (jf : Factor k j ) 
    → remain if ≡ 0 → remain jf ≡  0