Theorem 15. We start with the automaton (START) |- 0 0 0 0 0 1 1 1 0 2 1 1 3 2 0 5 2 1 1 3 0 1 3 1 4 4 0 3 4 1 5 5 0 5 5 1 5 0 -| (FINAL) 2 -| (FINAL) This corresponds to the TB.txt file for Walnut as follows: msd_2 0 1 0 -> 0 1 -> 1 1 0 0 -> 2 1 -> 3 2 1 0 -> 5 1 -> 1 3 0 0 -> 1 1 -> 4 4 0 0 -> 3 1 -> 5 5 0 0 -> 5 1 -> 5 The Walnut command is eval bp2 "E x,y,z (2*n=x+y+z)&(TB[x]=@1)&(TB[y]=@1)&(TB[z]=@1)": The output log is eval bp2 "E x,y,z (2*n=x+y+z)&(TB[x]=@1)&(TB[y]=@1)&(TB[z]=@1)": (2*n)=((x+y)+z):4 states - 12ms TB[x]=@1:5 states - 1ms ((2*n)=((x+y)+z)&TB[x]=@1):20 states - 7ms TB[y]=@1:5 states - 1ms (((2*n)=((x+y)+z)&TB[x]=@1)&TB[y]=@1):62 states - 17ms TB[z]=@1:5 states - 1ms ((((2*n)=((x+y)+z)&TB[x]=@1)&TB[y]=@1)&TB[z]=@1):147 states - 29ms (E x , y , z ((((2*n)=((x+y)+z)&TB[x]=@1)&TB[y]=@1)&TB[z]=@1)):11 states - 78ms total computation time: 192ms and the output automaton is msd_2 0 1 0 -> 0 1 -> 1 1 1 0 -> 2 1 -> 3 2 1 0 -> 4 1 -> 5 3 1 0 -> 6 1 -> 7 4 0 0 -> 6 1 -> 8 5 1 0 -> 9 1 -> 6 6 1 0 -> 6 1 -> 6 7 1 0 -> 10 1 -> 6 8 0 0 -> 6 1 -> 10 9 1 0 -> 4 1 -> 6 10 0 0 -> 6 1 -> 6