--- a/agda/regex.agda	Wed Aug 15 14:37:11 2018 +0900
+++ b/agda/regex.agda	Wed Aug 15 17:38:48 2018 +0900
@@ -3,6 +3,7 @@
 open import Level renaming ( suc to succ ; zero to Zero )
 -- open import Data.Fin
 open import Data.Nat
+open import Data.Product
 -- open import Data.List 
 open import Data.Maybe 
 open import Data.Bool using ( Bool ; true ; false )
@@ -30,6 +31,7 @@
    field
       state :  ℕ
       move  :  Maybe Σ → Tree (RST Σ)
+      cond  :  Maybe Σ 
       RSTend : Bool
 
 open RST
@@ -53,7 +55,7 @@
 
 infixr 5 _++_ 
 
-_++_ : { Σ : Set} → Tree (RST Σ ) → Tree (RST Σ ) → Tree (RST Σ )
+_++_ : { Q : Set} → Tree Q → Tree Q → Tree Q 
 empty ++ t = t
 leaf n e ++ t = insertT n e t
 node n e left right ++ t =
@@ -61,13 +63,13 @@
 
 generateRNFA :  { Σ : Set  } → ( Regex  Σ ) → (_≟_ : ( q q' : Σ ) → Dec ( q ≡ q' ) ) →  RNFA  Σ
 generateRNFA  {Σ} regex _≟_ = generate regex (
-      record { Rstates = [] ; Rstart = record { state = 0 ; move = λ q → [] ; RSTend = true } ;
-                                Rend = record { state = 0 ; move = λ q → [] ; RSTend = true }  ; Rnum = 1 } )
+      record { Rstates = [] ; Rstart = record { state = 0 ; move = λ q → [] ; cond = nothing ; RSTend = true } ;
+                                Rend = record { state = 0 ; move = λ q → [] ; cond = nothing ; RSTend = true }  ; Rnum = 1 } )
  where
   literal :  Maybe Σ →  Σ → ℕ → Tree (RST  Σ)
   literal nothing  q' n = []
   literal (just q)  q' n with q ≟  q'
-  ... | yes _ = [ record { state = n ; move = λ i → empty ; RSTend = true  } ]
+  ... | yes _ = [ record { state = n ; move = λ i → empty ; cond = nothing ; RSTend = true  } ]
   ... | no _ = []
   generate : ( Regex  Σ ) →  RNFA Σ → RNFA Σ 
   generate (x *) R = record R' { Rstart =  record (Rstart R') { move = move0  }   ;
@@ -94,7 +96,7 @@
        R1 :  RNFA  Σ 
        R1 = generate x (  record R { Rnum = Rnum R + 1 } )
        S1 : RST Σ
-       S1 = record { state = Rnum R ; RSTend = RSTend (Rend R) ; move  = λ q → [] }
+       S1 = record { state = Rnum R ; RSTend = RSTend (Rend R) ; move  = λ q → [] ; cond = nothing }
        R2 :  RNFA  Σ
        R2 = generate y ( record R1 { Rstart = S1 ; Rend = S1  } )
        move0 : Maybe Σ → Tree (RST  Σ)
@@ -108,6 +110,7 @@
        Rstart = record {
                state  = Rnum R
              ; move = λ q → literal q x ( state (Rstart R) )
+             ; cond = just x
              ; RSTend = false
             } ;
        Rstates =  [ Rstart R ] ++ Rstates R 
@@ -116,6 +119,7 @@
 regex2nfa :  (regex : Regex In2 ) → εAutomaton (RST In2) In2 
 regex2nfa regex = record {
       εδ =  move 
+    ; all-εδ =  cond1
     ; εid = λ s → state s
     ; allState = Rstates G
     ; εstart =   Rstart G
@@ -123,4 +127,14 @@
       where
           G : RNFA In2
           G =  generateRNFA regex ieq
+          GTree :  Tree ( Tree (RST In2) ) 
+          GTree = εclosure (Rstates G) move 
+          cond2 : Maybe (Tree (RST In2) )  → Tree (Maybe In2 × Tree (RST In2))
+          cond2 nothing =  empty
+          cond2 (just empty) = empty
+          cond2 (just (leaf n r)) = leaf n (  cond r , move r ( cond r ) )
+          cond2 (just (node n r left  right )) = cond2 (just left ) ++ leaf n (  cond r , move r ( cond r ) ) ++  cond2 (just right )
+          cond1 : RST In2 → Tree (Maybe In2 × Tree (RST In2))
+          cond1 s = cond2 ( memberT ( state s ) GTree ) 
 
+