--- a/agda/sbconst2.agda	Sat Mar 14 19:42:27 2020 +0900
+++ b/agda/sbconst2.agda	Sun Dec 27 13:26:44 2020 +0900
@@ -10,52 +10,46 @@
 open import logic
 open NAutomaton
 open Automaton
-open import finiteSet
-open FiniteSet
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
-
 open Bool
 
-δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool)
-δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → f r /\ nδ r i q )
-
-open FiniteSet
+δconv : { Q : Set } { Σ : Set  } → ( ( Q → Bool ) → Bool ) →  ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool)
+δconv {Q} { Σ} exists nδ f i q =  exists ( λ r → f r /\ nδ r i q )
 
-subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  
-    (NAutomaton Q  Σ ) → (astart : Q ) → (Automaton (Q → Bool)  Σ )  
-subset-construction {Q} { Σ} {n} fin NFA astart = record {
-        δ = λ q x → δconv fin ( Nδ NFA ) q x
-     ;  aend = λ f → exists fin ( λ q → f q /\ Nend NFA q )
+subset-construction : { Q : Set } { Σ : Set  } → 
+    ( ( Q → Bool ) → Bool ) →
+    (NAutomaton Q  Σ ) → (Automaton (Q → Bool)  Σ )  
+subset-construction {Q} { Σ}  exists NFA = record {
+        δ = λ q x → δconv exists ( Nδ NFA ) q x
+     ;  aend = λ f → exists ( λ q → f q /\ Nend NFA q )
    } 
 
-am2start = λ q1 → equal? finState1 ss q1
+test4 = subset-construction existsS1 am2 
 
-test4 = subset-construction finState1 am2 ss
-
-test5 = accept test4 ( λ q1 → equal? finState1 ss q1) ( i0  ∷ i1  ∷ i0  ∷ [] )
-test6 = accept test4 ( λ q1 → equal? finState1 ss q1) ( i1  ∷ i1  ∷ i1  ∷ [] )
+test51 = accept test4 start1 ( i0  ∷ i1  ∷ i0  ∷ [] )
+test61 = accept test4 start1 ( i1  ∷ i1  ∷ i1  ∷ [] )
 
-subset-construction-lemma→ : { Q : Set } { Σ : Set  } { n  : ℕ }  → (fin : FiniteSet Q {n} ) →  
-    (NFA : NAutomaton Q  Σ ) → (astart : Q )
+subset-construction-lemma→ : { Q : Set } { Σ : Set  } { n  : ℕ }  → (exists : ( Q → Bool ) → Bool ) →
+    (NFA : NAutomaton Q  Σ ) → (astart : Q → Bool ) 
     → (x : List Σ)
-    → Naccept NFA fin ( λ q1 → equal? fin  astart q1) x ≡ true
-    → accept (  subset-construction fin NFA astart ) ( λ q1 → equal? fin  astart q1) x ≡ true
-subset-construction-lemma→ {Q} {Σ} {n} fin NFA astart x naccept = lemma1 x ( λ q1 → equal? fin  astart q1) naccept where
+    → Naccept NFA exists astart  x ≡ true
+    → accept (  subset-construction exists NFA ) astart  x ≡ true
+subset-construction-lemma→ {Q} {Σ} {n} exists NFA astart x naccept = lemma1 x astart naccept where
     lemma1 :  (x : List Σ) → ( states : Q → Bool )
-       → Naccept NFA fin states x ≡ true
-       → accept (  subset-construction fin NFA astart ) states x ≡ true
+       → Naccept NFA exists states x ≡ true
+       → accept (  subset-construction exists NFA ) states x ≡ true
     lemma1 [] states naccept = naccept
-    lemma1 (h ∷ t ) states naccept = lemma1 t (δconv fin (Nδ NFA) states h) naccept
+    lemma1 (h ∷ t ) states naccept = lemma1 t (δconv exists (Nδ NFA) states h) naccept
 
-subset-construction-lemma← : { Q : Set } { Σ : Set  } { n  : ℕ }  → (fin : FiniteSet Q {n} ) →  
-    (NFA : NAutomaton Q  Σ ) → (astart : Q )
+subset-construction-lemma← : { Q : Set } { Σ : Set  } { n  : ℕ }  → (exists : ( Q → Bool ) → Bool ) →
+    (NFA : NAutomaton Q  Σ ) → (astart : Q → Bool )
     → (x : List Σ)
-    → accept (  subset-construction fin NFA astart ) ( λ q1 → equal? fin  astart q1) x ≡ true
-    → Naccept NFA fin ( λ q1 → equal? fin  astart q1) x ≡ true
-subset-construction-lemma← {Q} {Σ} {n} fin NFA astart x saccept = lemma2 x ( λ q1 → equal? fin  astart q1) saccept where
+    → accept (  subset-construction exists NFA ) astart x ≡ true
+    → Naccept NFA exists astart x ≡ true
+subset-construction-lemma← {Q} {Σ} {n} exists NFA astart x saccept = lemma2 x astart saccept where
     lemma2 :  (x : List Σ) → ( states : Q → Bool )
-       → accept (  subset-construction fin NFA astart ) states x ≡ true
-       → Naccept NFA fin states x ≡ true
+       → accept (  subset-construction exists NFA ) states x ≡ true
+       → Naccept NFA exists states x ≡ true
     lemma2 [] states saccept = saccept
-    lemma2 (h ∷ t ) states saccept = lemma2 t (δconv fin (Nδ NFA) states h) saccept
+    lemma2 (h ∷ t ) states saccept = lemma2 t (δconv exists (Nδ NFA) states h) saccept