--- a/automaton-in-agda/src/finiteSetUtil.agda	Tue Jan 25 09:11:01 2022 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Wed Nov 16 17:43:10 2022 +0900
@@ -103,7 +103,7 @@
 
 iso-fin : {A B : Set} → FiniteSet A  → Bijection A B → FiniteSet B 
 iso-fin {A} {B}  fin iso = record {
-   Q←F = λ f → fun→ iso ( FiniteSet.Q←F fin f )
+       Q←F = λ f → fun→ iso ( FiniteSet.Q←F fin f )
      ; F←Q = λ b → FiniteSet.F←Q fin (fun← iso b )
      ; finiso→ = finiso→ 
      ; finiso← = finiso← 
@@ -131,10 +131,10 @@
 
 fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B) 
 fin-∨1 {B} fb =  record {
-   Q←F = Q←F
- ; F←Q =  F←Q
- ; finiso→ = finiso→
- ; finiso← = finiso←
+       Q←F = Q←F
+     ; F←Q =  F←Q
+     ; finiso→ = finiso→
+     ; finiso← = finiso←
    }  where
    b = FiniteSet.finite fb
    Q←F : Fin (suc b) → One ∨ B
@@ -502,6 +502,14 @@
 -- there is a duplicate element in finite list
 --
 
+--
+-- How about this?
+--      get list of Q
+--      remove one element for each Q from list
+--      there must be remaining list > 1
+--      theses are duplicates
+--      actualy it is duplicate
+
 phase2 : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
 phase2 finq q [] = false
 phase2 finq q (x ∷ qs) with equal? finq q x