--- a/agda/nfa.agda	Mon Nov 05 18:37:23 2018 +0900
+++ b/agda/nfa.agda	Mon Nov 05 21:56:44 2018 +0900
@@ -35,6 +35,36 @@
     →  ∀ {q : Q} → ( (q : Q ) → Bool )  → Σ → Q → Bool
 Nmoves1 {Q} { Σ} M {q'} Qs  s q  = (Qs q') ∧ ( Nδ M q' s q ) 
 
+Naccept2 : { Q : Set } { Σ : Set  } 
+    → NAutomaton Q  Σ
+    → List  Σ  → {q : Q} → Bool
+Naccept2 {Q} {Σ} M input {q} = Naccept3 M ( Nstart M ) input {q}
+   where
+      Naccept3 : NAutomaton Q  Σ → ( Q → Bool ) →  List  Σ  → {q : Q} →  Bool
+      Naccept3 M sb []  {q} =  sb q ∧ Nend M q
+      Naccept3 M sb (i ∷ t ) {q} = Naccept3 M ( Nmoves1 M {q} sb i ) t {q}
+
+record FiniteSet' ( Q : Set ) { n : ℕ }
+        : Set  where
+     field
+        Q←F : (m : ℕ) → m < n  → Q
+        F←Q : Q → ℕ 
+        F←Q<n :  ∀{q : Q } → F←Q q < n
+        finiso→ : (q : Q) → Q←F ( F←Q q ) F←Q<n  ≡ q
+        finiso← : (f : ℕ ) → (f<n : f < n ) → F←Q ( Q←F f f<n) ≡ f
+     lt0 : (n : ℕ) →  n Data.Nat.≤ n
+     lt0 zero = z≤n
+     lt0 (suc n) = s≤s (lt0 n)
+     lt2 : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
+     lt2 {zero} lt = z≤n
+     lt2 {suc m} {zero} ()
+     lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
+     exists : ( Q → Bool ) → Bool
+     exists p = exists1 n (lt0 n) p where
+         exists1 : (m : ℕ ) → m Data.Nat.≤ n  → ( Q → Bool ) → Bool
+         exists1  zero  _ _ = false
+         exists1 ( suc m ) m<n p = p (Q←F m m<n ) ∨ exists1 m (lt2 m<n) p
+
 record FiniteSet ( Q : Set ) { n : ℕ }
         : Set  where
      field