# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1541409213 -32400
# Node ID a9471b42573e1d5675ed1b4815a38b4d77f798da
# Parent  2887577a3d6332f1ab126a4c4d2620c69083e93a
...

diff -r 2887577a3d63 -r a9471b42573e agda/nfa.agda
--- a/agda/nfa.agda	Mon Nov 05 16:41:25 2018 +0900
+++ b/agda/nfa.agda	Mon Nov 05 18:13:33 2018 +0900
@@ -7,7 +7,7 @@
 open import Data.Maybe
 open import Relation.Nullary
 open import Data.Empty
-open import Data.Bool using ( Bool ; true ; false ; _∧_ )
+open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
@@ -38,16 +38,22 @@
 record FiniteSet ( Q : Set ) { n : ℕ }
         : Set  where
      field
-        fin : Fin n
         Q←F : Fin n → Q
         F←Q : Q → Fin n 
         finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
         finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ 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 fin fin p where
-         exists1 : {m : ℕ} → Fin m → Fin n → ( Q → Bool ) → Bool
-         exists1 ( zero ) _ _ = false
-         exists1 ( suc f ) fn p = p (Q←F (Data.Fin.pred fn) ) ∧ exists1 f (Data.Fin.pred fn) p
+     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 (fromℕ≤ {m} {n} m<n)) ∨ exists1 m (lt2 m<n) p
 
 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
 fless zero = s≤s z≤n
@@ -55,8 +61,7 @@
 
 finState1 : FiniteSet States1 
 finState1 = record {
-        fin = fromℕ 2
-      ; Q←F = Q←F
+        Q←F = Q←F
       ; F←Q  = F←Q
       ; finiso→ = finiso→
       ; finiso← = finiso←
@@ -88,19 +93,18 @@
     → {n : ℕ } → FiniteSet Q  {n}
     →  ( Q → Bool )  → Σ → Q → Bool
 Nmoves {Q} { Σ} M fin  Qs  s q  =
-      FiniteSet.exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q )  ))
+      exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q )  ))
 
 
 Naccept : { Q : Set } { Σ : Set  } 
     → NAutomaton Q  Σ
     → {n : ℕ } → FiniteSet Q {n}
-    → List  Σ  → Q → Bool
-Naccept M fin [] = Nend M 
-Naccept {Q} {Σ} M fin (s ∷ tail ) = Naccept1 M ( Nstart M ) s tail 
+    → List  Σ  → Bool
+Naccept {Q} {Σ} M fin input = Naccept1 M ( Nstart M ) input
    where
-      Naccept1 : NAutomaton Q  Σ → ( Q → Bool ) →  Σ → List  Σ  → Q → Bool
-      Naccept1 M sb s [] q = sb q ∧ Nend M q
-      Naccept1 M sb s (i ∷ t ) = Naccept1 M ( Nmoves M  fin sb s ) i t
+      Naccept1 : NAutomaton Q  Σ → ( Q → Bool ) →  List  Σ  →  Bool
+      Naccept1 M sb []  = exists fin ( λ q → sb q ∧ Nend M q )
+      Naccept1 M sb (i ∷ t ) = Naccept1 M ( Nmoves M  fin sb i ) t
 
 
 transition3 : States1  → In2  → States1 → Bool
@@ -125,7 +129,16 @@
 am2  :  NAutomaton  States1 In2
 am2  =  record { Nδ = transition3 ; Nstart = start1 ; Nend = fin1}
 
-example2-1 = Naccept am2 finState1 ( i0  ∷ i1  ∷ i0  ∷ [] ) sr
-example2-2 = Naccept am2 finState1 ( i1  ∷ i1  ∷ i1  ∷ [] ) sr
+example2-1 = Naccept am2 finState1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
+example2-2 = Naccept am2 finState1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
 
+fin0 :  States1  → Bool
+fin0 st = false
+fin0 ss = false
+fin0 sr = false
 
+test1 : Bool
+test1 = exists finState1 fin1
+
+test0 : Bool
+test0 = exists finState1 fin0