# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624415460 -32400
# Node ID 6e8b163ca73717b10ae95a1322867bb11d7487c0
# Parent  9a36ec9b824a53c60b13e0a28ed05985ef9abb7a
...

diff -r 9a36ec9b824a -r 6e8b163ca737 automaton-in-agda/src/prime.agda
--- a/automaton-in-agda/src/prime.agda	Tue Jun 22 20:14:40 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Wed Jun 23 11:31:00 2021 +0900
@@ -47,6 +47,44 @@
 
 open import logic
 open _∧_
+
+nonPrime1 : { n : ℕ } → 1 < n → ¬ Prime n → NonPrime n
+nonPrime1 {n} 1<n np = n-induction {_} {_} {G} {λ m → NonPrime n } (λ g → G.g g) I
+         record { p = n ; 1<p = 1<n ; g = n ; npr = λ lt → np ; div = div= ; is-g = is-g= refl } where
+    record G  : Set where
+      field
+        p : ℕ
+        1<p : 1 < p 
+        g : ℕ
+        div : Dividable p n
+        npr : g > 0 → ¬ Prime p
+        is-g : (j : ℕ) → g ≤ j → j < p → gcd p j ≡ 1
+    is-g= : {g p : ℕ} → g ≡ p →  (j : ℕ) → g ≤ j → j < p → gcd p j ≡ 1
+    is-g= eq _ g≤j j<p = ⊥-elim ( nat-≡< eq (≤-trans (s≤s g≤j ) j<p))
+    next : G → G 
+    next g = next1 (G.g g) (gcd (G.g g) (G.p g)) where
+      next1  : ℕ →  ℕ  → G 
+      next1  0 _ = g
+      next1  _ 0  = g
+      next1  (suc m) 1 = record g { g = m ;  npr = λ lt → G.npr g {!!} ; is-g = {!!} }
+      next1  (suc m) (suc (suc f))  with PrimeP (suc (suc f))
+      ... | yes p = record { p = suc (suc f) ; g = 0 ; 1<p = Prime.p>1 p ; div = {!!} ; npr = λ () ; is-g = {!!} }
+      ... | no np = record { p = suc (suc f) ; g = suc (suc f)  ; 1<p = s≤s (s≤s z≤n) ; div = {!!} ; npr = λ lt → np ; is-g = is-g= refl }
+    pzero : (p : G ) → G.g (next p) ≡ zero → NonPrime n
+    pzero g eq = record { factor = G.p g ; prime = record { p>1 = G.1<p g ; isPrime = {!!} } ;  dividable = G.div g }
+    ind :  (p : G ) → NonPrime n → NonPrime n
+    ind = {!!}
+    decline : (p : G ) → 0 < G.g p → G.g (next p) < G.g p
+    decline = {!!}
+    I : Ninduction G  _  (λ g → G.g g)
+    I = record {
+              pnext = next
+            ; fzero = λ {p} → pzero p
+            ; decline = λ {p} → decline p
+            ; ind = λ {p} → ind p
+          }
+
+
 nonPrime : { n : ℕ } → 1 < n → ¬ Prime n → NonPrime n
 nonPrime {n} 1<n np = np1 n (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) ) where
     mg1 :  (m : ℕ )→ ( (j : ℕ ) → suc m ≤ j → j < n → gcd n j ≡ 1  ) →  gcd n (suc m) ≡ 1 → (j : ℕ) → m ≤ j → j < n → gcd n j ≡ 1
@@ -61,9 +99,7 @@
     ... | tri≈ ¬a b ¬c = np1 m (mg1 m mg b )
     ... | tri> ¬a ¬b c with PrimeP ( gcd n (suc m) )
     ... | yes y = record { factor = gcd n (suc m) ; prime = y ;  dividable = proj1 (gcd-divable n (suc m) ) }
-    ... | no ngcd = record { factor = NonPrime.factor np2 ; prime = NonPrime.prime np2 ;  dividable = {!!} }where
-        np2 : NonPrime (gcd n (suc m))
-        np2 = nonPrime {gcd n (suc m)} c ngcd
+    ... | no ngcd = np1 m (mg1 m mg {!!} )
 
 
 prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j )