Mercurial > hg > Members > kono > Proof > automaton

changeset 44:aa15eff1aeb3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
seprate finite
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Dec 2018 11:45:37 +0900
parents 31e4bd173951
children e9edc777dc03
files agda/derive.agda agda/finiteSet.agda agda/nfa-list.agda agda/nfa.agda agda/regex1.agda agda/sbconst1.agda agda/sbconst2.agda
diffstat 7 files changed, 168 insertions(+), 210 deletions(-) [+]
line wrap: on
line diff
--- a/agda/derive.agda	Sat Dec 22 03:08:21 2018 +0900
+++ b/agda/derive.agda	Sat Dec 22 11:45:37 2018 +0900
@@ -2,11 +2,130 @@
 
 open import nfa
 open import regex1
-open import Data.Nat
-open import Data.List
+open import Data.Nat hiding ( _<_ ; _>_ )
+open import Data.Fin hiding ( _<_ )
+open import Data.List hiding ( [_] )
 
 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
-open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
+open import finiteSet
+
+finIn2 : FiniteSet In2
+finIn2 = record {
+        Q←F = Q←F'
+      ; F←Q  = F←Q'
+      ; finiso→ = finiso→'
+      ; finiso← = finiso←'
+   } where
+       Q←F' : Fin 2 → In2
+       Q←F' zero = i0
+       Q←F' (suc zero) = i1
+       Q←F' (suc (suc ())) 
+       F←Q' : In2 → Fin 2
+       F←Q' i0 = zero
+       F←Q' i1 = suc (zero)
+       finiso→' : (q : In2) → Q←F' (F←Q' q) ≡ q
+       finiso→' i0 = refl
+       finiso→' i1 = refl
+       finiso←' : (f : Fin 2) → F←Q' (Q←F' f) ≡ f
+       finiso←' zero = refl
+       finiso←' (suc zero) = refl
+       finiso←' (suc (suc ()))
+
+
+test-r1 = < i0 > & < i1 >
+test-r2 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i1  ∷ [] )
+test-r3 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i0  ∷ [] )
+
+issub : {Σ : Set} {n : ℕ } → Regex Σ → Regex Σ → FiniteSet Σ {n} → Bool
+issub (r *) s f = issub r s f
+issub (r & r₁) s f = issub r s f ∨ issub r₁ s f
+issub (r || r₁) s f =  issub r s f ∨ issub r₁ s f
+issub < x > < s > f with cmpi f x s 
+issub < x > < s > f | yes p = true
+issub < x > < s > f | no ¬p = false
+issub < x > s f  = false
+
+record RegexSub {Σ : Set} (R :  Regex Σ) {n : ℕ }  (fin :  FiniteSet Σ {n} ): Set where
+    field
+       Subterm : Regex Σ
+       sub     : issub R Subterm fin ≡ true
+
+open import Data.Product
+
+
+regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ × ( List (Regex Σ) ) 
+regex2nfa {Σ} (r *) fin =  record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!}  where
+          nr0 =  proj₁ (regex2nfa r fin)
+          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
+          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ (  NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr0 s0 i s1)
+          Nstart : (Regex Σ) → Bool
+          Nstart s0 = NAutomaton.Nstart nr0 s0
+          Nend : (Regex Σ) → Bool
+          Nend s0 =  NAutomaton.Nend nr0 s0
+regex2nfa {Σ} (r0 & r1) fin =  record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
+          nr0 =  proj₁ (regex2nfa r0 fin)
+          nr1 =  proj₁ (regex2nfa r1 fin)
+          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
+          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧  NAutomaton.Nδ nr1 s0 i s1 )
+          Nstart : (Regex Σ) → Bool
+          Nstart s0 = NAutomaton.Nstart nr0 s0  ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nstart nr1 s0 )
+          Nend : (Regex Σ) → Bool
+          Nend s0 = NAutomaton.Nend nr0 s0  ∨ (  NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nend nr1 s0 )
+regex2nfa {Σ} (r0 || r1) fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
+          nr0 =  proj₁ (regex2nfa r0 fin)
+          nr1 =  proj₁ (regex2nfa r1 fin)
+          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
+          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ NAutomaton.Nδ nr1 s0 i s1
+          Nstart : (Regex Σ) → Bool
+          Nstart s0 = NAutomaton.Nstart nr0 s0  ∨ NAutomaton.Nstart nr1 s0 
+          Nend : (Regex Σ) → Bool
+          Nend s0 = NAutomaton.Nend nr0 s0  ∨ NAutomaton.Nend nr1 s0 
+regex2nfa {Σ} < x > fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
+          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
+          Nδ r1 s r2 with cmpi fin s x
+          Nδ r1 s r2 | yes _ = true
+          Nδ r1 s r2 | no _ = false
+          Nstart : (Regex Σ) → Bool
+          Nstart = {!!}
+          Nstart < s > with cmpi fin s x
+          ... | yes _ = true
+          ... | no  _ = false
+          Nstart _ = false
+          Nend  :  (Regex Σ) → Bool
+          Nend  _ = false
+
+test-r4 = regex2nfa  (< i0 > & < i1 >) finIn2 
+
+testr5 = Naccept ( proj₁ test-r4) {!!} ( i0  ∷ i1  ∷ [] )
+
+rfin : {Σ : Set} → (s : List ( Regex Σ)) → FiniteSet (Regex Σ ) {length s } 
+rfin {Σ} s = record {
+        Q←F = Q←F'
+      ; F←Q  = F←Q'
+      ; finiso→ = finiso→'
+      ; finiso← = finiso←'
+  } where
+        Q←F' : Fin (length s) → Regex Σ
+        Q←F' = {!!}
+        F←Q'  : Regex Σ → Fin (length s)
+        F←Q'  = {!!}
+        finiso→' : (q : Regex Σ) → Q←F' (F←Q' q) ≡ q
+        finiso→' = {!!}
+        finiso←' : (f : Fin (length s)) → F←Q' (Q←F' f) ≡ f
+        finiso←' = {!!}
+
+reglang⇔n=regex2nfa : {Σ : Set} → {n m : ℕ } (fin : FiniteSet Σ {n}) 
+     → ( regex : Regex Σ )
+     → ( In : List Σ )
+     → regular-language regex fin  In  ≡ Naccept {Regex Σ} {_} (  proj₁ ( regex2nfa {Σ} regex  fin  ))
+         (rfin (proj₂  ( regex2nfa {Σ} regex  fin  ) )) In
+reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex *) In = {!!}
+reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex & regex₁) In = {!!}
+reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex || regex₁) In = {!!}
+reglang⇔n=regex2nfa {Σ} {n} {m} fin < x > In = {!!}
 
 
 derivatives : {Σ : Set} → Σ → Regex  Σ → Regex  Σ
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/finiteSet.agda	Sat Dec 22 11:45:37 2018 +0900
@@ -0,0 +1,30 @@
+module finiteSet  where
+
+open import Data.Nat
+open import Data.Bool
+open import Data.Fin renaming ( _<_ to _<<_ )
+open import Relation.Binary.Core
+
+record FiniteSet ( Q : Set ) { n : ℕ }
+        : Set  where
+     field
+        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 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
+fless (suc f) = s≤s ( fless f )
--- a/agda/nfa-list.agda	Sat Dec 22 03:08:21 2018 +0900
+++ b/agda/nfa-list.agda	Sat Dec 22 11:45:37 2018 +0900
@@ -8,7 +8,6 @@
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
-
 data  States1   : Set  where
    sr : States1
    ss : States1
--- a/agda/nfa.agda	Sat Dec 22 03:08:21 2018 +0900
+++ b/agda/nfa.agda	Sat Dec 22 11:45:37 2018 +0900
@@ -10,7 +10,7 @@
 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
-
+open import finiteSet
 
 data  States1   : Set  where
    sr : States1
@@ -31,30 +31,6 @@
 
 open NAutomaton
 
-record FiniteSet ( Q : Set ) { n : ℕ }
-        : Set  where
-     field
-        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 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
-fless (suc f) = s≤s ( fless f )
-
 finState1 : FiniteSet States1 
 finState1 = record {
         Q←F = Q←F
@@ -151,6 +127,7 @@
 inputnn : { n :  ℕ }  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ
 inputnn {zero} {_} _ _ s = s
 inputnn {suc n} x y s = x  ∷ ( inputnn {n} x y ( y  ∷ s ) )                                                                                                         
+
 -- lemmaNN :  { Q : Set } { Σ : Set  } → ( x y : Σ ) → (M : NAutomaton Q  Σ)
 --     → ( n :  ℕ )  → (fin :  FiniteSet Q  {n} ) 
 --     →  Naccept M fin ( inputnn {n} x y [] )  ≡ true  
--- a/agda/regex1.agda	Sat Dec 22 03:08:21 2018 +0900
+++ b/agda/regex1.agda	Sat Dec 22 11:45:37 2018 +0900
@@ -1,9 +1,10 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module regex1 where
 
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Data.Fin
 open import Data.Nat hiding ( _≟_ )
-open import Data.List hiding ( any )
+open import Data.List hiding ( any ;  [_] )
 import Data.Bool using ( Bool ; true ; false ; _∧_ )
 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
 open import  Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) 
@@ -47,6 +48,7 @@
 repeat x [] = true
 repeat {Σ} x ( h  ∷ t ) = split x (repeat {Σ} x) ( h  ∷ t )
 
+open import finiteSet
 open FiniteSet
 
 cmpi :  {Σ : Set} → {n : ℕ } (fin : FiniteSet Σ {n}) → (x y : Σ ) → Dec (F←Q fin x ≡  F←Q fin y) 
@@ -62,126 +64,3 @@
 ... | no _  = false
 regular-language < h > f _ = false
 
-finIn2 : FiniteSet In2
-finIn2 = record {
-        Q←F = Q←F'
-      ; F←Q  = F←Q'
-      ; finiso→ = finiso→'
-      ; finiso← = finiso←'
-   } where
-       Q←F' : Fin 2 → In2
-       Q←F' zero = i0
-       Q←F' (suc zero) = i1
-       Q←F' (suc (suc ())) 
-       F←Q' : In2 → Fin 2
-       F←Q' i0 = zero
-       F←Q' i1 = suc (zero)
-       finiso→' : (q : In2) → Q←F' (F←Q' q) ≡ q
-       finiso→' i0 = refl
-       finiso→' i1 = refl
-       finiso←' : (f : Fin 2) → F←Q' (Q←F' f) ≡ f
-       finiso←' zero = refl
-       finiso←' (suc zero) = refl
-       finiso←' (suc (suc ()))
-
-
-test-r1 = < i0 > & < i1 >
-test-r2 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i1  ∷ [] )
-test-r3 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i0  ∷ [] )
-
-issub : {Σ : Set} {n : ℕ } → Regex Σ → Regex Σ → FiniteSet Σ {n} → Bool
-issub (r *) s f = issub r s f
-issub (r & r₁) s f = issub r s f ∨ issub r₁ s f
-issub (r || r₁) s f =  issub r s f ∨ issub r₁ s f
-issub < x > < s > f with cmpi f x s 
-issub < x > < s > f | yes p = true
-issub < x > < s > f | no ¬p = false
-issub < x > s f  = false
-
-record RegexSub {Σ : Set} (R :  Regex Σ) {n : ℕ }  (fin :  FiniteSet Σ {n} ): Set where
-    field
-       Subterm : Regex Σ
-       sub     : issub R Subterm fin ≡ true
-
-open import Data.Product
-
-
-regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ × ( List (Regex Σ) ) 
-regex2nfa {Σ} (r *) fin =  record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!}  where
-          nr0 =  proj₁ (regex2nfa r fin)
-          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
-          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ (  NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr0 s0 i s1)
-          Nstart : (Regex Σ) → Bool
-          Nstart s0 = NAutomaton.Nstart nr0 s0
-          Nend : (Regex Σ) → Bool
-          Nend s0 =  NAutomaton.Nend nr0 s0
-regex2nfa {Σ} (r0 & r1) fin =  record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
-          nr0 =  proj₁ (regex2nfa r0 fin)
-          nr1 =  proj₁ (regex2nfa r1 fin)
-          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
-          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧  NAutomaton.Nδ nr1 s0 i s1 )
-          Nstart : (Regex Σ) → Bool
-          Nstart s0 = NAutomaton.Nstart nr0 s0  ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nstart nr1 s0 )
-          Nend : (Regex Σ) → Bool
-          Nend s0 = NAutomaton.Nend nr0 s0  ∨ (  NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nend nr1 s0 )
-regex2nfa {Σ} (r0 || r1) fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
-          nr0 =  proj₁ (regex2nfa r0 fin)
-          nr1 =  proj₁ (regex2nfa r1 fin)
-          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
-          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ NAutomaton.Nδ nr1 s0 i s1
-          Nstart : (Regex Σ) → Bool
-          Nstart s0 = NAutomaton.Nstart nr0 s0  ∨ NAutomaton.Nstart nr1 s0 
-          Nend : (Regex Σ) → Bool
-          Nend s0 = NAutomaton.Nend nr0 s0  ∨ NAutomaton.Nend nr1 s0 
-regex2nfa {Σ} < x > fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
-          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
-          Nδ r1 s r2 with cmpi fin s x
-          Nδ r1 s r2 | yes _ = true
-          Nδ r1 s r2 | no _ = false
-          Nstart : (Regex Σ) → Bool
-          Nstart < s > with cmpi fin s x
-          ... | yes _ = true
-          ... | no  _ = false
-          Nstart _ = false
-          Nend  :  (Regex Σ) → Bool
-          Nend  _ = false
-
-test-r4 = regex2nfa  (< i0 > & < i1 >) finIn2 
-
--- testr5 = Naccept test-r4 {!!} ( i0  ∷ i1  ∷ [] )
-
-rfin : {Σ : Set} → (s : List ( Regex Σ)) → FiniteSet (Regex Σ ) {length s } 
-rfin {Σ} s = record {
-        Q←F = Q←F'
-      ; F←Q  = F←Q'
-      ; finiso→ = finiso→'
-      ; finiso← = finiso←'
-  } where
-        Q←F' : Fin (length s) → Regex Σ
-        Q←F' = {!!}
-        F←Q'  : Regex Σ → Fin (length s)
-        F←Q'  = {!!}
-        finiso→' : (q : Regex Σ) → Q←F' (F←Q' q) ≡ q
-        finiso→' = {!!}
-        finiso←' : (f : Fin (length s)) → F←Q' (Q←F' f) ≡ f
-        finiso←' = {!!}
-
-reglang⇔n=regex2nfa : {Σ : Set} → {n m : ℕ } (fin : FiniteSet Σ {n}) 
-     → ( regex : Regex Σ )
-     → ( In : List Σ )
-     → regular-language regex fin  In  ≡ Naccept {Regex Σ} {_} (  proj₁ ( regex2nfa {Σ} regex  fin  ))
-         (rfin (proj₂  ( regex2nfa {Σ} regex  fin  ) )) In
-reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex *) In = {!!}
-reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex & regex₁) In = {!!}
-reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex || regex₁) In = {!!}
-reglang⇔n=regex2nfa {Σ} {n} {m} fin < x > In = {!!}
-
-
-
-
-
-
-
-
-
-
--- a/agda/sbconst1.agda	Sat Dec 22 03:08:21 2018 +0900
+++ b/agda/sbconst1.agda	Sat Dec 22 11:45:37 2018 +0900
@@ -1,56 +1,34 @@
 module sbconst1 where
 
 open import Level renaming ( suc to succ ; zero to Zero )
-open import Data.Nat
+open import Data.Nat hiding ( _≟_ )
+open import Data.Fin
 open import Data.List
 open import Data.Maybe
-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)
 open import Data.Product
--- open import Data.Nat.DivMod
--- open import Data.Fin  using ( toℕ )
-
+open import finiteSet
 
 open import automaton
 open import nfa-list
 open Automaton
 open NAutomaton
 
-record FiniteSet ( Q : Set ) ( max : ℕ  )
-        : Set  where
-     field
-        not-zero : max > 0
-        ←ℕ : ℕ → Q
-        ←Q : Q → ℕ 
-        finite : (q : Q) → ←Q q < max
-        finiso→ :(q : Q) → ←ℕ ( ←Q q ) ≡ q
-        finiso← :(n : ℕ) → ←Q ( ←ℕ n ) ≡ n
-     fmax : ℕ
-     fmax = max
-
 open FiniteSet
 
-exists : { Q : Set} {n  : ℕ } → FiniteSet Q n → ( Q → Bool ) → Bool
-exists {Q} {n} N f = exists1 (fmax N)
-  where
-     exists1 :  ℕ → Bool
-     exists1 zero = false
-     exists1 (suc i) with f (←ℕ N i ) 
-     ... | true = true
-     ... | false = exists1 i
-
-list2sbst : {Q : Set} { n :  ℕ } → FiniteSet Q n → List Q → Q → Bool
+list2sbst : {Q : Set} { n :  ℕ } → FiniteSet Q {n} → List Q → Q → Bool
 list2sbst N [] _ = false
-list2sbst N ( h ∷ t ) q with  ←Q N q  ≟ ←Q N h 
+list2sbst N ( h ∷ t ) q with  F←Q N q  ≟ F←Q N h 
 ... | yes _ = true
 ... | no _ = list2sbst N t q
 
 
-δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q n →  ( nδ : Q → Σ → List Q ) → (Q → Bool) → Σ → (Q → Bool)
-δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → list2sbst N (nδ r i) q )
+δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  ( nδ : Q → Σ → List Q ) → (Q → Bool) → Σ → (Q → Bool)
+δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → f r ∧ list2sbst N (nδ r i) q )
 
-subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q n →  
+subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  
     (NAutomaton Q  Σ ) → (Automaton (Q → Bool)  Σ )  
 subset-construction {Q} { Σ} {n} N NFA = record {
         δ = λ q x → δconv N ( nδ NFA ) q x
@@ -62,28 +40,3 @@
      aend1 : (Q → Bool) → Bool
      aend1 f = exists N f
 
--- _div_ : ℕ → ℕ → Maybe ℕ
--- _div_ x zero = {!!}
--- _div_ x (suc y) = {!!}
--- 
--- _mod_ : ℕ → ℕ → Maybe ℕ
--- _mod_ = {!!}
--- 
--- lemma1 : { Q R : Set} {n m : ℕ } → FiniteSet Q n → FiniteSet R m → FiniteSet (Q × R) ( n * m )
--- lemma1 {Q} {R} {zero} {_} N M  = {!!}
--- lemma1 {Q} {R} {n} {zero} N M  = {!!}
--- lemma1 {Q} {R} {n} {m} N M = record {
---         not-zero = {!!}
---      ;  ←ℕ = λ i → ( ←ℕ N {!!} ,  ←ℕ M {!!})
---      ;  ←Q =  λ q → ( ←Q N ( proj₁ q ) * ( ←Q M (proj₂ q )))
---      ;  finite = {!!}
---      ;  finiso→ = {!!}
---      ;  finiso← = {!!}
---    }
--- 
--- _exp_ : ℕ → ℕ → ℕ
--- _exp_ = {!!}
--- 
--- sbstFin : { Q : Set} {n  : ℕ } → FiniteSet Q n → FiniteSet (Q → Bool) ( 2 exp n )
--- sbstFin = {!!}
--- 
--- a/agda/sbconst2.agda	Sat Dec 22 03:08:21 2018 +0900
+++ b/agda/sbconst2.agda	Sat Dec 22 11:45:37 2018 +0900
@@ -9,10 +9,11 @@
 open import nfa
 open NAutomaton
 open Automaton
+open import finiteSet
 open FiniteSet
 
 δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  ( nδ : Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool)
-δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → nδ r i q )
+δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → f r ∧ nδ r i q )
 
 subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  
     (NAutomaton Q  Σ ) → (Automaton (Q → Bool)  Σ )