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

diff -r 5b985fea126e -r 8cd5bea05150 automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 21:02:46 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 22:34:17 2023 +0900
@@ -619,45 +619,23 @@
     cb<mb = ?
 
     cb00 : (n : ℕ) → n < count-B (finite fa) → CountB n
-    cb00 n n<cb = ? where
-
-        lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
-        lem07 n 0 eq with is-B (Q←F fa (fromℕ< ? )) | inspect count-B 0
-        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym ? ; cb=n = trans eq1 eq 
-                ; cb-inject = λ cb1 iscb1 cb1eq → ? } 
-        ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq ? )
-        lem07 n (suc i) eq with <-cmp (finite fa) i
-        ... | tri< a ¬b ¬c = ?
-        ... | tri≈ ¬a b ¬c = ?
-        ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))| inspect count-B (suc i)
-        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym ? ; cb=n = trans eq1 ?
-                 ; cb-inject = λ cb1 iscb1 cb1eq → ? } 
-        ... | no nisb | record { eq = eq1 } = lem07 n i ?
+    cb00 n n<cb = lem09 (finite fa) (count-B (finite fa)) (<-transˡ a<sa n<cb) refl where
 
         lem09 : (i j : ℕ) →  suc n ≤ j → j ≡ count-B i →  CountB n
-        lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
-        ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq ))
-        ... | case2 (s≤s lt) with is-B (Q←F fa (fromℕ< ? )) | inspect count-B 0
-        ... | yes isb | record { eq = eq1 } = ⊥-elim ?
-        ... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) ?)
-        lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
-        ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq ))
-        ... | case2 (s≤s lt) with <-cmp (finite fa) i
-        ... | tri< a ¬b ¬c = ?
-        ... | tri≈ ¬a b ¬c = ?
-        ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))| inspect count-B (suc i)
-        ... | yes isb | record { eq = eq1 } = ? -- lem09 i j lt ?
-        ... | no nisb | record { eq = eq1 } = ? -- lem09 i (suc j) (≤-trans lt a≤sa) ?
-
-        -- cb01 : (i j : ℕ) → suc n ≤ j  → j ≡ count-B j → CountB n
-        -- cb01 0 (suc j) (s≤s le) eq with
-        -- cb01 (suc i) (suc j) (s≤s le) eq = ?
-        -- cb01 (suc i) (suc j) j<fa i<cb with is-B (Q←F fa (fromℕ< j<fa ))
-        -- ... | yes y = record { b = Is.a y ; cb = suc (CountB.cb pcb)  ; b=cn = ? ; cb=n = ? ; cb-inject = ? }  where
-        --     pcb : CountB j
-        --     pcb = cb00 (suc
-        -- ... | no nb  = record { b = CountB.b pcb ; cb = CountB.cb pcb ; b=cn = CountB.b=cn pcb ; cb=n = ? ; cb-inject = ? } where
-        --     pcb : CountB j
-        --     pcb = cb00 i j (<-trans a<sa j<fa)
+        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) = ?
+        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
+        ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c))
+        ... | 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 →  ?} 
+        ... | case2 (s≤s lt) = lem09 i j lt (cong pred eq)
 
 -- end