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