--- a/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 19:21:51 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Wed Jul 19 07:08:43 2023 +0900
@@ -702,24 +702,43 @@
 
         lem06 : (i j : ℕ) → (i<fa : i < finite fa) (j<fa : j < finite fa) 
             →  Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B i ≡ count-B j → i ≡ j
-        lem06 i j i<fa j<fa bi bj eq = ? where
+        lem06 i j i<fa j<fa bi bj eq = lem08 where
             lem20 : (i j : ℕ) → i < j → (i<fa : i < finite fa) (j<fa : j < finite fa) 
                 →  Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B j ≡ count-B i → ⊥
-            lem20 zero (suc j) i<j bi bj le = ?
+            lem20 zero (suc j) i<j i<fa j<fa bi bj le with <-cmp (finite fa) (suc j) 
+            ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa)
+            ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa)
+            ... | tri> ¬a ¬b c with  is-B (Q←F fa ( fromℕ< 0<fa )) | inspect count-B 0 | is-B (Q←F fa (fromℕ< c)) | inspect count-B (suc j)
+            ... | no nisc  | _ | _ | _ = ⊥-elim (nisc record { a = Is.a bi ; fa=c = lem26 } ) where
+                 lem26 : f (Is.a bi) ≡ Q←F fa (fromℕ< 0<fa)
+                 lem26 = trans (Is.fa=c bi) (cong (Q←F fa) (fromℕ<-cong _ _ refl i<fa 0<fa) )
+            ... |  yes _ | _ | no nisc | _  = ⊥-elim (nisc record { a = Is.a bj ; fa=c = lem26 } ) where
+                 lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c)
+                 lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) )
+            ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = ⊥-elim ( nat-≤> lem25 a<sa) where
+                 lem24 : count-B j ≡ 0
+                 lem24 = cong pred le
+                 lem25 : 1 ≤ 0
+                 lem25 = begin
+                    1 ≡⟨ sym eq1 ⟩
+                    count-B 0 ≤⟨ count-B-mono {0} {j} z≤n ⟩
+                    count-B j ≡⟨ lem24 ⟩
+                    0 ∎ where open ≤-Reasoning
             lem20 (suc i) zero () bi bj le
             lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ?
+
             lem08 : i ≡ j
             lem08 with <-cmp i j
-            ... | tri< a ¬b ¬c = ⊥-elim ( lem20 i j a ? ? bi bj (sym eq) )
+            ... | tri< a ¬b ¬c = ⊥-elim ? -- ( lem20 i j a i<fa j<fa bi bj (sym eq) )
             ... | tri≈ ¬a b ¬c = b
-            ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ ? ? bj bi eq )
+            ... | tri> ¬a ¬b c₁ = ⊥-elim ? -- ( lem20 j i c₁ j<fa i<fa bj bi eq )
 
         lem09 : (i j : ℕ) →  suc n ≤ j → j ≡ count-B i →  CountB n
         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 = lem10 ; cb=n = trans eq1 (sym (trans eq2 eq))
-                ; cb-inject = ? } where
+                ; cb-inject = λ cb1 c1<fa b1 eq → lem06 0 cb1 0<fa c1<fa isb b1 eq } where
              lem10 : 0 ≡ toℕ (F←Q fa (f (Is.a isb)))
              lem10 = begin
                 0 ≡⟨ sym ( toℕ-fromℕ< 0<fa ) ⟩
@@ -734,7 +753,7 @@
         ... | 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 = lem11 ; cb=n = trans eq1 (sym (trans eq2 eq ))
-                ; cb-inject = λ cb1 iscb1 cb1eq →  ?} where
+                ; cb-inject = λ cb1 c1<fa b1 eq → lem06 (suc i) cb1 c c1<fa isb b1 eq } where
               lem11 : suc i ≡ toℕ (F←Q fa (f (Is.a isb)))
               lem11 = begin
                 suc i ≡⟨ sym ( toℕ-fromℕ< c) ⟩