--- a/automaton-in-agda/src/gcd.agda	Fri Jun 25 09:20:32 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Fri Jun 25 20:16:53 2021 +0900
@@ -466,30 +466,89 @@
             ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev
           } 
 
--- 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
+record Equlid (i j gcd : ℕ ) : Set where
+  field
+    eqa : ℕ
+    eqb : ℕ
+    gcd-equ : ((eqa * i) - (eqb * j) ≡ gcd  ) ∨ ((eqb * j) - (eqa * i) ≡ gcd )
+
+di-next : {i i0 j j0 : ℕ} → Dividable i0  ((j0 + suc i) - suc j ) ∧ Dividable j0 ((i0 + suc j) - suc i) →
+           Dividable i0  ((j0 + i) - j ) ∧ Dividable j0 ((i0 + j) - i) 
+di-next {i} {i0} {j} {j0} x =
+      ⟪ ( subst (λ k → Dividable i0 (k - suc j)) ( begin
+               j0 + suc i ≡⟨ sym (+-assoc j0 1 i ) ⟩ 
+               (j0 + 1) + i ≡⟨ cong (λ k → k + i) (+-comm j0 _ ) ⟩ 
+               suc (j0 + i) ∎ ) (proj1 x) ) ,
+       ( subst (λ k → Dividable j0 (k - suc i)) ( begin
+               i0 + suc j ≡⟨ sym (+-assoc i0 1 j ) ⟩ 
+               (i0 + 1) + j ≡⟨ cong (λ k → k + j) (+-comm i0 _ ) ⟩ 
+               suc (i0 + j) ∎ ) (proj2 x) ) ⟫    
+           where open ≡-Reasoning
+
+postulate 
+   gcd-equlid : ( p q r : ℕ )  → 1 < p  → ((i : ℕ ) → i < p → 0 < i   → gcd p i ≡ 1)  →  Dividable p (q * r)  → Dividable p q ∨ Dividable p r
+   gcd-equlid1 : ( i i0 j j0 : ℕ )  → Dividable i0  ((j0 + i) - j ) ∧ Dividable j0 ((i0 + j) - i) → Equlid i0 j0 (gcd1 i i0 j j0)
+-- gcd-equlid1 zero i0 zero j0 di 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) 
+-- gcd-equlid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = 1 ; gcd-equ = case1 {!!} }
+-- gcd-equlid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; gcd-equ = case2 {!!} }
+-- gcd-equlid1 zero (suc i0) (suc (suc j)) j0 di with gcd-equlid1 i0 (suc i0) (suc j) (suc (suc j))  {!!} 
+-- ... | e with Equlid.gcd-equ e
+-- ... | case1 x = record { eqa = ea + eb * f ; eqb =  eb ; gcd-equ = case1 (trans  ge1 x ) } where
+--    --   Dividable (suc i0) ((j0 + 0) - (suc (suc j))) ∨ Dividable j0 (suc (i0 + suc (suc j)))
+--    --        (j0 + 0) - (suc (suc j)) ≡ f * (suc i0)
+--    ea = Equlid.eqa e 
+--    eb = Equlid.eqb e
+--    f = Dividable.factor (proj1 di)
+--    ge1 : ((ea + eb * f) * suc i0) - (eb * j0)  ≡ (ea * suc i0) - (eb * suc (suc j))       
+--    ge1  = begin
+--       ((ea + eb * f ) * suc i0) - (eb * j0)  ≡⟨ {!!} ⟩ 
+--       ((ea + eb * f ) * suc i0) - eb * (f * (suc i0) + suc (suc j) )  ≡⟨ {!!} ⟩ 
+--       ((ea + eb * f ) * suc i0 - (eb * f) * (suc i0)) + eb * suc (suc j)   ≡⟨ {!!} ⟩ 
+--       ((ea * suc i0 + (eb * f ) * suc i0 ) - (eb * f) * (suc i0)) + eb * suc (suc j)   ≡⟨ {!!} ⟩ 
+--       (ea * suc i0) - (eb * suc (suc j)) ∎ where open ≡-Reasoning
+-- ... | case2 x = {!!}
+-- gcd-equlid1 (suc zero) i0 zero j0 di = {!!}
+-- gcd-equlid1 (suc (suc i)) i0 zero zero di = {!!}
+-- gcd-equlid1 (suc (suc i)) i0 zero (suc j0) di 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 
+-- gcd-equlid1 (suc zero) i0 (suc j) j0 di =
+--      gcd-equlid1 zero i0 j j0  (di-next di)
+-- gcd-equlid1 (suc (suc i)) i0 (suc j) j0  di = 
+--      gcd-equlid1 (suc i) i0 j j0 (di-next di)
+
 
+div→gcd : {n k : ℕ } → k > 1 → Dividable k n → gcd n k ≡ k
+div→gcd {n} {k} k>1 = n-induction {_} {_} {ℕ} {λ m → Dividable k m → gcd m k ≡ k } (λ x → x) I n where
+        decl : {m  : ℕ } → 0 < m → m - k < m
+        decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m 
+        ind : (m : ℕ ) → (Dividable k (m - k) → gcd (m - k) k ≡ k) → Dividable k m → gcd m k ≡ k
+        ind m prev d with <-cmp (suc m) k
+        ... | tri≈ ¬a refl ¬c = ⊥-elim ( div+1 k>1 d div= )
+        ... | tri>  ¬a ¬b c = subst (λ g → g ≡ k) ind1 ( prev (proj2 (div-div k>1 div= d))) where
+           ind1 : gcd (m - k) k ≡ gcd m k
+           ind1 = begin
+               gcd (m - k) k  ≡⟨ sym (gcd+j (m - k)  _) ⟩
+               gcd (m - k + k) k ≡⟨ cong (λ g → gcd g k) (minus+n {m} {k} c) ⟩
+               gcd m k ∎ where open ≡-Reasoning
+        ... | tri< a ¬b ¬c with <-cmp 0 m 
+        ... | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim ( div<k k>1 a₁ (<-trans a<sa a) d )
+        ... | tri≈ ¬a refl ¬c₁ = subst (λ g → g ≡ k ) (gcdsym {k} {0} ) (gcd20 k)
+        fzero : (m : ℕ) → (m - k) ≡ zero → Dividable k m → gcd m k ≡ k 
+        fzero 0 eq d = trans  (gcdsym {0} {k} ) (gcd20 k) 
+        fzero (suc m) eq d with <-cmp (suc m) k
+        ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 (s≤s z≤n) a d )
+        ... | tri≈ ¬a refl ¬c = gcdmm k k
+        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (minus>0 c) )
+        I : Ninduction ℕ  _  (λ x → x)
+        I = record {
+              pnext = λ p → p - k
+            ; fzero = λ {m} eq → fzero m eq
+            ; decline = λ {m} lt → decl lt 
+            ; ind = λ {p} prev → ind p prev
+          } 
 
 gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1
 gcdmul+1 zero n = gcd204 n

--- a/automaton-in-agda/src/root2.agda	Fri Jun 25 09:20:32 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Fri Jun 25 20:16:53 2021 +0900
@@ -20,80 +20,21 @@
 
 open _∧_
 
-div→gcd : {n k : ℕ } → k > 1 → Dividable k n → gcd n k ≡ k
-div→gcd {n} {k} k>1 = n-induction {_} {_} {ℕ} {λ m → Dividable k m → gcd m k ≡ k } (λ x → x) I n where
-        decl : {m  : ℕ } → 0 < m → m - k < m
-        decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m 
-        ind : (m : ℕ ) → (Dividable k (m - k) → gcd (m - k) k ≡ k) → Dividable k m → gcd m k ≡ k
-        ind m prev d with <-cmp (suc m) k
-        ... | tri≈ ¬a refl ¬c = ⊥-elim ( div+1 k>1 d div= )
-        ... | tri>  ¬a ¬b c = subst (λ g → g ≡ k) ind1 ( prev (proj2 (div-div k>1 div= d))) where
-           ind1 : gcd (m - k) k ≡ gcd m k
-           ind1 = begin
-               gcd (m - k) k  ≡⟨ sym (gcd+j (m - k)  _) ⟩
-               gcd (m - k + k) k ≡⟨ cong (λ g → gcd g k) (minus+n {m} {k} c) ⟩
-               gcd m k ∎ where open ≡-Reasoning
-        ... | tri< a ¬b ¬c with <-cmp 0 m 
-        ... | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim ( div<k k>1 a₁ (<-trans a<sa a) d )
-        ... | tri≈ ¬a refl ¬c₁ = subst (λ g → g ≡ k ) (gcdsym {k} {0} ) (gcd20 k)
-        fzero : (m : ℕ) → (m - k) ≡ zero → Dividable k m → gcd m k ≡ k 
-        fzero 0 eq d = trans  (gcdsym {0} {k} ) (gcd20 k) 
-        fzero (suc m) eq d with <-cmp (suc m) k
-        ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 (s≤s z≤n) a d )
-        ... | tri≈ ¬a refl ¬c = gcdmm k k
-        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (minus>0 c) )
-        I : Ninduction ℕ  _  (λ x → x)
-        I = record {
-              pnext = λ p → p - k
-            ; fzero = λ {m} eq → fzero m eq
-            ; decline = λ {m} lt → decl lt 
-            ; ind = λ {p} prev → ind p prev
-          } 
-
---  n ≡ i * k + r
---  n^2 = (i * k)^2 + i * r * k  + r^2
---  r^2 | k   yes → jj
-
 open import prime
 
 -- equlid : ( n m k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * m ) → Dividable k n ∨ Dividable k m
 -- equlid = {!!}
 
--- divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n
--- divdable^2 zero zero 1<k 1<n pk dn2 = {!!}
--- divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
--- ... | yes y = y
--- ... | no non with equlid (suc n) (suc n) (suc k) 1<k {!!} pk dn2
--- ... | case1 dn = dn
--- ... | case2 dm = dm
-
-even^2 : {n : ℕ} → even ( n * n ) → even n
-even^2 {n} en with even? n
+divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n
+divdable^2 zero zero () 1<n pk dn2
+divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
 ... | yes y = y
-... | no ne = ⊥-elim ( odd4 ((2 * m) + 2 * m * suc (2 * m)) (n+even {2 * m} {2 * m * suc (2 * m)} ee3 ee4) (subst (λ k → even k) ee2 en )) where
-    m : ℕ
-    m = Odd.j ( odd3 n ne )
-    ee3 : even (2 * m)
-    ee3 = subst (λ k → even k ) (*-comm m 2) (n*even {m} {2} tt )
-    ee4 : even ((2 * m) * suc (2 * m))
-    ee4 = even*n {(2 * m)} {suc (2 * m)} (even*n {2} {m} tt )
-    ee2 : n * n ≡ suc (2 * m) + ((2 * m) * (suc (2 * m) ))
-    ee2 = begin n * n ≡⟨ cong ( λ k → k * k) (Odd.is-twice (odd3 n ne)) ⟩
-       suc (2 * m) * suc (2 * m) ≡⟨ *-distribʳ-+ (suc (2 * m)) 1 ((2 * m) ) ⟩
-        (1 * suc (2 * m)) + 2 * m * suc (2 * m) ≡⟨ cong (λ k → k + 2 * m * suc (2 * m)) (begin
-        suc m + 1 * m + 0 * (suc m + 1 * m ) ≡⟨ +-comm (suc m + 1 * m) 0 ⟩
-        suc m + 1 * m  ≡⟨⟩
-        suc (2 * m)
-        ∎) ⟩ suc (2 * m)  + 2 * m * suc (2 * m) ∎ where open ≡-Reasoning
+... | no non with gcd-equlid (suc k) (suc n) (suc n) 1<k (Prime.isPrime pk) dn2
+... | case1 dn = dn
+... | case2 dm = dm
 
-e3 : {i j : ℕ } → 2 * i ≡ 2 * j →  i ≡ j
-e3 {zero} {zero} refl = refl
-e3 {suc x} {suc y} eq with <-cmp x y
-... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (s≤s (<-trans (<-plus a) (<-plus-0 (s≤s (<-plus a ))))))
-... | tri≈ ¬a b ¬c = cong suc b
-... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c ))))))
-
-open Factor
+p2 : Prime 2
+  p2 = record { p>1 = a<sa ; isPrime = {!!} }
 
 -- gcd-div : ( i j k : ℕ ) → (if : Dividable k i) (jf : Dividable k j )
 --    → Dividable k ( gcd i  j )
@@ -104,58 +45,9 @@
     rot13 d refl with Dividable.factor d | Dividable.is-factor d
     ... | zero | ()
     ... | suc n | ()
-    rot11 : {m : ℕ } → even m → Factor 2 m 
-    rot11 {zero} em = record { factor = 0 ; remain = 0 ; is-factor = refl }
-    rot11 {suc zero} ()
-    rot11 {suc (suc m) } em = record { factor = suc (factor fc ) ; remain = remain fc ; is-factor = isfc } where
-       fc : Factor 2 m
-       fc = rot11 {m} em
-       isfc : suc (factor fc) * 2 + remain fc ≡ suc (suc m)
-       isfc = begin
-          suc (factor fc) * 2 + remain fc ≡⟨ cong (λ k →  k + remain fc) (*-distribʳ-+ 2 1 (factor fc)) ⟩
-          ((1 * 2) +  (factor fc)* 2 ) + remain fc ≡⟨⟩
-          ((1 + 1) +  (factor fc)* 2 ) + remain fc ≡⟨ cong (λ k → k + remain fc) (+-assoc 1  1 _ ) ⟩
-          (1 + (1 +  (factor fc)* 2 )) + remain fc ≡⟨⟩
-          suc (suc ((factor fc * 2) + remain fc )) ≡⟨ cong (λ x → suc (suc x)) (is-factor fc) ⟩
-          suc (suc m) ∎ where open ≡-Reasoning
-    rot5 : {n : ℕ} → n > 1 → n > 0
-    rot5 {n} lt = <-trans a<sa lt 
-    rot1 : even ( m * m )
-    rot1 = subst (λ k → even k ) rot4 (n*even {n * n} {2} tt ) where
-       rot4 : (n * n) * 2 ≡ m * m  
-       rot4 = begin
-          (n * n) * 2     ≡⟨ *-comm (n * n) 2 ⟩
-          2 * ( n * n )   ≡⟨ sym (*-assoc 2 n n) ⟩
-          2 *  n * n      ≡⟨ 2nm ⟩
-          m * m           ∎ where open ≡-Reasoning
-    E : Even m
-    E = e2 m ( even^2 {m} ( rot1 ))
-    rot2 : 2 * n * n ≡ 2 * Even.j E * m
-    rot2 = subst (λ k → 2 * n * n ≡ k * m ) (Even.is-twice E) 2nm
-    rot3 : n * n ≡ Even.j E * m
-    rot3 = e3 ( begin
-          2 * (n * n)   ≡⟨ sym (*-assoc 2 n _) ⟩
-          2 *  n * n    ≡⟨ rot2 ⟩
-          2 * Even.j E * m ≡⟨  *-assoc 2 (Even.j E)  m  ⟩
-          2 * (Even.j E * m)  ∎ ) where open ≡-Reasoning
-    rot7 : even n  
-    rot7 =  even^2 {n} (subst (λ k → even k) (sym rot3) ((n*even {Even.j E} {m} ( even^2 {m} ( rot1 )))))
-    f2 : Factor 2 n
-    f2 = rot11 rot7
-    f3 : ( n : ℕ) → (e : even n ) →  remain (rot11 {n} e)  ≡ 0
-    f3 zero e = refl
-    f3 (suc (suc n)) e = f3 n e 
-    fm : Factor 2 m
-    fm = record { factor = Even.j E ; remain = 0 ; is-factor = fm1 } where
-       fm1 : Even.j E * 2 + 0 ≡ m
-       fm1 = begin
-         Even.j E * 2 + 0 ≡⟨ +-comm _ 0  ⟩
-         Even.j E * 2  ≡⟨  *-comm (Even.j E) 2  ⟩
-         2 * Even.j E  ≡⟨  sym ( Even.is-twice E )  ⟩
-         m ∎  where open ≡-Reasoning
+    dm : Dividable 2 m
+    dm = divdable^2 m 2 a<sa m>1 p2 record { factor = n * n ; is-factor = {!!} }
     dn : Dividable 2 n
-    dn = record { factor = factor f2 ; is-factor = subst (λ k → factor f2 * 2 + k ≡ n ) (f3 n rot7) (is-factor f2)  }
-    dm : Dividable 2 m
-    dm = record { factor = factor fm ; is-factor = is-factor fm }
+    dn = divdable^2 n 2 a<sa n>1 p2 record { factor = Dividable.factor dm * m ; is-factor = {!!} }