# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1541409759 -32400
# Node ID 9b00dc130ede6b35566bff56c9febf001c3bb642
# Parent  a9471b42573e1d5675ed1b4815a38b4d77f798da
nfa using subset mapping done

diff -r a9471b42573e -r 9b00dc130ede agda/nfa.agda
--- a/agda/nfa.agda	Mon Nov 05 18:13:33 2018 +0900
+++ b/agda/nfa.agda	Mon Nov 05 18:22:39 2018 +0900
@@ -112,9 +112,9 @@
 transition3 sr i1 ss = true
 transition3 sr i1 sr = true
 transition3 ss i0 sr = true
-transition3 ss i1 sr = true
+transition3 ss i1 st = true
 transition3 st i0 sr = true
-transition3 st i1 sr = true
+transition3 st i1 st = true
 transition3 _ _ _ = false
 
 fin1 :  States1  → Bool
@@ -137,8 +137,11 @@
 fin0 ss = false
 fin0 sr = false
 
+test0 : Bool
+test0 = exists finState1 fin0
+
 test1 : Bool
 test1 = exists finState1 fin1
 
-test0 : Bool
-test0 = exists finState1 fin0
+test2 = Nmoves am2 finState1 start1 
+