--- a/automaton-in-agda/src/finiteSetUtil.agda	Sat Jul 15 18:44:51 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 08:14:57 2023 +0900
@@ -572,75 +572,44 @@
 
 open import bijection using ( InjectiveF ; Is )
 
+record countB (B : Set) : Set where
+   field
+      cb : ℕ
+      ib : {i : ℕ} → i < cb → B
+      ib-inject : {i j : ℕ} → (i<cb : i < cb) → (j<cb : j < cb) → ib i<cb ≡ ib j<cb  → i ≡ j
+
 inject-fin : {A B : Set}  (fa : FiniteSet A ) 
    → (fi : InjectiveF B A) 
    → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f fi) a)  )
    → FiniteSet B
-inject-fin {A} {B} fa fi is-B = B<n→B (inf00 (finite fa) NP.≤-refl ) where
-   f = InjectiveF.f fi
-   record B<n ( n : ℕ ) : Set where
-       field 
-           b : B  
-           b<n : toℕ (F←Q fa (f b)) < n
-   B<n→B : FiniteSet (B<n (finite fa)) → FiniteSet B
-   B<n→B b<n = record {
-       finite = finite b<n
-       ; Q←F = λ fb → B<n.b (Q←F b<n fb )
-       ; F←Q =  λ b → F←Q b<n record { b = b ; b<n = fin<n }
+inject-fin {A} {B} fa fi is-B = record {
+       finite = countB.cb (cb00 (finite fa) NP.≤-refl )
+       ; Q←F = λ fb → countB.ib (cb00 (finite fa) NP.≤-refl ) (fin<n {_} {fb})
+       ; F←Q =  λ b → fromℕ< (cb<cb (fin<n {_} {F←Q fa (InjectiveF.f fi b)} ))
        ; finiso→ = ?
        ; finiso← = ?
-       } 
-   inf00 : (n : ℕ ) → n ≤ finite fa → FiniteSet (B<n n)
-   inf00 zero lt = record {
-       finite = 0
-       ; Q←F = inf03
-       ; F←Q =  inf01
-       ; finiso→ = inf02
-       ; finiso← = λ ()
        } where
-          inf03 : Fin 0 → B<n zero
-          inf03 ()
-          inf01 : B<n zero → Fin 0
-          inf01 b with B<n.b<n b
-          ... | le = ⊥-elim ( nat-≤> le (s≤s z≤n )) 
-          inf02 : (b : B<n zero) → inf03 (inf01 b) ≡ b
-          inf02 b = ⊥-elim ( nat-≤> (B<n.b<n b) (s≤s z≤n ) )
-   inf00 (suc n) le with is-B ( Q←F fa ( fromℕ< {n} ?  ))
-   ... | yes isb = record {
-        finite = suc (finite bp)
-        ; Q←F =  info05
-        ; F←Q =  info06
-        ; finiso→ = ?
-        ; finiso← = ?
-        } where
-          n≤fa : suc n ≤ finite fa
-          n≤fa = le
-          bp : FiniteSet (B<n n)
-          bp = inf00 n (NP.≤-trans a≤sa le )
-          info05 : Fin (suc (finite bp)) → B<n (suc n)
-          info05 x with <-cmp (toℕ x) (finite bp)
-          ... | tri< a ¬b ¬c = record { b = B<n.b (Q←F bp ? ) ; b<n = ? }
-          ... | tri≈ ¬a b ¬c = ?
-          ... | tri> ¬a ¬b c = ?
-          -- zero = record { b = Is.a isb ; b<n = ? }
-          -- info05 (suc x) = record { b = B<n.b (Q←F bp x) ; b<n = ? }
-          info06 : B<n (suc n) → Fin (suc (finite bp))
-          info06 x with <-cmp (toℕ (F←Q fa (f (B<n.b x)))) n
-          ... | tri< a ¬b ¬c = fromℕ< {toℕ (F←Q fa (f (B<n.b x)))} ?
-          ... | tri≈ ¬a b ¬c = fromℕ< {n} ?
-          ... | tri> ¬a ¬b c = ?
-   ... | no nisb = record {
-        finite = finite bp
-        ; Q←F =  λ x → record { b = B<n.b ( Q←F bp x) ; b<n = ? }
-        ; F←Q =  info07
-        ; finiso→ = ?
-        ; finiso← = ?
-        } where
-          bp : FiniteSet (B<n n)
-          bp = inf00 n (NP.≤-trans a≤sa le )
-          info07 : B<n (suc n) → Fin (finite bp)
-          info07 x with <-cmp (toℕ (F←Q fa (f (B<n.b x)))) n
-          ... | t = ?
+   f = InjectiveF.f fi
+   cb00 : (i : ℕ) → i ≤ finite fa → countB B
+   cb00 0 i<fa = record { cb = 0 ; ib = λ () ; ib-inject = λ () }
+   cb00 (suc i) i<fa with is-B (Q←F fa (fromℕ< i<fa))
+   ... | yes y = record { cb = suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))) ; ib = cb01 ; ib-inject = cb02 } where
+        pcb : countB B
+        pcb = cb00 i (NP.≤-trans a≤sa i<fa)
+        cb01 :  {j : ℕ} → j < suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))) → B
+        cb01 {j} j<c with <-∨ j<c
+        ... | case1 eq = Is.a y
+        ... | case2 lt = countB.ib (cb00 i (NP.≤-trans a≤sa i<fa)) lt
+        cb02 : {i1 : ℕ} {j : ℕ}
+            (i<cb : i1 < suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))))
+            (j<cb : j < suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa)))) →
+            cb01 i<cb ≡ cb01 j<cb → i1 ≡ j
+        cb02 = ?
+   ... | no n  = record { cb = countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))       ; ib = cb01 
+     ; ib-inject = countB.ib-inject (cb00 i (NP.≤-trans a≤sa i<fa))} where
+        cb01 :  {j : ℕ} → j < countB.cb (cb00 i (NP.≤-trans a≤sa i<fa)) → B
+        cb01 {j} j<c = countB.ib (cb00 i (NP.≤-trans a≤sa i<fa)) j<c
 
+   cb<cb : {i : ℕ} → (i<fa : i ≤ finite fa) → countB.cb (cb00 _ i<fa) < countB.cb (cb00 _ NP.≤-refl)  
+   cb<cb = ?
 
-