The rewrite relation of the following TRS is considered.
U11(tt,M,N) | → | U12(tt,activate(M),activate(N)) | (1) |
U12(tt,M,N) | → | s(plus(activate(N),activate(M))) | (2) |
U21(tt,M,N) | → | U22(tt,activate(M),activate(N)) | (3) |
U22(tt,M,N) | → | plus(x(activate(N),activate(M)),activate(N)) | (4) |
plus(N,0) | → | N | (5) |
plus(N,s(M)) | → | U11(tt,M,N) | (6) |
x(N,0) | → | 0 | (7) |
x(N,s(M)) | → | U21(tt,M,N) | (8) |
activate(X) | → | X | (9) |
prec(U11) | = | 2 | stat(U11) | = | mul | |
prec(tt) | = | 0 | stat(tt) | = | mul | |
prec(U12) | = | 2 | stat(U12) | = | mul | |
prec(s) | = | 1 | stat(s) | = | mul | |
prec(plus) | = | 2 | stat(plus) | = | mul | |
prec(U21) | = | 3 | stat(U21) | = | mul | |
prec(U22) | = | 3 | stat(U22) | = | mul | |
prec(x) | = | 3 | stat(x) | = | mul | |
prec(0) | = | 0 | stat(0) | = | mul |
π(U11) | = | [1,2,3] |
π(tt) | = | [] |
π(U12) | = | [1,2,3] |
π(activate) | = | 1 |
π(s) | = | [1] |
π(plus) | = | [1,2] |
π(U21) | = | [1,2,3] |
π(U22) | = | [1,2,3] |
π(x) | = | [1,2] |
π(0) | = | [] |
U12(tt,M,N) | → | s(plus(activate(N),activate(M))) | (2) |
U22(tt,M,N) | → | plus(x(activate(N),activate(M)),activate(N)) | (4) |
plus(N,0) | → | N | (5) |
plus(N,s(M)) | → | U11(tt,M,N) | (6) |
x(N,0) | → | 0 | (7) |
x(N,s(M)) | → | U21(tt,M,N) | (8) |
prec(tt) | = | 0 | weight(tt) | = | 1 | ||||
prec(activate) | = | 3 | weight(activate) | = | 1 | ||||
prec(U11) | = | 2 | weight(U11) | = | 2 | ||||
prec(U12) | = | 1 | weight(U12) | = | 0 | ||||
prec(U21) | = | 5 | weight(U21) | = | 2 | ||||
prec(U22) | = | 4 | weight(U22) | = | 0 |
U11(tt,M,N) | → | U12(tt,activate(M),activate(N)) | (1) |
U21(tt,M,N) | → | U22(tt,activate(M),activate(N)) | (3) |
activate(X) | → | X | (9) |
There are no rules in the TRS. Hence, it is terminating.