--- a/automaton-in-agda/src/prime.agda	Tue Jun 22 15:39:02 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Tue Jun 22 20:14:40 2021 +0900
@@ -26,30 +26,44 @@
 PrimeP : ( n : ℕ ) → Dec ( Prime n )
 PrimeP 0 = no (λ p → ⊥-elim ( nat-<> (Prime.p>1 p) (s≤s z≤n))) 
 PrimeP 1 = no (λ p → ⊥-elim ( nat-≤> (Prime.p>1 p) (s≤s (≤-refl))))
-PrimeP (suc (suc n)) = isPrime1 (suc (suc n)) (suc n) (s≤s (s≤s z≤n)) a<sa (λ i m<i i<n → isp0 (suc n) i m<i i<n ) where
+PrimeP (suc (suc n)) = isPrime1 (suc (suc n)) (suc n) (s≤s (s≤s z≤n)) a<sa (λ i m<i i<n → isp0 (suc n) i (<to≤ m<i) i<n ) where  
    isp0 : (n : ℕ) (i : ℕ) ( n<i : n ≤ i) ( i<n : i < suc n ) →  gcd (suc n) i ≡ 1
    isp0  n i n<i i<n with <-cmp i n
    ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> n<i a) 
    ... | tri≈ ¬a refl ¬c = gcd203 i
    ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c i<n )
-   isPrime1 : ( n m : ℕ ) → n > 1 → m < n → ( (i : ℕ) → m ≤ i → i < n  →  gcd n i ≡ 1 )  → Dec ( Prime n )
-   isPrime1 n zero n>1 m<n lt = yes record { isPrime = λ j j<i 0<j → lt j z≤n j<i ; p>1 = n>1 } 
+   isPrime1 : ( n m : ℕ ) → n > 1 → m < n → ( (i : ℕ) → m < i → i < n  →  gcd n i ≡ 1 )  → Dec ( Prime n )
+   isPrime1 n zero n>1 m<n lt = yes record { isPrime = λ j j<i 0<j → lt j 0<j j<i ; p>1 = n>1 } 
    isPrime1 n (suc m) n>1 m<n lt with <-cmp (gcd n (suc m)) 1
    ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> ( gcd>0 n (suc m) (<-trans (s≤s z≤n) n>1) (s≤s z≤n)) a )
    ... | tri≈ ¬a b ¬c = isPrime1 n m n>1 (<-trans a<sa m<n) isp1 where
-    --   (i : ℕ) → suc m ≤ i → suc i ≤ n → gcd1 n n i i ≡ 1
-        isp1 :  (i : ℕ) → m ≤ i → i < n → gcd n i ≡ 1
-        isp1 = {!!}
+    --  lt : (i : ℕ) → suc m ≤ i → suc i ≤ n → gcd1 n n i i ≡ 1
+        isp1 :  (i : ℕ) → m < i → i < n → gcd n i ≡ 1
+        isp1 i m<i i<n with <-cmp (suc m) i
+        ... | tri< a ¬b ¬c = lt i a i<n
+        ... | tri≈ ¬a m=i  ¬c = subst (λ k → gcd n k ≡ 1) m=i b -- gcd n (suc m) ≡ 1 →  gcd n i ≡ 1
+        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c) -- suc i ≤ suc m →  i < m
    ... | tri> ¬a ¬b c = no ( λ p → nat-≡< (sym (Prime.isPrime p (suc m) m<n (s≤s z≤n) )) c )
 
+open import logic
+open _∧_
 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
+    mg1 m mg gcd j m<j j<n with <-cmp j (suc m)
+    ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> (≤-trans {!!} m<j) a)
+    ... | tri≈ ¬a refl ¬c = gcd
+    ... | tri> ¬a ¬b c = mg j {!!} j<n
     np1 : ( m : ℕ ) → ( (j : ℕ ) → m ≤ j → j < n → gcd n j ≡ 1  ) → NonPrime n
     np1 zero mg = ⊥-elim ( np record { isPrime = λ j lt _ → mg j z≤n lt ; p>1 = 1<n } ) -- zero < j , j < n
     np1 (suc m) mg with <-cmp ( gcd n (suc m) ) 1
     ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> ( gcd>0 n (suc m) (<-trans (s≤s z≤n) 1<n) (s≤s z≤n)) a )
-    ... | tri≈ ¬a b ¬c = np1 m {!!}
-    ... | tri> ¬a ¬b c = record { factor = gcd n (suc m) ; prime = {!!} ;  dividable = record { factor = {!!} ; is-factor = {!!} } }
+    ... | 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
 
 
 prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) 
@@ -79,9 +93,9 @@
      (suc m) * 1 ≤⟨  *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩
      (suc m) * factorial m ≡⟨ refl ⟩
      factorial (suc m)  ∎  where open ≤-Reasoning
-  factorial⟩m : (m : ℕ) → m ≤ factorial m
-  factorial⟩m zero = z≤n
-  factorial⟩m (suc m) = begin
+  m<factorial : (m : ℕ) → m ≤ factorial m
+  m<factorial zero = z≤n
+  m<factorial (suc m) = begin
      suc m ≡⟨ cong suc (+-comm 0 _) ⟩
      1 * suc m ≡⟨ *-comm 1 _ ⟩
      (suc m) * 1 ≤⟨  *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩
@@ -131,4 +145,7 @@
   ... | yes p = pmax _ f>m p 
   ... | no np = div+1 (Prime.p>1 (NonPrime.prime p1)) (fact (NonPrime.factor p1) (NonPrime.prime p1) ) (NonPrime.dividable p1) where
       p1 : NonPrime  ( suc (factorial (suc m)) )
-      p1 = nonPrime {!!} np
+      p1 = nonPrime (begin
+       2 ≤⟨ s≤s ( s≤s z≤n) ⟩
+       suc (suc m) ≤⟨ s≤s (m<factorial (suc m))  ⟩
+       suc (factorial (suc m)) ∎ ) np where open ≤-Reasoning