--- a/agda/regex.agda	Wed Aug 15 04:51:04 2018 +0900
+++ b/agda/regex.agda	Wed Aug 15 11:25:46 2018 +0900
@@ -40,7 +40,7 @@
       Rstart :   RST Σ
       Rend :   RST Σ
       Rnum :  ℕ
-
+   
 open RNFA
 
 mergeℕ :  List ℕ → List ℕ → List ℕ
@@ -72,30 +72,40 @@
        move1 : Maybe Σ → List ℕ
        move1 nothing = mergeℕ (move (Rstart R') nothing) (  state (Rend R')  ∷ state (Rend R')  ∷ [] ) 
        move1 (just x) =  move (Rstart R') (just x )
-  generate (x & y) R = record R1 { Rstart =  Rstart R1 ; Rend = Rend R2 ;
+  generate (x & y) R = record R1 { Rend = Rend R2 ;
                                    Rstates = Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 }
     where
        R2 : RNFA Σ 
        R2 = generate y R
        R1 : RNFA Σ 
-       R1 = generate x ( record R2 {  Rnum = Rnum R2 + 1 ; Rend = Rstart R2 ; Rstart = record { state = Rnum R2  ; RSTend = false ; move = {!!} } } )
+       R1 = generate x ( record R2 {  Rstart = record (Rstart R1) { move = move0  } ; Rend = record (Rend R1) { move = move1 } } )
        move0 : Maybe Σ → List ℕ
-       move0 nothing = mergeℕ (move (Rstart R2) nothing) [ state (Rend R2) ]
-       move0 (just x) =  {!!}
+       move0 nothing = mergeℕ (move (Rstart R1) nothing) [ state (Rstart R2) ]
+       move0 (just x) =  move (Rstart R1) (just x )
+       move1 : Maybe Σ → List ℕ
+       move1 nothing = mergeℕ (move (Rend R1) nothing) [ state (Rend R2) ]
+       move1 (just x) =  move (Rend R1) (just x )
   generate (x || y) R =  record R1 { Rstart =  Rstart R1 ; Rend = Rend R2 ;
                                    Rstates = [ Rstart R1 ] ++ Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 ++ [ Rend R2 ] }
     where
-       R1 = generate x ( record R  {  Rnum = Rnum R  + 1 ; Rend = Rstart R  ; Rstart = record { state = Rnum R   ; RSTend = false ; move = {!!} } } )
-       R2 = generate y ( record R2 {  Rnum = Rnum R2 + 1 ; Rend = Rstart R2 ; Rstart = record { state = Rnum R2  ; RSTend = false ; move = {!!} } } )
+       S1 : RST Σ
+       S1 = record { state = Rnum R ; RSTend = RSTend R ; move  = λ q → [] }
+       R1 = generate x (  record R { Rnum = Rnum R +1 } )
+       R2 = generate y ( record R1 { Rstart = S1 ; Rend = S1  } )
+       move0 : Maybe Σ → List ℕ
+       move0 nothing = mergeℕ (move (Rstart R1) nothing) [ state (Rstart R2) ]
+       move0 (just x) =  move (Rstart R1) (just x )
+       move1 : Maybe Σ → List ℕ
+       move1 nothing = mergeℕ (move (Rend R1) nothing) [ state (Rend R2) ]
+       move1 (just x) =  move (Rend R1) (just x )
   generate < x > R = record R {
        Rnum = Rnum R + 1 ;
-       Rstates = Rstates R ++ (
-            record {
+       Rstart = record {
                state  = Rnum R
              ; move = λ q → listcase q x ( state (Rstart R) )
              ; RSTend = false
-            }   ∷  [] ) }
-
+            }
+       Rstates =  Rstart R  ∷  Rstate R }
 
 regex2nfa :  (regex : Regex In2 ) → εAutomaton (RST In2) In2 
 regex2nfa regex = record {