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