--- a/agda/nfa136.agda	Sat Mar 14 19:42:27 2020 +0900
+++ b/agda/nfa136.agda	Sun Dec 27 13:26:44 2020 +0900
@@ -2,7 +2,7 @@
 
 open import logic
 open import nfa
-open import automaton hiding ( StatesQ )
+open import automaton 
 open import Data.List
 open import finiteSet
 open import Data.Fin
@@ -59,35 +59,55 @@
 start136 q1 = true
 start136 _ = false
 
+exists136 : (StatesQ → Bool) → Bool
+exists136 f = f q1 \/ f q2 \/ f q3
+
+to-list-136 : (StatesQ → Bool) → List StatesQ
+to-list-136 f = tl1 where
+   tl3 : List StatesQ 
+   tl3 with f q3
+   ... | true = q3 ∷  []
+   ... | false = []
+   tl2 : List StatesQ 
+   tl2 with f q2
+   ... | true = q2 ∷ tl3 
+   ... | false = tl3
+   tl1 : List StatesQ 
+   tl1 with f q1
+   ... | true = q1 ∷ tl2
+   ... | false = tl2
+
 nfa136 :  NAutomaton  StatesQ A2
 nfa136 =  record { Nδ = transition136; Nend = end136 }
 
-example136-1 = Naccept nfa136 finStateQ start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )
+example136-1 = Naccept nfa136 exists136 start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )
+
+t146-1 = Ntrace nfa136 exists136 to-list-136 start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )
 
-example136-0 = Naccept nfa136 finStateQ start136( a0 ∷ [] )
+example136-0 = Naccept nfa136 exists136 start136( a0 ∷ [] )
 
-example136-2 = Naccept nfa136 finStateQ start136( b0  ∷ a0  ∷ b0 ∷ a0 ∷ b0 ∷ [] )
+example136-2 = Naccept nfa136 exists136 start136( b0  ∷ a0  ∷ b0 ∷ a0 ∷ b0 ∷ [] )
+t146-2 = Ntrace nfa136 exists136 to-list-136 start136( b0  ∷ a0  ∷ b0 ∷ a0 ∷ b0 ∷ [] )
 
 open FiniteSet
 
 nx : (StatesQ → Bool) → (List A2 ) → StatesQ → Bool
 nx now [] = now
-nx now ( i ∷ ni ) = (Nmoves nfa136 finStateQ (nx now ni) i )
+nx now ( i ∷ ni ) = (Nmoves nfa136 exists136 (nx now ni) i )
 
-example136-3 = to-list finStateQ start136
-example136-4 = to-list finStateQ (nx start136  ( a0  ∷ b0 ∷ a0 ∷ [] ))
+example136-3 = to-list-136 start136
+example136-4 = to-list-136 (nx start136  ( a0  ∷ b0 ∷ a0 ∷ [] ))
 
 open import sbconst2
 
 fm136 : Automaton ( StatesQ → Bool  )  A2
--- fm136  = record { δ = λ qs q → transition136 {!!} {!!}  ; aend = λ qs → exists finStateQ end136 }
-fm136  = subset-construction finStateQ nfa136 q1
+fm136  = subset-construction exists136 nfa136 
 
 open NAutomaton
 
-lemma136 : ( x : List A2 ) → Naccept nfa136 finStateQ start136 x  ≡ accept fm136 start136 x 
+lemma136 : ( x : List A2 ) → Naccept nfa136 exists136 start136 x  ≡ accept fm136 start136 x 
 lemma136 x = lemma136-1 x start136 where
     lemma136-1 : ( x : List A2 ) → ( states : StatesQ → Bool )
-        → Naccept nfa136 finStateQ states x  ≡ accept fm136 states x 
+        → Naccept nfa136 exists136 states x  ≡ accept fm136 states x 
     lemma136-1 [] _ = refl
-    lemma136-1 (h ∷ t) states = lemma136-1 t (δconv finStateQ (Nδ nfa136) states h)
+    lemma136-1 (h ∷ t) states = lemma136-1 t (δconv exists136 (Nδ nfa136) states h)