# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1689662856 -32400
# Node ID e7a7cab74ca1e6b652b45f33d6f4a9b37de33720
# Parent  bc2cb1c6bc80c9fd1fb07b9a531980990f24ba8b
...

diff -r bc2cb1c6bc80 -r e7a7cab74ca1 automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 10:48:40 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 15:47:36 2023 +0900
@@ -649,14 +649,14 @@
         ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where
             lem33 : f b ≡ Q←F fa ( fromℕ< {0} 0<fa )
             lem33 = begin
-              f b ≡⟨ ? ⟩
-              Q←F fa ( F←Q fa (f b))  ≡⟨ sym (cong (λ k → Q←F fa k)  ( fromℕ<-toℕ _ ?)) ⟩
-              Q←F fa ( fromℕ< ? )  ≡⟨ ? ⟩
+              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 _ _ (sym eq) fin<n 0<fa) ⟩
               Q←F fa ( fromℕ< {0} 0<fa ) ∎ where
                 open ≡-Reasoning
         lem32 (suc n) eq with <-cmp (finite fa) (suc n)
-        ... | tri< a ¬b ¬c = ?
-        ... | tri≈ ¬a b ¬c = ?
+        ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym eq) (<-trans fin<n a) )
+        ... | tri≈ ¬a eq1 ¬c = ⊥-elim ( nat-≡< (sym eq) (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 fin<n ))
         ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))
         ... | yes isb = ?
         ... | no nisb = ?