equal
deleted
inserted
replaced
8 |
8 |
9 Automata = DA + NAe + |
9 Automata = DA + NAe + |
10 |
10 |
11 constdefs |
11 constdefs |
12 na2da :: ('a,'s)na => ('a,'s set)da |
12 na2da :: ('a,'s)na => ('a,'s set)da |
13 "na2da A == ({start A}, %a Q. Union(next A a `` Q), %Q. ? q:Q. fin A q)" |
13 "na2da A == ({start A}, %a Q. Union(next A a ` Q), %Q. ? q:Q. fin A q)" |
14 |
14 |
15 nae2da :: ('a,'s)nae => ('a,'s set)da |
15 nae2da :: ('a,'s)nae => ('a,'s set)da |
16 "nae2da A == ({start A}, |
16 "nae2da A == ({start A}, |
17 %a Q. Union(next A (Some a) `` ((eps A)^* ``` Q)), |
17 %a Q. Union(next A (Some a) ` ((eps A)^* `` Q)), |
18 %Q. ? p: (eps A)^* ``` Q. fin A p)" |
18 %Q. ? p: (eps A)^* `` Q. fin A p)" |
19 |
19 |
20 end |
20 end |