Theorem 2.   

Grail 3.0

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

produces the output automaton ge1 as follows:

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

This corresponds to the GE.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 -> 1
3 0
0 -> 3
1 -> 3
4 1
0 -> 4
1 -> 5
5 1
0 -> 4
1 -> 3

The Walnut command is

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

The output is

eval geq "E x,y,z (n=x+y+z)&(GE[x]=@1)&(GE[y]=@1)&(GE[z]=@1)":
n=((x+y)+z):3 states - 10ms
 GE[x]=@1:5 states - 1ms
   (n=((x+y)+z)&GE[x]=@1):15 states - 5ms
      GE[y]=@1:5 states - 1ms
          ((n=((x+y)+z)&GE[x]=@1)&GE[y]=@1):54 states - 15ms
	       GE[z]=@1:5 states - 1ms
	             (((n=((x+y)+z)&GE[x]=@1)&GE[y]=@1)&GE[z]=@1):230 states - 36ms
		            (E x , y , z (((n=((x+y)+z)&GE[x]=@1)&GE[y]=@1)&GE[z]=@1)):6 states - 65ms
			    total computation time: 176ms

and the output is

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