# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624580432 -32400
# Node ID 9011d76a67fb1c1c2ad015ff2b7d03c4a7fa6494
# Parent  54977cc189e648713c2a9f3bcb88d28856eebf9b
...

diff -r 54977cc189e6 -r 9011d76a67fb automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Fri Jun 25 08:49:12 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Fri Jun 25 09:20:32 2021 +0900
@@ -466,25 +466,29 @@
             ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev
           } 
 
--- gcd-equlid : ( i i0 j j0 b0  : ℕ ) 
---           Dividable i0  (j0 + i - j ) ∨ Dividable j0 (i0 + j - i)
---           (x0 < j0 → gcd x0 j0 ≡ 1) → gcd (i0 * b0) j0  ≡ j0 → gcd1 i i0 j j0  ≡ 1 → gcd b0 j0  ≡ j0
--- gcd-equlid zero i0 zero j0  a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 with <-cmp i0 j0
--- ... | tri< a' ¬b ¬c = {!!}
--- ... | tri≈ ¬a refl ¬c = {!!}
--- ... | tri> ¬a ¬b c = {!!}
--- gcd-equlid zero i0 (suc zero) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = {!!}
--- gcd-equlid zero zero (suc (suc j)) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = {!!}
--- gcd-equlid zero (suc i0) (suc (suc j)) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 =    {!!}
---     gcd-equlid i0 (suc i0) (suc j) (suc (suc j)) {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
--- gcd-equlid (suc zero) i0 zero j0 = {!!}
--- gcd-equlid (suc (suc i)) i0 zero zero a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = {!!}
--- gcd-equlid (suc (suc i)) i0 zero (suc j0) a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = 
---      gcd-equlid (suc i) (suc (suc i)) j0 (suc j0) {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
--- gcd-equlid (suc zero) i0 (suc j) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 =  
---      gcd-equlid zero i0 j j0 {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
--- gcd-equlid (suc (suc i)) i0 (suc j) j0 a a0 b b0 ab ab0 x0 x0<j0 gxj=1 a*b gabj ga1 = 
---      gcd-equlid (suc i) i0 j j0 {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
+-- record Equlid (i j gcd : ℕ ) : Set where
+--   field
+--     eqa : ℕ
+--     eqb : ℕ
+--     gcd-equ : ((eqa * i) - (eqb * j) ≡ gcd  ) ∨ ((eqb * j) - (eqa * i) ≡ gcd )
+-- 
+-- gcd-equlid1 : ( i i0 j j0 : ℕ )  → Equlid i0 j0 (gcd1 i i0 j j0)
+-- gcd-equlid1 zero i0 zero j0  with <-cmp i0 j0
+-- ... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; gcd-equ = case1 {!!} }
+-- ... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; gcd-equ = case1 {!!} }
+-- ... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ; gcd-equ = case2 {!!} }
+-- gcd-equlid1 zero i0 (suc zero) j0 = record { eqa = 1 ; eqb = 1 ; gcd-equ = case1 {!!} }
+-- gcd-equlid1 zero zero (suc (suc j)) j0 = record { eqa = 0 ; eqb = 1 ; gcd-equ = case2 {!!} }
+-- gcd-equlid1 zero (suc i0) (suc (suc j)) j0 with gcd-equlid1 i0 (suc i0) (suc j) (suc (suc j)) 
+-- ... | e = record { eqa = Equlid.eqb e ; eqb =  Equlid.eqa e ; gcd-equ = {!!} }
+-- gcd-equlid1 (suc zero) i0 zero j0 = {!!}
+-- gcd-equlid1 (suc (suc i)) i0 zero zero = {!!}
+-- gcd-equlid1 (suc (suc i)) i0 zero (suc j0) with gcd-equlid1 (suc i) (suc (suc i)) j0 (suc j0) 
+-- ... | e = {!!}
+-- gcd-equlid1 (suc zero) i0 (suc j) j0 =
+--      gcd-equlid1 zero i0 j j0 
+-- gcd-equlid1 (suc (suc i)) i0 (suc j) j0  = 
+--      gcd-equlid1 (suc i) i0 j j0 
 
 
 gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1