# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1689668437 -32400
# Node ID 168465a7b107b02d2f3004a8ef1ac5e5d8f63a18
# Parent  ab531332d0a16b4fe96e5992e8db4709592aaab9
...

diff -r ab531332d0a1 -r 168465a7b107 automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 17:10:30 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 17:20:37 2023 +0900
@@ -642,12 +642,10 @@
              ... | 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 : ℕ) → toℕ (F←Q fa (f b)) ≤ i → 0 < count-B i 
-        lem32 zero le with ≤-∨ le
-        lem32 zero le | case2 lt = ⊥-elim ( nat-≤> lt (s≤s z≤n ))
-        lem32 zero le | case1 eq with is-B (Q←F fa ( fromℕ< {0} 0<fa ))
-        ... | yes isb = ≤-refl
+    lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where
+        lem32 : (i : ℕ) → toℕ (F←Q fa (f b)) ≡ i → 0 < count-B i 
+        lem32 zero   eq with is-B (Q←F fa ( fromℕ< {0} 0<fa ))
+        ... | yes isb = s≤s z≤n 
         ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where
             lem33 : f b ≡ Q←F fa ( fromℕ< {0} 0<fa )
             lem33 = begin
@@ -656,18 +654,20 @@
               Q←F fa ( fromℕ< fin<n )  ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq fin<n 0<fa) ⟩
               Q←F fa ( fromℕ< {0} 0<fa ) ∎ where
                 open ≡-Reasoning
-        lem32 (suc n) le with <-cmp (finite fa) (suc n) | inspect count-B (suc n) | ≤-∨ le
-        ... | tri< a ¬b ¬c | _ | case1 eq = lem32 n ? -- ? -- ⊥-elim ( nat-≤> le (<-trans fin<n a) )
-        ... | tri< a ¬b ¬c | _ | case2 lt = lem32 n ? -- ? -- ⊥-elim ( nat-≤> le (<-trans fin<n a) )
-        ... | tri≈ ¬a eq1 ¬c | _ | case1 eq = ? -- ⊥-elim ( nat-≤> le (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 fin<n ))
-        ... | tri≈ ¬a eq1 ¬c | _ | case2 lt = ? -- ⊥-elim ( nat-≤> le (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 fin<n ))
-        ... | tri> ¬a ¬b c | record { eq = eq1 } | case1 eq with is-B (Q←F fa (fromℕ< c))   
+        lem32 (suc i) eq with <-cmp (finite fa) (suc i) | inspect count-B (suc i) 
+        ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≡< eq (<-trans fin<n a) )
+        ... | tri≈ ¬a eq1 ¬c | _ = ⊥-elim ( nat-≡< eq (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 fin<n ))
+        ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c))   
         ... | yes isb = s≤s z≤n 
-        ... | no nisb = lem32 n ? -- (≤-trans a≤sa le)
-        lem32 (suc n) le | tri> ¬a ¬b c | record { eq = eq1 } | case2 lt with is-B (Q←F fa (fromℕ< c))   
-        ... | yes isb = s≤s z≤n 
-        ... | no nisb = lem32 n ? -- (≤-trans a≤sa le)
-
+        ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where
+            lem33 : f b ≡ Q←F fa ( fromℕ< c)
+            lem33 = begin
+              f b ≡⟨ sym (finiso→  fa _) ⟩
+              Q←F fa ( F←Q fa (f b))  ≡⟨ sym (cong (λ k → Q←F fa k)  ( fromℕ<-toℕ _ fin<n)) ⟩
+              Q←F fa ( fromℕ< fin<n )  ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq fin<n c ) ⟩
+              Q←F fa ( fromℕ< c ) ∎ where
+                open ≡-Reasoning
+ 
     cb<mb : (b : B) → pred (count-B (toℕ (F←Q fa (f b)))) < maxb
     cb<mb b = sx≤y→x<y ( begin
         suc ( pred (count-B (toℕ (F←Q fa (f b)))))  ≡⟨ sucprd (lem31 b) ⟩