The TRS could be proven terminating. The proof took 832 ms.
Problem 1 was processed with processor DependencyGraph (82ms). | – Problem 2 was processed with processor PolynomialLinearRange4 (191ms). | | – Problem 3 was processed with processor PolynomialLinearRange4 (146ms). | | | – Problem 4 was processed with processor PolynomialLinearRange4 (62ms).
| T(zWadr(x_1, x_2)) | → | T(x_2) | T(app(x_1, x_2)) | → | T(x_1) | |
| T(zWadr(L, prefix(L))) | → | zWadr#(L, prefix(L)) | T(from(x_1)) | → | T(x_1) | |
| T(zWadr(x_1, x_2)) | → | T(x_1) | zWadr#(cons(X, XS), cons(Y, YS)) | → | app#(Y, cons(X, nil)) | |
| T(app(XS, YS)) | → | app#(XS, YS) | T(zWadr(XS, YS)) | → | zWadr#(XS, YS) | |
| T(s(x_1)) | → | T(x_1) | T(prefix(x_1)) | → | T(x_1) | |
| T(prefix(L)) | → | prefix#(L) | T(from(s(X))) | → | from#(s(X)) | |
| T(app(x_1, x_2)) | → | T(x_2) |
| app(nil, YS) | → | YS | app(cons(X, XS), YS) | → | cons(X, app(XS, YS)) | |
| from(X) | → | cons(X, from(s(X))) | zWadr(nil, YS) | → | nil | |
| zWadr(XS, nil) | → | nil | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) | |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons
Context-sensitive strategy:
μ(T) = μ(nil) = ∅
μ(from#) = μ(s) = μ(prefix) = μ(prefix#) = μ(from) = μ(cons) = {1}
μ(app) = μ(app#) = μ(zWadr) = μ(zWadr#) = {1, 2}
| T(zWadr(x_1, x_2)) → T(x_2) | T(app(x_1, x_2)) → T(x_1) |
| T(s(x_1)) → T(x_1) | T(from(x_1)) → T(x_1) |
| T(prefix(x_1)) → T(x_1) | T(zWadr(x_1, x_2)) → T(x_1) |
| T(app(x_1, x_2)) → T(x_2) |
| T(zWadr(x_1, x_2)) | → | T(x_2) | T(app(x_1, x_2)) | → | T(x_1) | |
| T(s(x_1)) | → | T(x_1) | T(from(x_1)) | → | T(x_1) | |
| T(prefix(x_1)) | → | T(x_1) | T(zWadr(x_1, x_2)) | → | T(x_1) | |
| T(app(x_1, x_2)) | → | T(x_2) |
| app(nil, YS) | → | YS | app(cons(X, XS), YS) | → | cons(X, app(XS, YS)) | |
| from(X) | → | cons(X, from(s(X))) | zWadr(nil, YS) | → | nil | |
| zWadr(XS, nil) | → | nil | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) | |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons
Context-sensitive strategy:
μ(T) = μ(nil) = ∅
μ(s) = μ(from#) = μ(prefix) = μ(from) = μ(prefix#) = μ(cons) = {1}
μ(app) = μ(zWadr) = μ(app#) = μ(zWadr#) = {1, 2}
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(app(x_1, x_2)) | → | T(x_1) | T(from(x_1)) | → | T(x_1) | |
| T(prefix(x_1)) | → | T(x_1) | T(app(x_1, x_2)) | → | T(x_2) |
| T(zWadr(x_1, x_2)) | → | T(x_2) | T(s(x_1)) | → | T(x_1) | |
| T(zWadr(x_1, x_2)) | → | T(x_1) |
| app(nil, YS) | → | YS | app(cons(X, XS), YS) | → | cons(X, app(XS, YS)) | |
| from(X) | → | cons(X, from(s(X))) | zWadr(nil, YS) | → | nil | |
| zWadr(XS, nil) | → | nil | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) | |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, cons, nil
Context-sensitive strategy:
μ(T) = μ(nil) = ∅
μ(from#) = μ(s) = μ(prefix) = μ(prefix#) = μ(from) = μ(cons) = {1}
μ(app) = μ(app#) = μ(zWadr) = μ(zWadr#) = {1, 2}
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(s(x_1)) | → | T(x_1) |
| T(zWadr(x_1, x_2)) | → | T(x_2) | T(zWadr(x_1, x_2)) | → | T(x_1) |
| app(nil, YS) | → | YS | app(cons(X, XS), YS) | → | cons(X, app(XS, YS)) | |
| from(X) | → | cons(X, from(s(X))) | zWadr(nil, YS) | → | nil | |
| zWadr(XS, nil) | → | nil | zWadr(cons(X, XS), cons(Y, YS)) | → | cons(app(Y, cons(X, nil)), zWadr(XS, YS)) | |
| prefix(L) | → | cons(nil, zWadr(L, prefix(L))) |
Termination of terms over the following signature is verified: app, zWadr, s, prefix, from, nil, cons
Context-sensitive strategy:
μ(T) = μ(nil) = ∅
μ(s) = μ(from#) = μ(prefix) = μ(from) = μ(prefix#) = μ(cons) = {1}
μ(app) = μ(zWadr) = μ(app#) = μ(zWadr#) = {1, 2}
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(zWadr(x_1, x_2)) | → | T(x_2) | T(zWadr(x_1, x_2)) | → | T(x_1) |