# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1623978251 -32400
# Node ID db05b4df5b67ad2acaedce1d44d983208a038e29
# Parent  a5c8a90615be20679f34abdd9541cf4bbb1d005b
...

diff -r a5c8a90615be -r db05b4df5b67 automaton-in-agda/src/prime.agda
--- a/automaton-in-agda/src/prime.agda	Fri Jun 18 07:54:25 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Fri Jun 18 10:04:11 2021 +0900
@@ -86,31 +86,32 @@
      suc (factorial m + m * factorial m)  ≡⟨ refl ⟩
      suc (factorial (suc m)) ∎  where open ≤-Reasoning
   fact< : (n : ℕ) → 0 < n → n < suc (suc m) → Dividable n ( factorial (suc m) )
-  fact< n 0<n n<m = record { factor = F.f1 (fact1 m init1) ? ? ? ; is-factor = last  } where
+  fact< n 0<n n<m = record { factor = F.f1 (fact1 m ) n 0<n n<m ; is-factor = last } where
      record F (m : ℕ) : Set where
         field
           f1 : (n : ℕ ) → 0 < n →  n < suc (suc m ) → ℕ
-          is-f1 : (0<n : 0 < n ) →  (n<m : n < suc (suc m )) → f1 n 0<n n<m * n ≡ factorial (suc m)
+          is-f1 : (n : ℕ) (0<n : 0 < n ) →  (n<m : n < suc (suc m )) → f1 n 0<n n<m * n ≡ factorial (suc m)
      init0 : (n : ℕ) → 0 < n → n < 2 → 1 * n ≡ factorial 1
      init0 (suc zero) (s≤s lt) (s≤s (s≤s z≤n)) = refl
      init : F 0
-     init = record { f1 = ? ; is-f1 = λ 0<n lt → init0 n 0<n lt } where
-     init1 : F ( m - m )
-     init1 = subst (λ k → F k ) (sym (minus<=0 {m} ≤-refl)) init
-     fact1 : (j : ℕ ) → F ((suc m) - suc j) → F j  
-     fact1 zero f = record { f1 = ? ;  is-f1 = fact2 } where
-        fact3 : 0 < n → n < suc (suc m) →  F.f1 f n ? ? * n ≡ factorial (suc m)
-        fact3 = ? -- F.is-f1 f ? ? 
-        fact2 : 0 < n → n < 2 → F.f1 f n ? ? * n ≡ factorial 1
-        fact2 = {!!}
-     fact1 (suc j) f with <-cmp n j
-     ... | tri< a ¬b ¬c = record { f1 = ? ;  is-f1 = {!!} }
-     ... | tri≈ ¬a refl ¬c = record { f1 = ? ;  is-f1 = λ lt → {!!} }
-     ... | tri> ¬a ¬b c = record { f1 = ? ;  is-f1 = λ lt → {!!} }
-     last : F.f1 (fact1 m init1 ) ? ? ? * n + 0 ≡ factorial (suc m)
+     init = record { f1 = λ n lt lt1 → 1 ; is-f1 = λ n 0<n lt → init0 n 0<n lt } where
+     fact1 : (j : ℕ ) → F j
+     fact1 zero = init
+     fact1 (suc m) = record { f1 = fact2 ; is-f1 = fact3 }  where
+        fact2 : (n : ℕ ) →  0 < n →  n < suc (suc (suc m )) → ℕ
+        fact2 (suc j)  with <-cmp n j
+        ... | tri< a ¬b ¬c = {!!}
+        ... | tri≈ ¬a refl ¬c = {!!}
+        ... | tri> ¬a ¬b c = {!!}
+        fact3 : (n : ℕ ) (0<n : 0 < n) (n<m : n < suc (suc (suc m))) → fact2 n 0<n n<m * n ≡ factorial (suc (suc m))
+        fact3 n 0<n n<m  with <-cmp n {!!}
+        ... | tri< a ¬b ¬c = {!!}
+        ... | tri≈ ¬a b ¬c = {!!}
+        ... | tri> ¬a ¬b c = {!!}
+     last :  F.f1 (fact1 m) n 0<n n<m * n + 0 ≡ factorial (suc m)
      last = begin
-         F.f1 (fact1 m init1) ? ? ? * n + 0 ≡⟨ +-comm _ 0 ⟩
-         F.f1 (fact1 m init1) ? ? ? * n ≡⟨ F.is-f1 (fact1 m init1) 0<n n<m ⟩
+         F.f1 (fact1 m ) n 0<n n<m * n + 0 ≡⟨ +-comm _ 0 ⟩
+         F.f1 (fact1 m ) n 0<n n<m * n ≡⟨  F.is-f1 (fact1 m) n 0<n n<m ⟩
          factorial (suc m) ∎  where open ≡-Reasoning
   fact : (n : ℕ) → Prime n → Dividable n ( factorial (suc m) )
   fact n p = fact< n (<-trans (s≤s z≤n) (Prime.p>0 p)) ( prime<max n p )