--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/nfa.agda	Mon Nov 05 08:59:31 2018 +0900
@@ -0,0 +1,113 @@
+module nfa where
+
+-- open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat
+open import Data.List
+open import Data.Fin
+open import Data.Maybe
+open import Data.Bool using ( Bool ; true ; false ; _∧_ )
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
+data  States1   : Set  where
+   sr : States1
+   ss : States1
+   st : States1
+
+data  In2   : Set  where
+   i0 : In2
+   i1 : In2
+
+
+record NAutomaton ( Q : Set ) ( Σ : Set  )
+       : Set  where
+    field
+          Nδ : Q → Σ → Q → Bool
+          Nstart : Q → Bool
+          Nend  :  Q → Bool
+
+open NAutomaton
+
+Nmoves1 : { Q : Set } { Σ : Set  }
+    → NAutomaton Q  Σ
+    →  ∀ {q : Q} → ( (q : Q ) → Bool )  → Σ → Q → Bool
+Nmoves1 {Q} { Σ} M {q'} Qs  s q  = (Qs q') ∧ ( Nδ M q' s q ) 
+
+record FiniteSet ( Q : Set ) ( n : ℕ )
+        : Set  where
+     field
+        fin : Fin n
+        Q←F : {n : ℕ } → Fin n → Q
+        F←Q : {n : ℕ } → Q → Fin n 
+        finiso→ : {n : ℕ } → (q : Q) → Q←F {n} ( F←Q q ) ≡ q
+        finiso← : {n : ℕ } → (f : Fin n ) → F←Q ( Q←F f ) ≡ f
+     exists : ( Q → Bool ) → Bool
+     exists p = exists1 fin p where
+         exists1 : {n : ℕ } → (f : Fin n ) → ( Q → Bool ) → Bool
+         exists1 ( Fin.zero ) _ = false
+         exists1 ( Fin.suc f ) p = p (Q←F f) ∧ exists1 f p
+
+finState1 : FiniteSet States1 3
+finState1 = record {
+        fin = fromℕ 2
+      ; Q←F = {!!}
+      ; F←Q  = {!!}
+      ; finiso→ = {!!}
+      ; finiso← = {!!}
+   } where
+       Q←F : {n : ℕ } → Fin n → States1
+       Q←F zero = sr
+       Q←F (suc zero) = ss
+       Q←F (suc (suc zero)) = st
+       Q←F (suc (suc (suc _)))  = {!!}
+       F←Q : {n : ℕ } → States1 → Fin n
+       F←Q = {!!}
+
+open FiniteSet
+
+Nmoves : { Q : Set } { Σ : Set  }
+    → NAutomaton Q  Σ
+    → {n : ℕ } → FiniteSet Q n
+    →  ( Q → Bool )  → Σ → Q → Bool
+Nmoves {Q} { Σ} M fin  Qs  s q  =
+      FiniteSet.exists fin ( λ qn → (Qs q ∧ ( Nδ M q s qn )  ))
+
+
+Naccept : { Q : Set } { Σ : Set  } 
+    → NAutomaton Q  Σ
+    → {n : ℕ } → FiniteSet Q n
+    → List  Σ  → Q → Bool
+Naccept M fin [] = Nend M 
+Naccept {Q} {Σ} M fin (s ∷ tail ) = exists1 M ( Nstart M ) s tail 
+   where
+      exists1 : NAutomaton Q  Σ → ( Q → Bool ) →  Σ → List  Σ  → Q → Bool
+      exists1 M sb s [] = Nend M
+      exists1 M sb s (i ∷ t ) = exists1 M ( Nmoves M  fin sb s ) i t
+
+
+transition3 : States1  → In2  → States1 → Bool
+transition3 sr i0 sr = true
+transition3 sr i1 ss = true
+transition3 sr i1 sr = true
+transition3 ss i0 sr = true
+transition3 ss i1 sr = true
+transition3 st i0 sr = true
+transition3 st i1 sr = true
+transition3 _ _ _ = false
+
+fin1 :  States1  → Bool
+fin1 st = true
+fin1 ss = false
+fin1 sr = false
+
+start1 : States1 → Bool
+start1 sr = true
+start1 _ = true
+
+am2  :  NAutomaton  States1 In2
+am2  =  record { Nδ = transition3 ; Nstart = start1 ; Nend = fin1}
+
+example2-1 = Naccept am2 finState1 ( i0  ∷ i1  ∷ i0  ∷ [] )
+example2-2 = Naccept am2 finState1 ( i1  ∷ i1  ∷ i1  ∷ [] )
+
+