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)>[x]=@1):21 states - 7ms GT[y]=@1:7 states - 1ms ((n=((x+y)+z)>[x]=@1)>[y]=@1):131 states - 17ms GT[z]=@1:7 states - 0ms (((n=((x+y)+z)>[x]=@1)>[y]=@1)>[z]=@1):746 states - 72ms (E x , y , z (((n=((x+y)+z)>[x]=@1)>[y]=@1)>[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