# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1689603688 -32400
# Node ID 9f3647718a9f45ab0a72fb5a1f929790e3cb814f
# Parent  8cd5bea051501aee25c6b66acadb52fde804741c
...

diff -r 8cd5bea05150 -r 9f3647718a9f automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 22:34:17 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 23:21:28 2023 +0900
@@ -625,9 +625,15 @@
         lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) | inspect count-B 0
         ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )
         ... | yes isb | record { eq = eq1 } with ≤-∨ (s≤s le)
-        ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = ? ; cb=n = trans eq1 (sym (trans eq2 eq))
-                ; cb-inject = λ cb1 iscb1 cb1eq →  ?}
-        ... | case2 (s≤s lt) = ?
+        ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans eq1 (sym (trans eq2 eq))
+                ; cb-inject = λ cb1 iscb1 cb1eq →  ?} where
+             lem10 : 0 ≡ toℕ (F←Q fa (f (Is.a isb)))
+             lem10 = begin
+                0 ≡⟨ sym ( toℕ-fromℕ< 0<fa ) ⟩
+                toℕ (fromℕ< {0} 0<fa ) ≡⟨ cong toℕ (sym (finiso← fa _))  ⟩
+                toℕ (F←Q fa (Q←F fa (fromℕ< {0} 0<fa )))  ≡⟨ cong (λ k → toℕ ((F←Q fa k))) (sym (Is.fa=c isb)) ⟩
+                toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning
+        ... | case2 (s≤s lt) = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-transʳ z≤n lt)  ))
         lem09 (suc i) (suc j) (s≤s le) eq with <-cmp (finite fa) i | inspect count-B (suc i)
         ... | tri< a ¬b ¬c | _ = lem09 i (suc j) (s≤s le) eq
         ... | tri≈ ¬a b ¬c | _ = lem09 i (suc j) (s≤s le) eq
@@ -635,7 +641,13 @@
         ... | no nisb = lem09 i (suc j) (s≤s le) eq
         ... | yes isb with ≤-∨ (s≤s le)
         ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ;  b=cn = ?  ; cb=n = trans eq1 (sym (trans eq2 eq))
-                ; cb-inject = λ cb1 iscb1 cb1eq →  ?} 
+                ; cb-inject = λ cb1 iscb1 cb1eq →  ?} where
+              lem10 :  suc i ≡ toℕ (F←Q fa (f (Is.a isb)))
+              lem10 = begin
+                suc i ≡⟨ cong suc (sym ( toℕ-fromℕ< c )) ⟩
+                ? ≡⟨ ? ⟩
+                toℕ (F←Q fa (Q←F fa (fromℕ< c )))  ≡⟨ cong (λ k → toℕ ((F←Q fa k))) (sym (Is.fa=c isb)) ⟩
+                toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning
         ... | case2 (s≤s lt) = lem09 i j lt (cong pred eq)
 
 -- end