--- a/automaton-in-agda/src/gcd.agda	Tue Jun 22 10:14:37 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Tue Jun 22 14:48:46 2021 +0900
@@ -298,6 +298,8 @@
 gcd-divable i j  = n-induction {_} {_} {ℕ ∧ ℕ}
    {λ p  → Dividable ( gcd (proj1 p) (proj2 p) ) (proj1 p) ∧ Dividable ( gcd (proj1 p)  (proj2 p) ) (proj2 p)} F I ⟪ i , j ⟫ where
         F : ℕ ∧ ℕ → ℕ
+        F ⟪ 0 , j ⟫ = 0
+        F ⟪ suc i , 0 ⟫ = 0
         F ⟪ i , j ⟫ with <-cmp i j
         ... | tri< a ¬b ¬c = j
         ... | tri≈ ¬a b ¬c = 0
@@ -329,29 +331,47 @@
         Fcase22 : { i j : ℕ } → j ≡ 0 → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
         Fcase22 {i} {0} refl = ⟪  subst (λ k → Dividable k i) (sym (gcd20 i)) div=
                                 , subst (λ k → Dividable k 0) (sym (gcd20 i)) div0 ⟫
+        Fn0 : {i  : ℕ} → (F (next  ⟪ i , 0 ⟫) ≡ 0 ) ∧ (F (next  ⟪ 0 , i ⟫) ≡ 0 )
+        Fn0 {zero} = ⟪ refl , refl ⟫
+        Fn0 {suc i} = ⟪ refl , refl ⟫
+        F01 : {i j : ℕ} → F ⟪ i , j - i ⟫ ≡ 0 → F (next ⟪ i , j - i ⟫) ≡ 0
+        F01 {zero} {zero} eq = refl
+        F01 {zero} {suc j} eq = refl
+        F01 {suc i} {zero} eq = refl
+        F01 {suc i} {suc j} eq with <-cmp i j --  F ⟪ i - (j - i) , j - i ⟫ ∨ F ⟪ (j - i) -i , j - i -i ⟫
+        ... | tri< a ¬b ¬c =  {!!}
+        ... | tri≈ ¬a refl ¬c = subst (λ k → F (next ⟪ suc i , k ⟫) ≡ 0) F011 (proj1 (Fn0 {suc i})  ) where
+             F011 : 0 ≡ i - i 
+             F011 = sym (minus<=0 {i} ≤-refl )
+        ... | tri> ¬a ¬b c = subst (λ k → F (next ⟪ suc i , k ⟫) ≡ 0) F011 (proj1 (Fn0 {suc i})  ) where
+             F011 : 0 ≡ j - i 
+             F011 = sym (minus<=0 {j} {i} (<to≤ c) )
         F00 :  {p : ℕ ∧ ℕ} → F (next p) ≡ zero → Dividable (gcd (proj1 p) (proj2 p)) (proj1 p) ∧ Dividable (gcd (proj1 p) (proj2 p)) (proj2 p)
-        F00 {⟪ i , j ⟫} eq with <-cmp i j
-        ... | tri< a ¬b ¬c with <-cmp i (j - i)
-        ... | tri< a₁ ¬b₁ ¬c₁ = Fcase1 (sym ( i-j=0→i=j (<to≤ a) eq ))
-        ... | tri≈ ¬a b ¬c₁ = {!!} -- i = j - i
-        ... | tri> ¬a ¬b₁ c = Fcase21 eq -- case2 (case1 eq)
-        F00 {⟪ i , j ⟫} eq | tri≈ ¬a b ¬c = {!!} -- case1 b
-        F00 {⟪ i , j ⟫} eq | tri> ¬a ¬b c with <-cmp (i - j) j
-        ... | tri< a ¬b₁ ¬c = Fcase22 eq 
+        F00 {⟪ 0 , j ⟫} eq = Fcase21 refl
+        F00 {⟪ i , 0 ⟫} eq = Fcase22 refl
+        F00 {⟪ suc i , suc j ⟫} eq with <-cmp (suc i) (suc j)
+        ... | tri< a ¬b ¬c with F0 {suc i} {j - i} eq
+        ... | case1 (si=j-i)  = {!!}
+        ... | case2 (case2 j-i=0 ) = {!!}
+        F00 {⟪ suc i , suc j ⟫} eq | tri≈ ¬a b ¬c = {!!} -- case1 b
+        F00 {⟪ suc i , suc j ⟫} eq | tri> ¬a ¬b c with <-cmp (i - j) (suc j)
+        ... | tri< a ¬b₁ ¬c = Fcase22 {!!}
         ... | tri≈ ¬a₁ b ¬c = {!!} -- i -j = j
-        ... | tri> ¬a₁ ¬b₁ c₁ = Fcase1 ( i-j=0→i=j (<to≤ c) eq )
+        ... | tri> ¬a₁ ¬b₁ c₁ = Fcase1 ( i-j=0→i=j (<to≤ c) {!!} )
 
         Fdecl :  ( p : ℕ ∧ ℕ ) → 0 < F p  →  F (next p) < F p
-        Fdecl ⟪ i , j ⟫ 0<F with <-cmp i j 
-        ... | tri< a ¬b ¬c = fd1  where
-             fd1 : F ⟪ i , j - i ⟫ < j
+        Fdecl ⟪ 0 , j ⟫ ()
+        Fdecl ⟪ suc i , 0 ⟫ ()
+        Fdecl ⟪ suc i , suc j ⟫ 0<F with <-cmp (suc i) (suc j)
+        ... | tri< a ¬b ¬c = fd1 where
+             fd1 : F ⟪ suc i , j - i ⟫ < suc j
              fd1 with <-cmp i ( j - i )
              ... | tri< a ¬b ¬c = {!!}  -- j - i < j
              ... | tri≈ ¬a b ¬c = {!!} -- 0 < j
-             ... | tri> ¬a ¬b c = a -- i < j
+             ... | tri> ¬a ¬b c = {!!} -- i < j
         ... | tri≈ ¬a refl ¬c  = ⊥-elim ( nat-≡< refl 0<F )
         ... | tri> ¬a ¬b c = fd2 where
-             fd2 : F ⟪ i  - j , j  ⟫ < i
+             fd2 : F ⟪ i  - j , suc j  ⟫ < suc i
              fd2 = {!!}
 
         ind3 : {i j : ℕ } → i < j