# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1689641050 -32400
# Node ID 5aae7a429f37d119fde1b4b6058cc0081e6b0117
# Parent  34426fe27745577057d2d18a8b81410693113d66
...

diff -r 34426fe27745 -r 5aae7a429f37 automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 09:16:53 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 09:44:10 2023 +0900
@@ -641,11 +641,24 @@
              ... | yes isb = ? -- refl-≤s
              ... | no nisb = ? -- ≤-refl
 
+    lem31 : (b : B) → 0 < count-B (toℕ (F←Q fa (f b)))
+    lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where
+        lem32 : (i : ℕ) → i ≡ toℕ (F←Q fa (f b)) → 0 < count-B i 
+        lem32 zero eq with is-B (Q←F fa ( fromℕ< {0} 0<fa ))
+        ... | yes isb = ?
+        ... | no nisb = ?
+        lem32 (suc n) eq with <-cmp (finite fa) (suc n)
+        ... | tri< a ¬b ¬c = ?
+        ... | tri≈ ¬a b ¬c = ?
+        ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))
+        ... | yes isb = ?
+        ... | no nisb = ?
 
     cb<mb : (b : B) → pred (count-B (toℕ (F←Q fa (f b)))) < maxb
-    cb<mb b = sx≤y→x<y (begin
-        ? ≤⟨ ? ⟩ 
-        ? ∎ where
+    cb<mb b = sx≤y→x<y ( begin
+        suc ( pred (count-B (toℕ (F←Q fa (f b)))))  ≡⟨ sucprd (lem31 b) ⟩ 
+        count-B (toℕ (F←Q fa (f b)))  ≤⟨ lem02 ⟩ 
+        count-B (finite fa)   ∎ ) where
           open ≤-Reasoning
           lem02 : count-B (toℕ (F←Q fa (f b))) ≤ count-B (finite fa)
           lem02 = count-B-mono (<to≤ (fin<n {_} {(F←Q fa (f b))})) 
@@ -707,13 +720,11 @@
              CB = cb00 (toℕ (fromℕ< (cb<mb b))) fin<n
              isb : Is B A f (Q←F fa (fromℕ< fin<n))
              isb = ?
-             lem31 : 0 < count-B (toℕ (F←Q fa (f b)))
-             lem31 = ?
              lem30 : count-B (CountB.cb CB) ≡ count-B (toℕ (F←Q fa (InjectiveF.f fi b)))
              lem30 = begin
                  count-B (CountB.cb CB) ≡⟨ CountB.cb=n CB ⟩
                  suc (toℕ (fromℕ< (cb<mb b)))  ≡⟨ cong suc (toℕ-fromℕ< (cb<mb b)) ⟩
-                 suc (pred (count-B (toℕ (F←Q fa (f b))))) ≡⟨ sucprd lem31 ⟩
+                 suc (pred (count-B (toℕ (F←Q fa (f b))))) ≡⟨ sucprd (lem31 b) ⟩
                  count-B (toℕ (F←Q fa (f b))) ∎