Theorem 9.   

Grail 3.0

echo '0*+0*1(1+10+01)*' | retofm | fmdeterm | fmmin | fmcomp | fmrenum > lt1

produces the output automaton lt1 as follows:

(START) |- 0
1 0 2
1 1 3
2 0 4
2 1 1
3 0 1
3 1 3
0 0 0
0 1 1
4 0 4
4 1 4
0 -| (FINAL)
1 -| (FINAL)
3 -| (FINAL)

This corresponds to the LT.txt file for Walnut as follows:

msd_2
0 1
0 -> 0
1 -> 1
1 1
0 -> 2
1 -> 3
2 0
0 -> 4
1 -> 1
3 1
0 -> 1
1 -> 3
4 0
0 -> 4
1 -> 4

The Walnut command is

eval lt "E x,y (n=x+y)&(LT[x]=@1)&(LT[y]=@1)":

The output log is

n=(x+y):2 states - 19ms
 LT[x]=@1:4 states - 4ms
   (n=(x+y)&LT[x]=@1):8 states - 5ms
      LT[y]=@1:4 states - 2ms
          ((n=(x+y)&LT[x]=@1)&LT[y]=@1):29 states - 11ms
	       (E x , y ((n=(x+y)&LT[x]=@1)&LT[y]=@1)):1 states - 8ms
	       total computation time: 59ms

and the output automaton is

msd_2
0 1
0 -> 0
1 -> 0