--- a/automaton-in-agda/src/gcd.agda	Tue Jun 15 13:44:31 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Tue Jun 15 15:39:17 2021 +0900
@@ -26,20 +26,16 @@
 
 
 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
-decf {n} {zero} record { factor = f ; remain = zero ; is-factor = fa } = ⊥-elim ( nat-≡< fa (
-        begin suc (f * zero + zero) ≡⟨ {!!}  ⟩
-        f * 0 ≡⟨ {!!} ⟩
-        zero ≤⟨ z≤n ⟩
-        suc n ∎ )) where open ≤-Reasoning
-decf {n} {suc k} record { factor = (suc f) ; remain = zero ; is-factor = fa } = 
-     record { factor = f ; remain = k ; is-factor = ( begin -- fa : suc (k + f * suc k + zero) ≡ suc n
-        f * suc k + k ≡⟨ +-comm _ k ⟩
-        k + f * suc k ≡⟨ +-comm zero _ ⟩
-        (k + f * suc k) + zero  ≡⟨ cong pred fa ⟩
-        n ∎ ) }  where open ≡-Reasoning
-decf {n} {k} record { factor = zero ; remain = zero ; is-factor = fa } = {!!}
-decf {n} {k} record { factor = zero ; remain = (suc r) ; is-factor = fa } = {!!}
-decf {n} {k} record { factor = suc f1 ; remain = (suc r) ; is-factor = fa } = 
+decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = 
+ decf1 {n} {k} f r fa where
+  dr : ( n k : ℕ ) → (f r : ℕ) → ℕ
+  dr n zero (suc f) zero = 0
+  dr n (suc k) (suc f) zero = k
+  dr n k f (suc r) = r
+  dr n zero zero zero = r
+  dr n (suc k) zero zero = r
+  decf1 : { n k : ℕ } → (f r : ℕ) → (f * k + r ≡ suc n)  → Factor k n 
+  decf1 {n} {k} f (suc r) fa  =  -- this case must be the first
      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 ⟩
@@ -48,31 +44,39 @@
           (suc r ) + f * k ≡⟨ +-comm (suc r) _ ⟩
           f * k + suc r  ≡⟨ fa ⟩
           suc n ∎ ) ⟩ 
-        n ∎ ) }  where
-          open ≡-Reasoning
-          f = suc f1
+        n ∎ ) }  where open ≡-Reasoning
+  decf1 {n} {zero} (suc f) zero fa  = ⊥-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 n ∎ )) where open ≤-Reasoning
+  decf1 {n} {suc k} (suc f) zero fa  = 
+     record { factor = f ; remain = k ; is-factor = ( begin -- fa : suc (k + f * suc k + zero) ≡ suc n
+        f * suc k + k ≡⟨ +-comm _ k ⟩
+        k + f * suc k ≡⟨ +-comm zero _ ⟩
+        (k + f * suc k) + zero  ≡⟨ cong pred fa ⟩
+        n ∎ ) }  where open ≡-Reasoning
 
-decf-step : {i k i0 : ℕ } → (if : Factor k (suc i)) → (i0f : Factor k i0) → Dividable k (suc i - remain if)  → Dividable k (i - remain (decf if))
-decf-step {i} {zero} {i0} record { factor = (suc f) ; remain = zero ; is-factor = fa } i0f div = ⊥-elim (nat-≡< fa (
+decf-step : {i k i0 : ℕ } → (if : Factor k (suc i)) → (i0f : Factor k i0) → Dividable k (suc i - remain if)  → Dividable k (i - remain (decf {i} {k} if))
+decf-step {i} {k} {i0} if i0f div = 
+  decf-step1 {i} {k} {i0} (factor if) (remain if) (is-factor if) i0f div where
+   decf-step1 : {i k i0 : ℕ } →  (f r : ℕ) → (fa : f * k + r ≡ suc i) →  (i0f : Factor k i0)
+        → Dividable k (suc i - r)  → Dividable k (i - remain (decf record {factor = f ; remain = r ; is-factor = fa}))
+   decf-step1 {i} {k} {i0}  f (suc r) fa i0f div = 
+      record { factor = f ;  is-factor = (
+        begin f * k + 0 ≡⟨ {!!} ⟩
+        i - r ≡⟨ refl ⟩
+         (i - remain (decf (record { factor = f ; remain = suc r ; is-factor = fa }))) ∎ ) }  where
+            open ≡-Reasoning
+   decf-step1 {i} {zero} {i0} (suc f) zero fa i0f div = ⊥-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 div = 
-   record { factor = f ;  is-factor = (
+   decf-step1 {i} {suc k} {i0} (suc f)  zero fa i0f div = 
+      record { factor = f ;  is-factor = (
         begin f * suc k + 0 ≡⟨ {!!} ⟩
-        i - k  ≡⟨ refl  ⟩
-        (i - remain (decf (record { factor = suc f ; remain = zero ; is-factor = fa }))) ∎ ) }  where open ≡-Reasoning
-decf-step {i} {suc k} {i0} record { factor = zero ;  remain = zero ; is-factor = fa } i0f div = {!!}
-decf-step {i} {k} {i0} record { factor = zero ; remain = suc r ; is-factor = fa } i0f div = {!!}
-decf-step {i} {k} {i0} record { factor = suc f1 ; remain = suc r ; is-factor = fa } i0f div = 
-   record { factor = f ;  is-factor = (
-        begin f * k + 0 ≡⟨ {!!} ⟩
-         (i - remain (decf {i} {k} (record { factor = f ; remain = suc r ; is-factor = fa }))) ∎ ) }  where
-   open ≡-Reasoning
-   f = suc f1
-   df1 : remain (decf {i} {k} (record { factor = f ; remain = suc r ; is-factor = fa })) ≡ r
-   df1 = {!!}
+        i - k ∎ ) }  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