# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624071165 -32400
# Node ID 764bc577b1e9e6443b5987ead8f16c4b47098f95
# Parent  f1370437c68eb50f2d4db9b3205a33e40a7dbff0
...

diff -r f1370437c68e -r 764bc577b1e9 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Sat Jun 19 10:54:51 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Sat Jun 19 11:52:45 2021 +0900
@@ -219,11 +219,32 @@
       factor jf * j0  ≡⟨ cong (λ k → factor jf * k) y  ⟩
       factor jf * 0  ≡⟨ *-comm (factor jf) 0  ⟩
       0 ∎   where open ≡-Reasoning
-gcd-divable zero (suc i0) (suc (suc j)) j0 if jf if=0 jf=0
-    with gcd-divable i0 (suc i0) (suc j) (suc (suc j))
-        record { factor = {!!} ; is-factor = {!!} ; remain = suc j - i0 }
-        record { factor = {!!} ; is-factor = {!!} ; remain = i0 - suc j } refl refl 
-... | t = ⟪ record { factor = {!!} ; is-factor = {!!} } , {!!} ⟫ -- Dividable (gcd1 i0 (suc i0) (suc j) (suc (suc j))) (suc i0)
+gcd-divable zero (suc i0) (suc (suc j)) j0 if jf if=0 jf=0  =
+    ⟪ record { factor = gg8 ; is-factor = {!!} } , record { factor = gg8 ; is-factor = {!!} } ⟫ where
+    gg8 : ℕ
+    gg8 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
+    gg9 : factor if * suc i0 + (suc j - i0) ≡ suc (suc j) 
+    gg9 = begin
+      factor if * suc i0 + (suc j - i0)  ≡⟨ {!!}  ⟩
+      factor if * suc i0 + (suc (suc j) - zero)  ≡⟨ {!!} ⟩
+      factor if * suc i0 + remain if ≡⟨ is-factor if ⟩
+      j0  ≡⟨ {!!}  ⟩
+      suc (suc j)  ∎   where open ≡-Reasoning
+    gg10 : factor jf * suc (suc j) + (i0 - suc j) ≡ suc i0
+    gg10 = begin
+      factor jf * suc (suc j) + (i0 - suc j) ≡⟨ {!!}  ⟩
+      factor jf * j0 + remain jf ≡⟨ is-factor jf  ⟩
+      suc i0  ∎   where open ≡-Reasoning
+    gg7 : Dividable gg8 (suc i0) ∧ Dividable gg8 (suc (suc j))
+    gg7 = gcd-divable i0 (suc i0) (suc j) (suc (suc j))
+        record { factor = factor if ; is-factor = gg9 ; remain = suc j - i0 }
+        record { factor = factor jf ; is-factor = gg10 ; remain = i0 - suc j } refl refl 
+--if   : Factor (suc i0) j0    --  factor if * (suc i0) + (suc (suc j) - zero  ≡ j0
+--jf   : Factor j0 (suc i0)    --  factor jf * j0 + (zero - suc (suc j))) ≡ suc i0
+--if=0 : remain if ≡ (suc (suc j) - zero)
+--jf=0 : remain jf ≡ (zero - suc (suc j))
+--    factor if * suc i0 + (suc j - i0) ≡ suc (suc j)
+--    factor jf * suc (suc j) + (i0 - suc j) ≡ suc i
 gcd-divable (suc zero) i0 zero j0 if jf if=0 jf=0 = ⟪ record { factor = i0 ; is-factor = gg3 } ,  record { factor = j0 ; is-factor = gg3 } ⟫
 gcd-divable (suc (suc i)) i0 zero zero if jf if=0 jf=0 = ⟪ record { factor = 1 ; is-factor = gg1 } ,  record { factor = factor if ; is-factor = gg4 } ⟫
    where