Mercurial > hg > Members > kono > Proof > automaton
changeset 31:9b00dc130ede
nfa using subset mapping done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 05 Nov 2018 18:22:39 +0900 |
parents | a9471b42573e |
children | cd311109d63b |
files | agda/nfa.agda |
diffstat | 1 files changed, 7 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- 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 +