# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624865204 -32400
# Node ID ea3d184c4b1f8e85271ad3d3f0bfe8824806a2ab
# Parent  bed5daf239cd62297f93d10ab1ae144547319c92
...

diff -r bed5daf239cd -r ea3d184c4b1f automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 28 14:57:40 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 28 16:26:44 2021 +0900
@@ -355,6 +355,29 @@
 gcd-next1 {i0} {j} {j0} g = record { i<i0 = refl-≤s ; j<j0 = refl-≤s
   ; div-i = proj1 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) ; div-j = proj2 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) }
 
+-- i<i0  : zero ≤ i0
+-- j<j0  : 1 ≤ j0
+-- div-i : Dividable i0 ((j0 + zero) - 1)  -- fi * i0 ≡ (j0 + zero) - 1
+-- div-j : Dividable j0 ((i0 + 1) - zero) --  fj * j0 ≡ (i0 + 1) - zero
+gcd-01 : {i0 j0 : ℕ } → (d : GCD zero i0 1 j0 ) → Dividable.factor (GCD.div-i d) ≡ 1
+gcd-01 {i0} {j0} d with <-cmp (Dividable.factor (GCD.div-i d)) 1
+... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< {!!} (GCD.j<j0 d)) where
+   ge003 : 0 ≡ j0
+   ge003 = sym ( begin
+              j0 ≡⟨ {!!} ⟩
+              (( j0 + 0 ) - 1) + 1 ≡⟨ {!!} ⟩
+              {!!} * i0  ≡⟨ {!!} ⟩
+              0 * i0  ≡⟨ {!!} ⟩
+              0 ∎ ) 
+           where open ≡-Reasoning
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b c = {!!}  where --    ((j0 + zero) - 1) * fj ≡ ((i0 + 1) - zero) * fi → fi > 1 → fj ≡ 0
+                                 --
+   ge004 : Dividable.factor (GCD.div-i d) ≡ 0
+   ge004 = {!!}
+   ge005 : Dividable.factor (GCD.div-i d) ≡ 0 →  Dividable.factor (GCD.div-j d) ≡ 0
+   ge005 = {!!}
+
 -- gcd-dividable1 : ( i i0 j j0 : ℕ )
 --      → Dividable i0  (j0 + i - j ) ∨ Dividable j0 (i0 + j - i)
 --      → Dividable ( gcd1 i i0 j j0  ) i0 ∧ Dividable ( gcd1 i i0 j j0  ) j0
@@ -567,7 +590,15 @@
 ... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () }
 ... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () } 
 ... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ;  is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0 }
-gcd-euclid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
+-- i<i0  : zero ≤ i0
+-- j<j0  : 1 ≤ j0
+-- div-i : Dividable i0 ((j0 + zero) - 1)  -- fi * i0 ≡ (j0 + zero) - 1
+-- div-j : Dividable j0 ((i0 + 1) - zero) --  fj * j0 ≡ (i0 + 1) - zero
+gcd-euclid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } where
+   ge6 :  i0 > j0 → i0 - j0 ≡ gcd1 zero i0 1 j0
+   ge6 i0>j0 =  begin
+       i0 - j0   ≡⟨  {!!}  ⟩
+       1   ∎ where open ≡-Reasoning
 gcd-euclid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 
 gcd-euclid1 zero (suc i0) (suc (suc j)) j0 di with gcd-euclid1 i0 (suc i0) (suc j) (suc (suc j)) ( gcd-next1 di )
 ... | e = record { eqa = ea + eb * f ; eqb =  eb