Theorem 7.   

Grail

echo '0*+0*1(11)*(0+100+101)(00+01+10+11)*' | retofm | fmdeterm | fmmin | fmcomp | fmrenum > ov1

produces the output automaton ov1 as follows:

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

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

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

The Walnut command is

eval over "~(E x,y (n=x+y)&(OV[x]=@1)&(OV[y]=@1))":

The output log is

eval over "~(E x,y (n=x+y)&(OV[x]=@1)&(OV[y]=@1))":
n=(x+y):2 states - 17ms
 OV[x]=@1:5 states - 4ms
   (n=(x+y)&OV[x]=@1):10 states - 7ms
      OV[y]=@1:5 states - 2ms
          ((n=(x+y)&OV[x]=@1)&OV[y]=@1):34 states - 14ms
	       (E x , y ((n=(x+y)&OV[x]=@1)&OV[y]=@1)):8 states - 7ms
	             ~(E x , y ((n=(x+y)&OV[x]=@1)&OV[y]=@1)):7 states - 0ms
		     total computation time: 61ms

and the output automaton is

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