The TRS could not be proven terminating. The proof attempt took 60011 ms.
Problem 1 was processed with processor ReductionPairSAT (9322ms). | – Problem 2 remains open; application of the following processors failed [DependencyGraph (426ms), ReductionPairSAT (8264ms)].
| a__from#(X) | → | mark#(X) | mark#(from(X)) | → | a__from#(mark(X)) | |
| mark#(quot(X1, X2)) | → | mark#(X2) | a__sel#(s(N), cons(X, XS)) | → | mark#(N) | |
| mark#(quot(X1, X2)) | → | a__quot#(mark(X1), mark(X2)) | a__quot#(s(X), s(Y)) | → | mark#(Y) | |
| mark#(minus(X1, X2)) | → | mark#(X1) | a__minus#(s(X), s(Y)) | → | a__minus#(mark(X), mark(Y)) | |
| mark#(zWquot(X1, X2)) | → | mark#(X1) | mark#(zWquot(X1, X2)) | → | mark#(X2) | |
| mark#(sel(X1, X2)) | → | mark#(X2) | mark#(s(X)) | → | mark#(X) | |
| mark#(sel(X1, X2)) | → | mark#(X1) | mark#(minus(X1, X2)) | → | mark#(X2) | |
| mark#(from(X)) | → | mark#(X) | mark#(cons(X1, X2)) | → | mark#(X1) | |
| a__zWquot#(cons(X, XS), cons(Y, YS)) | → | mark#(Y) | a__minus#(s(X), s(Y)) | → | mark#(Y) | |
| a__sel#(s(N), cons(X, XS)) | → | mark#(XS) | a__sel#(s(N), cons(X, XS)) | → | a__sel#(mark(N), mark(XS)) | |
| a__zWquot#(cons(X, XS), cons(Y, YS)) | → | a__quot#(mark(X), mark(Y)) | a__quot#(s(X), s(Y)) | → | a__minus#(mark(X), mark(Y)) | |
| a__sel#(0, cons(X, XS)) | → | mark#(X) | mark#(minus(X1, X2)) | → | a__minus#(mark(X1), mark(X2)) | |
| a__zWquot#(cons(X, XS), cons(Y, YS)) | → | mark#(X) | mark#(zWquot(X1, X2)) | → | a__zWquot#(mark(X1), mark(X2)) | |
| mark#(sel(X1, X2)) | → | a__sel#(mark(X1), mark(X2)) | a__minus#(s(X), s(Y)) | → | mark#(X) | |
| mark#(quot(X1, X2)) | → | mark#(X1) | a__quot#(s(X), s(Y)) | → | mark#(X) |
| a__from(X) | → | cons(mark(X), from(s(X))) | a__sel(0, cons(X, XS)) | → | mark(X) | |
| a__sel(s(N), cons(X, XS)) | → | a__sel(mark(N), mark(XS)) | a__minus(X, 0) | → | 0 | |
| a__minus(s(X), s(Y)) | → | a__minus(mark(X), mark(Y)) | a__quot(0, s(Y)) | → | 0 | |
| a__quot(s(X), s(Y)) | → | s(a__quot(a__minus(mark(X), mark(Y)), s(mark(Y)))) | a__zWquot(XS, nil) | → | nil | |
| a__zWquot(nil, XS) | → | nil | a__zWquot(cons(X, XS), cons(Y, YS)) | → | cons(a__quot(mark(X), mark(Y)), zWquot(XS, YS)) | |
| mark(from(X)) | → | a__from(mark(X)) | mark(sel(X1, X2)) | → | a__sel(mark(X1), mark(X2)) | |
| mark(minus(X1, X2)) | → | a__minus(mark(X1), mark(X2)) | mark(quot(X1, X2)) | → | a__quot(mark(X1), mark(X2)) | |
| mark(zWquot(X1, X2)) | → | a__zWquot(mark(X1), mark(X2)) | mark(cons(X1, X2)) | → | cons(mark(X1), X2) | |
| mark(s(X)) | → | s(mark(X)) | mark(0) | → | 0 | |
| mark(nil) | → | nil | a__from(X) | → | from(X) | |
| a__sel(X1, X2) | → | sel(X1, X2) | a__minus(X1, X2) | → | minus(X1, X2) | |
| a__quot(X1, X2) | → | quot(X1, X2) | a__zWquot(X1, X2) | → | zWquot(X1, X2) |
Termination of terms over the following signature is verified: minus, mark, from, a__minus, a__zWquot, 0, s, a__quot, zWquot, a__sel, quot, sel, a__from, nil, cons
| a__quot#(s(X), s(Y)) | → | a__quot#(a__minus(mark(X), mark(Y)), s(mark(Y))) | a__from#(X) | → | mark#(X) | |
| mark#(from(X)) | → | a__from#(mark(X)) | mark#(quot(X1, X2)) | → | mark#(X2) | |
| a__sel#(s(N), cons(X, XS)) | → | mark#(N) | mark#(quot(X1, X2)) | → | a__quot#(mark(X1), mark(X2)) | |
| a__quot#(s(X), s(Y)) | → | mark#(Y) | mark#(minus(X1, X2)) | → | mark#(X1) | |
| a__minus#(s(X), s(Y)) | → | a__minus#(mark(X), mark(Y)) | mark#(zWquot(X1, X2)) | → | mark#(X1) | |
| mark#(zWquot(X1, X2)) | → | mark#(X2) | mark#(sel(X1, X2)) | → | mark#(X2) | |
| mark#(s(X)) | → | mark#(X) | mark#(sel(X1, X2)) | → | mark#(X1) | |
| mark#(minus(X1, X2)) | → | mark#(X2) | mark#(from(X)) | → | mark#(X) | |
| mark#(cons(X1, X2)) | → | mark#(X1) | a__zWquot#(cons(X, XS), cons(Y, YS)) | → | mark#(Y) | |
| a__minus#(s(X), s(Y)) | → | mark#(Y) | a__sel#(s(N), cons(X, XS)) | → | mark#(XS) | |
| a__sel#(s(N), cons(X, XS)) | → | a__sel#(mark(N), mark(XS)) | a__zWquot#(cons(X, XS), cons(Y, YS)) | → | a__quot#(mark(X), mark(Y)) | |
| a__quot#(s(X), s(Y)) | → | a__minus#(mark(X), mark(Y)) | a__sel#(0, cons(X, XS)) | → | mark#(X) | |
| mark#(minus(X1, X2)) | → | a__minus#(mark(X1), mark(X2)) | a__zWquot#(cons(X, XS), cons(Y, YS)) | → | mark#(X) | |
| mark#(zWquot(X1, X2)) | → | a__zWquot#(mark(X1), mark(X2)) | mark#(sel(X1, X2)) | → | a__sel#(mark(X1), mark(X2)) | |
| a__minus#(s(X), s(Y)) | → | mark#(X) | mark#(quot(X1, X2)) | → | mark#(X1) | |
| a__quot#(s(X), s(Y)) | → | mark#(X) |
| a__from(X) | → | cons(mark(X), from(s(X))) | a__sel(0, cons(X, XS)) | → | mark(X) | |
| a__sel(s(N), cons(X, XS)) | → | a__sel(mark(N), mark(XS)) | a__minus(X, 0) | → | 0 | |
| a__minus(s(X), s(Y)) | → | a__minus(mark(X), mark(Y)) | a__quot(0, s(Y)) | → | 0 | |
| a__quot(s(X), s(Y)) | → | s(a__quot(a__minus(mark(X), mark(Y)), s(mark(Y)))) | a__zWquot(XS, nil) | → | nil | |
| a__zWquot(nil, XS) | → | nil | a__zWquot(cons(X, XS), cons(Y, YS)) | → | cons(a__quot(mark(X), mark(Y)), zWquot(XS, YS)) | |
| mark(from(X)) | → | a__from(mark(X)) | mark(sel(X1, X2)) | → | a__sel(mark(X1), mark(X2)) | |
| mark(minus(X1, X2)) | → | a__minus(mark(X1), mark(X2)) | mark(quot(X1, X2)) | → | a__quot(mark(X1), mark(X2)) | |
| mark(zWquot(X1, X2)) | → | a__zWquot(mark(X1), mark(X2)) | mark(cons(X1, X2)) | → | cons(mark(X1), X2) | |
| mark(s(X)) | → | s(mark(X)) | mark(0) | → | 0 | |
| mark(nil) | → | nil | a__from(X) | → | from(X) | |
| a__sel(X1, X2) | → | sel(X1, X2) | a__minus(X1, X2) | → | minus(X1, X2) | |
| a__quot(X1, X2) | → | quot(X1, X2) | a__zWquot(X1, X2) | → | zWquot(X1, X2) |
Termination of terms over the following signature is verified: minus, mark, from, a__minus, a__zWquot, 0, s, a__quot, zWquot, a__sel, quot, sel, a__from, nil, cons
a__quot#: collapses to 1
minus: all arguments are removed from minus
mark: all arguments are removed from mark
from: all arguments are removed from from
a__minus#: collapses to 1
a__zWquot: all arguments are removed from a__zWquot
mark#: all arguments are removed from mark#
a__minus: all arguments are removed from a__minus
a__sel#: all arguments are removed from a__sel#
0: all arguments are removed from 0
s: all arguments are removed from s
a__quot: collapses to 1
zWquot: all arguments are removed from zWquot
a__sel: collapses to 2
sel: collapses to 2
quot: collapses to 1
a__from: all arguments are removed from a__from
a__zWquot#: collapses to 2
a__from#: all arguments are removed from a__from#
nil: all arguments are removed from nil
cons: all arguments are removed from cons
| a__sel(s(N), cons(X, XS)) → a__sel(mark(N), mark(XS)) | a__quot(s(X), s(Y)) → s(a__quot(a__minus(mark(X), mark(Y)), s(mark(Y)))) |
| mark(cons(X1, X2)) → cons(mark(X1), X2) | a__sel(X1, X2) → sel(X1, X2) |
| a__minus(s(X), s(Y)) → a__minus(mark(X), mark(Y)) | a__from(X) → from(X) |
| mark(0) → 0 | a__zWquot(XS, nil) → nil |
| a__from(X) → cons(mark(X), from(s(X))) | a__quot(0, s(Y)) → 0 |
| a__zWquot(cons(X, XS), cons(Y, YS)) → cons(a__quot(mark(X), mark(Y)), zWquot(XS, YS)) | a__zWquot(nil, XS) → nil |
| a__zWquot(X1, X2) → zWquot(X1, X2) | a__sel(0, cons(X, XS)) → mark(X) |
| mark(s(X)) → s(mark(X)) | mark(from(X)) → a__from(mark(X)) |
| mark(quot(X1, X2)) → a__quot(mark(X1), mark(X2)) | mark(zWquot(X1, X2)) → a__zWquot(mark(X1), mark(X2)) |
| mark(nil) → nil | mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2)) |
| a__minus(X1, X2) → minus(X1, X2) | a__minus(X, 0) → 0 |
| a__quot(X1, X2) → quot(X1, X2) | mark(minus(X1, X2)) → a__minus(mark(X1), mark(X2)) |
The dependency pairs and usable rules are stronlgy conservative!
The following dependency pairs (at least) can be eliminated according to the given precedence.
| a__quot#(s(X), s(Y)) → a__quot#(a__minus(mark(X), mark(Y)), s(mark(Y))) |