The rewrite relation of the following TRS is considered.
| din(der(plus(X,Y))) | → | u21(din(der(X)),X,Y) | (1) |
| u21(dout(DX),X,Y) | → | u22(din(der(Y)),X,Y,DX) | (2) |
| u22(dout(DY),X,Y,DX) | → | dout(plus(DX,DY)) | (3) |
| din(der(times(X,Y))) | → | u31(din(der(X)),X,Y) | (4) |
| u31(dout(DX),X,Y) | → | u32(din(der(Y)),X,Y,DX) | (5) |
| u32(dout(DY),X,Y,DX) | → | dout(plus(times(X,DY),times(Y,DX))) | (6) |
| din(der(der(X))) | → | u41(din(der(X)),X) | (7) |
| u41(dout(DX),X) | → | u42(din(der(DX)),X,DX) | (8) |
| u42(dout(DDX),X,DX) | → | dout(DDX) | (9) |
final states:
{1}
transitions:
| dout1(1) | → | 1 |
| dout1(7) | → | 1 |
| u310(1,1,1) | → | 1 |
| u320(1,1,1,1) | → | 1 |
| u211(4,1,1) | → | 1 |
| u211(4,1,1) | → | 4 |
| u211(4,1,1) | → | 18 |
| u211(4,1,7) | → | 1 |
| times0(1,1) | → | 1 |
| times1(1,7) | → | 10 |
| times1(1,1) | → | 9 |
| times1(1,1) | → | 10 |
| der1(7) | → | 13 |
| der1(1) | → | 3 |
| u421(14,1,7) | → | 1 |
| u421(4,1,1) | → | 1 |
| u311(4,1,1) | → | 1 |
| u311(4,1,1) | → | 4 |
| u311(4,1,1) | → | 18 |
| u220(1,1,1,1) | → | 1 |
| din1(3) | → | 4 |
| din1(13) | → | 14 |
| u420(1,1,1) | → | 1 |
| u210(1,1,1) | → | 1 |
| u312(18,1,7) | → | 20 |
| u312(18,1,1) | → | 20 |
| u212(18,1,1) | → | 14 |
| u212(18,1,7) | → | 4 |
| u212(18,1,7) | → | 18 |
| u212(20,10,9) | → | 14 |
| dout0(1) | → | 1 |
| plus1(10,9) | → | 7 |
| plus1(1,7) | → | 1 |
| plus1(1,1) | → | 7 |
| u411(4,1) | → | 1 |
| u411(4,1) | → | 4 |
| u411(4,1) | → | 18 |
| din0(1) | → | 1 |
| u221(4,1,1,1) | → | 1 |
| u221(4,1,1,7) | → | 1 |
| der0(1) | → | 1 |
| plus0(1,1) | → | 1 |
| din2(17) | → | 18 |
| din2(19) | → | 20 |
| der2(1) | → | 17 |
| der2(10) | → | 19 |
| u321(4,1,1,7) | → | 1 |
| u321(4,1,1,1) | → | 1 |
| u410(1,1) | → | 1 |