Theorem 12.   

Grail 3.0

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

produces the output automaton gt1 as follows:

(START) |- 0
0 0 0
0 1 1
1 0 2
1 1 3
7 0 6
7 1 3
5 0 5
5 1 6
2 0 4
2 1 1
6 0 5
6 1 7
4 0 5
4 1 2
3 0 3
3 1 3
0 -| (FINAL)
4 -| (FINAL)
5 -| (FINAL)
6 -| (FINAL)

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

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

The Walnut command is

eval grt "E x,y,z (n=x+y+z)&(GT[x]=@1)&(GT[y]=@1)&(GT[z]=@1)":

The output log is

n=((x+y)+z):3 states - 6ms
 GT[x]=@1:7 states - 1ms
   (n=((x+y)+z)&GT[x]=@1):21 states - 7ms
      GT[y]=@1:7 states - 1ms
          ((n=((x+y)+z)&GT[x]=@1)&GT[y]=@1):131 states - 17ms
	       GT[z]=@1:7 states - 0ms
	             (((n=((x+y)+z)&GT[x]=@1)&GT[y]=@1)&GT[z]=@1):746 states - 72ms
		            (E x , y , z (((n=((x+y)+z)&GT[x]=@1)&GT[y]=@1)&GT[z]=@1)):13 states - 1822ms
			    total computation time: 1956ms

and the output automaton is

msd_2
0 1
0 -> 0
1 -> 1
1 0
0 -> 2
1 -> 3
2 0
0 -> 4
1 -> 5
3 0
0 -> 6
1 -> 5
4 1
0 -> 7
1 -> 8
5 0
0 -> 9
1 -> 6
6 0
0 -> 7
1 -> 10
7 1
0 -> 7
1 -> 7
8 0
0 -> 7
1 -> 11
9 0
0 -> 7
1 -> 7
10 0
0 -> 7
1 -> 9
11 0
0 -> 7
1 -> 12
12 1
0 -> 7
1 -> 9