# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624324477 -32400
# Node ID b6c874c5c52d6d36357dd14ec79922836c6aea58
# Parent  7b093d0e5a61fd4f0842d223ec9855540c20b38c
...

diff -r 7b093d0e5a61 -r b6c874c5c52d automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 21 23:19:51 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Tue Jun 22 10:14:37 2021 +0900
@@ -249,9 +249,17 @@
         decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m 
         ind : (p : ℕ ) → Dec (Dividable k (p - k) ) → Dec (Dividable k p )
         ind p (yes y) with <-cmp p k
-        ... | tri< a ¬b ¬c = no  {!!}
         ... | tri≈ ¬a refl ¬c = yes (subst (λ g → Dividable k g) (minus+n ≤-refl ) (proj1 ( div+div y div= ))) 
         ... | tri> ¬a ¬b k<p  = yes (subst (λ g → Dividable k g) (minus+n (<-trans k<p a<sa)) (proj1 ( div+div y div= ))) 
+        ... | tri< a ¬b ¬c with <-cmp p 0
+        ... | tri≈ ¬a refl ¬c₁ = yes div0
+        ... | tri> ¬a ¬b₁ c = no (λ d → not-div p (Dividable.factor d) a c (Dividable.is-factor d) ) where
+            not-div : (p f : ℕ) → p < k  → 0 < p → f * k + 0 ≡ p → ⊥
+            not-div (suc p) (suc f) p<k 0<p eq = nat-≡< (sym eq) ( begin -- ≤-trans p<k {!!}) -- suc p ≤ k
+              suc (suc p) ≤⟨ p<k ⟩
+              k ≤⟨ x≤x+y  ⟩
+              k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩
+              suc f * k + 0 ∎  ) where open ≤-Reasoning  
         ind p (no n) = no (λ d → n (proj1 (div-div k>1 d div=))  ) 
         I : Ninduction ℕ  _  F
         I = record {
@@ -304,16 +312,34 @@
         F0 {zero} {suc j} p =  case2 (case1 refl)
         F0 {suc i} {zero} p =  case2 (case2 refl)
         F0 {suc i} {suc j} p with <-cmp i j
-        ... | tri< a ¬b ¬c = {!!} -- ⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
+        ... | tri< a ¬b ¬c = ⊥-elim ( F11 p )  where
+             F11 : F ⟪ suc i , suc j  ⟫ ≡ 0 → ⊥
+             F11 eq with <-cmp (suc i) (suc j)
+             ... | tri≈ ¬a b ¬c = nat-≡< b (s≤s a)
         ... | tri≈ ¬a refl ¬c = case1 refl
-        ... | tri> ¬a ¬b c = {!!} --⊥-elim ( nat-≡< (sym p) (s≤s z≤n ))
+        ... | tri> ¬a ¬b c =  ⊥-elim  (F11 p) where 
+             F11 : F ⟪ suc i , suc j  ⟫ ≡ 0 → ⊥
+             F11 eq with <-cmp (suc i) (suc j)
+             ... | tri≈ ¬a b ¬c = nat-≡< (sym b) (s≤s c)
+        Fcase1 : { i j : ℕ } → i ≡ j → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
+        Fcase1 {i} {i} refl = ⟪  subst (λ k → Dividable k i) (sym (gcdmm i i)) div= , subst (λ k → Dividable k i) (sym (gcdmm i i)) div= ⟫
+        Fcase21 : { i j : ℕ } → i ≡ 0 → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
+        Fcase21 {0} {j} refl = ⟪  subst (λ k → Dividable k 0) (sym (trans (gcdsym {0} {j} ) (gcd20 j)))div0
+                                , subst (λ k → Dividable k j) (sym (trans (gcdsym {0} {j}) (gcd20 j))) div= ⟫
+        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 ⟫
         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 F0 {i} {j} {!!}
-        ... | case1 refl = ⟪  subst (λ k → Dividable k i) (sym (gcdmm i i)) div= , subst (λ k → Dividable k i) (sym (gcdmm i i)) div= ⟫
-        ... | case2 (case1 refl) = ⟪  subst (λ k → Dividable k i) (sym (trans (gcdsym {0} {j} ) (gcd20 j)))div0
-                                    , subst (λ k → Dividable k j) (sym (trans (gcdsym {0} {j}) (gcd20 j))) div= ⟫
-        ... | case2 (case2 refl) = ⟪  subst (λ k → Dividable k i) (sym (gcd20 i)) div=
-                                    , subst (λ k → Dividable k j) (sym (gcd20 i)) div0 ⟫
+        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 
+        ... | tri≈ ¬a₁ b ¬c = {!!} -- i -j = j
+        ... | tri> ¬a₁ ¬b₁ c₁ = Fcase1 ( i-j=0→i=j (<to≤ c) eq )
 
         Fdecl :  ( p : ℕ ∧ ℕ ) → 0 < F p  →  F (next p) < F p
         Fdecl ⟪ i , j ⟫ 0<F with <-cmp i j 
@@ -399,7 +425,7 @@
         I = record {
               pnext = λ p → next p
             ; fzero = F00 
-            ; decline = λ {p} lt → {!!}
+            ; decline = λ {p} lt → Fdecl p lt
             ; ind = λ {p} prev → ind p prev
           }