TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60008 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (4904ms).
 | – Problem 2 was processed with processor ReductionPairSAT (17453ms).
 |    | – Problem 15 remains open; application of the following processors failed [DependencyGraph (661ms), ReductionPairSAT (timeout)].
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 10 was processed with processor ReductionPairSAT (94ms).
 |    |    | – Problem 16 was processed with processor ReductionPairSAT (51ms).
 | – Problem 4 was processed with processor SubtermCriterion (3ms).
 |    | – Problem 11 was processed with processor ReductionPairSAT (93ms).
 |    |    | – Problem 17 was processed with processor ReductionPairSAT (70ms).
 | – Problem 5 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 12 was processed with processor ReductionPairSAT (49ms).
 |    |    | – Problem 18 was processed with processor ReductionPairSAT (28ms).
 | – Problem 6 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 13 was processed with processor ReductionPairSAT (125ms).
 |    |    | – Problem 19 was processed with processor ReductionPairSAT (68ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 8 was processed with processor SubtermCriterion (1ms).
 | – Problem 9 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 14 was processed with processor ReductionPairSAT (57ms).
 |    |    | – Problem 20 was processed with processor ReductionPairSAT (31ms).

The following open problems remain:

Open Dependency Pair Problem 15

Dependency Pairs

mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))mark#(quot(X1, X2)) → mark#(X2)
mark#(minus(X1, X2)) → active#(minus(mark(X1), mark(X2)))active#(quot(0, s(Y))) → mark#(0)
mark#(minus(X1, X2)) → mark#(X1)mark#(zWquot(X1, X2)) → mark#(X1)
mark#(zWquot(X1, X2)) → mark#(X2)mark#(quot(X1, X2)) → active#(quot(mark(X1), mark(X2)))
mark#(sel(X1, X2)) → mark#(X2)mark#(s(X)) → mark#(X)
active#(sel(0, cons(X, XS))) → mark#(X)mark#(sel(X1, X2)) → mark#(X1)
active#(minus(s(X), s(Y))) → mark#(minus(X, Y))mark#(0) → active#(0)
mark#(minus(X1, X2)) → mark#(X2)mark#(s(X)) → active#(s(mark(X)))
mark#(from(X)) → mark#(X)mark#(cons(X1, X2)) → mark#(X1)
active#(minus(X, 0)) → mark#(0)active#(from(X)) → mark#(cons(X, from(s(X))))
mark#(sel(X1, X2)) → active#(sel(mark(X1), mark(X2)))active#(zWquot(nil, XS)) → mark#(nil)
active#(quot(s(X), s(Y))) → mark#(s(quot(minus(X, Y), s(Y))))active#(zWquot(XS, nil)) → mark#(nil)
mark#(from(X)) → active#(from(mark(X)))mark#(zWquot(X1, X2)) → active#(zWquot(mark(X1), mark(X2)))
active#(zWquot(cons(X, XS), cons(Y, YS))) → mark#(cons(quot(X, Y), zWquot(XS, YS)))active#(sel(s(N), cons(X, XS))) → mark#(sel(N, XS))
mark#(quot(X1, X2)) → mark#(X1)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))mark#(quot(X1, X2)) → quot#(mark(X1), mark(X2))
active#(quot(s(X), s(Y))) → quot#(minus(X, Y), s(Y))minus#(X1, mark(X2)) → minus#(X1, X2)
active#(quot(0, s(Y))) → mark#(0)mark#(minus(X1, X2)) → mark#(X1)
active#(zWquot(cons(X, XS), cons(Y, YS))) → cons#(quot(X, Y), zWquot(XS, YS))mark#(zWquot(X1, X2)) → mark#(X1)
mark#(s(X)) → s#(mark(X))minus#(X1, active(X2)) → minus#(X1, X2)
mark#(s(X)) → mark#(X)mark#(sel(X1, X2)) → mark#(X1)
active#(minus(s(X), s(Y))) → mark#(minus(X, Y))quot#(active(X1), X2) → quot#(X1, X2)
mark#(sel(X1, X2)) → sel#(mark(X1), mark(X2))zWquot#(mark(X1), X2) → zWquot#(X1, X2)
mark#(from(X)) → mark#(X)mark#(cons(X1, X2)) → mark#(X1)
zWquot#(X1, mark(X2)) → zWquot#(X1, X2)mark#(minus(X1, X2)) → minus#(mark(X1), mark(X2))
active#(minus(X, 0)) → mark#(0)active#(quot(s(X), s(Y))) → s#(Y)
mark#(sel(X1, X2)) → active#(sel(mark(X1), mark(X2)))active#(from(X)) → mark#(cons(X, from(s(X))))
sel#(X1, mark(X2)) → sel#(X1, X2)active#(zWquot(nil, XS)) → mark#(nil)
active#(quot(s(X), s(Y))) → mark#(s(quot(minus(X, Y), s(Y))))active#(quot(s(X), s(Y))) → s#(quot(minus(X, Y), s(Y)))
quot#(X1, mark(X2)) → quot#(X1, X2)sel#(active(X1), X2) → sel#(X1, X2)
active#(from(X)) → s#(X)cons#(X1, active(X2)) → cons#(X1, X2)
mark#(from(X)) → from#(mark(X))active#(minus(s(X), s(Y))) → minus#(X, Y)
sel#(X1, active(X2)) → sel#(X1, X2)active#(zWquot(XS, nil)) → mark#(nil)
mark#(from(X)) → active#(from(mark(X)))active#(zWquot(cons(X, XS), cons(Y, YS))) → quot#(X, Y)
active#(zWquot(cons(X, XS), cons(Y, YS))) → mark#(cons(quot(X, Y), zWquot(XS, YS)))from#(active(X)) → from#(X)
active#(sel(s(N), cons(X, XS))) → mark#(sel(N, XS))mark#(quot(X1, X2)) → mark#(X1)
minus#(active(X1), X2) → minus#(X1, X2)sel#(mark(X1), X2) → sel#(X1, X2)
mark#(quot(X1, X2)) → mark#(X2)mark#(minus(X1, X2)) → active#(minus(mark(X1), mark(X2)))
cons#(mark(X1), X2) → cons#(X1, X2)active#(zWquot(cons(X, XS), cons(Y, YS))) → zWquot#(XS, YS)
quot#(mark(X1), X2) → quot#(X1, X2)from#(mark(X)) → from#(X)
mark#(zWquot(X1, X2)) → mark#(X2)mark#(quot(X1, X2)) → active#(quot(mark(X1), mark(X2)))
minus#(mark(X1), X2) → minus#(X1, X2)mark#(nil) → active#(nil)
mark#(sel(X1, X2)) → mark#(X2)active#(sel(s(N), cons(X, XS))) → sel#(N, XS)
active#(quot(s(X), s(Y))) → minus#(X, Y)active#(from(X)) → cons#(X, from(s(X)))
active#(sel(0, cons(X, XS))) → mark#(X)cons#(X1, mark(X2)) → cons#(X1, X2)
mark#(cons(X1, X2)) → cons#(mark(X1), X2)mark#(minus(X1, X2)) → mark#(X2)
mark#(0) → active#(0)mark#(s(X)) → active#(s(mark(X)))
zWquot#(active(X1), X2) → zWquot#(X1, X2)cons#(active(X1), X2) → cons#(X1, X2)
s#(mark(X)) → s#(X)zWquot#(X1, active(X2)) → zWquot#(X1, X2)
mark#(zWquot(X1, X2)) → active#(zWquot(mark(X1), mark(X2)))mark#(zWquot(X1, X2)) → zWquot#(mark(X1), mark(X2))
s#(active(X)) → s#(X)quot#(X1, active(X2)) → quot#(X1, X2)
active#(from(X)) → from#(s(X))

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

The following SCCs where found

from#(active(X)) → from#(X)from#(mark(X)) → from#(X)
minus#(X1, active(X2)) → minus#(X1, X2)minus#(mark(X1), X2) → minus#(X1, X2)
minus#(X1, mark(X2)) → minus#(X1, X2)minus#(active(X1), X2) → minus#(X1, X2)
zWquot#(X1, active(X2)) → zWquot#(X1, X2)zWquot#(mark(X1), X2) → zWquot#(X1, X2)
zWquot#(X1, mark(X2)) → zWquot#(X1, X2)zWquot#(active(X1), X2) → zWquot#(X1, X2)
quot#(X1, active(X2)) → quot#(X1, X2)quot#(mark(X1), X2) → quot#(X1, X2)
quot#(active(X1), X2) → quot#(X1, X2)quot#(X1, mark(X2)) → quot#(X1, X2)
cons#(X1, active(X2)) → cons#(X1, X2)cons#(mark(X1), X2) → cons#(X1, X2)
cons#(X1, mark(X2)) → cons#(X1, X2)cons#(active(X1), X2) → cons#(X1, X2)
s#(mark(X)) → s#(X)s#(active(X)) → s#(X)
sel#(mark(X1), X2) → sel#(X1, X2)sel#(active(X1), X2) → sel#(X1, X2)
sel#(X1, active(X2)) → sel#(X1, X2)sel#(X1, mark(X2)) → sel#(X1, X2)
mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))mark#(quot(X1, X2)) → mark#(X2)
mark#(minus(X1, X2)) → active#(minus(mark(X1), mark(X2)))active#(quot(0, s(Y))) → mark#(0)
mark#(minus(X1, X2)) → mark#(X1)mark#(zWquot(X1, X2)) → mark#(X1)
mark#(zWquot(X1, X2)) → mark#(X2)mark#(quot(X1, X2)) → active#(quot(mark(X1), mark(X2)))
mark#(nil) → active#(nil)mark#(sel(X1, X2)) → mark#(X2)
mark#(s(X)) → mark#(X)active#(sel(0, cons(X, XS))) → mark#(X)
mark#(sel(X1, X2)) → mark#(X1)active#(minus(s(X), s(Y))) → mark#(minus(X, Y))
mark#(minus(X1, X2)) → mark#(X2)mark#(0) → active#(0)
mark#(s(X)) → active#(s(mark(X)))mark#(from(X)) → mark#(X)
mark#(cons(X1, X2)) → mark#(X1)active#(minus(X, 0)) → mark#(0)
mark#(sel(X1, X2)) → active#(sel(mark(X1), mark(X2)))active#(from(X)) → mark#(cons(X, from(s(X))))
active#(zWquot(nil, XS)) → mark#(nil)active#(quot(s(X), s(Y))) → mark#(s(quot(minus(X, Y), s(Y))))
active#(zWquot(XS, nil)) → mark#(nil)mark#(from(X)) → active#(from(mark(X)))
mark#(zWquot(X1, X2)) → active#(zWquot(mark(X1), mark(X2)))active#(zWquot(cons(X, XS), cons(Y, YS))) → mark#(cons(quot(X, Y), zWquot(XS, YS)))
active#(sel(s(N), cons(X, XS))) → mark#(sel(N, XS))mark#(quot(X1, X2)) → mark#(X1)

Problem 2: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))mark#(quot(X1, X2)) → mark#(X2)
mark#(minus(X1, X2)) → active#(minus(mark(X1), mark(X2)))active#(quot(0, s(Y))) → mark#(0)
mark#(minus(X1, X2)) → mark#(X1)mark#(zWquot(X1, X2)) → mark#(X1)
mark#(zWquot(X1, X2)) → mark#(X2)mark#(quot(X1, X2)) → active#(quot(mark(X1), mark(X2)))
mark#(nil) → active#(nil)mark#(sel(X1, X2)) → mark#(X2)
mark#(s(X)) → mark#(X)active#(sel(0, cons(X, XS))) → mark#(X)
mark#(sel(X1, X2)) → mark#(X1)active#(minus(s(X), s(Y))) → mark#(minus(X, Y))
mark#(0) → active#(0)mark#(minus(X1, X2)) → mark#(X2)
mark#(s(X)) → active#(s(mark(X)))mark#(from(X)) → mark#(X)
mark#(cons(X1, X2)) → mark#(X1)active#(minus(X, 0)) → mark#(0)
active#(from(X)) → mark#(cons(X, from(s(X))))mark#(sel(X1, X2)) → active#(sel(mark(X1), mark(X2)))
active#(zWquot(nil, XS)) → mark#(nil)active#(quot(s(X), s(Y))) → mark#(s(quot(minus(X, Y), s(Y))))
active#(zWquot(XS, nil)) → mark#(nil)mark#(from(X)) → active#(from(mark(X)))
mark#(zWquot(X1, X2)) → active#(zWquot(mark(X1), mark(X2)))active#(zWquot(cons(X, XS), cons(Y, YS))) → mark#(cons(quot(X, Y), zWquot(XS, YS)))
active#(sel(s(N), cons(X, XS))) → mark#(sel(N, XS))mark#(quot(X1, X2)) → mark#(X1)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Function Precedence

minus = mark = from = mark# = 0 = s = zWquot = active = active# = quot = sel = cons = nil

Argument Filtering

minus: all arguments are removed from minus
mark: all arguments are removed from mark
from: all arguments are removed from from
mark#: all arguments are removed from mark#
0: all arguments are removed from 0
s: all arguments are removed from s
zWquot: all arguments are removed from zWquot
active: collapses to 1
active#: collapses to 1
quot: all arguments are removed from quot
sel: all arguments are removed from sel
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

minus: multiset
mark: multiset
from: multiset
mark#: multiset
0: multiset
s: multiset
zWquot: multiset
quot: multiset
sel: multiset
cons: multiset
nil: multiset

Usable Rules

active(sel(0, cons(X, XS))) → mark(X)cons(active(X1), X2) → cons(X1, X2)
active(quot(0, s(Y))) → mark(0)from(mark(X)) → from(X)
minus(X1, active(X2)) → minus(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)mark(s(X)) → active(s(mark(X)))
minus(mark(X1), X2) → minus(X1, X2)active(zWquot(nil, XS)) → mark(nil)
quot(X1, mark(X2)) → quot(X1, X2)minus(X1, mark(X2)) → minus(X1, X2)
mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))cons(X1, mark(X2)) → cons(X1, X2)
active(minus(X, 0)) → mark(0)mark(from(X)) → active(from(mark(X)))
active(from(X)) → mark(cons(X, from(s(X))))quot(X1, active(X2)) → quot(X1, X2)
quot(mark(X1), X2) → quot(X1, X2)active(minus(s(X), s(Y))) → mark(minus(X, Y))
mark(nil) → active(nil)mark(0) → active(0)
s(active(X)) → s(X)active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))
from(active(X)) → from(X)cons(X1, active(X2)) → cons(X1, X2)
minus(active(X1), X2) → minus(X1, X2)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
zWquot(mark(X1), X2) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
quot(active(X1), X2) → quot(X1, X2)zWquot(X1, active(X2)) → zWquot(X1, X2)
mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))sel(X1, active(X2)) → sel(X1, X2)
mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))active(zWquot(XS, nil)) → mark(nil)
cons(mark(X1), X2) → cons(X1, X2)mark(cons(X1, X2)) → active(cons(mark(X1), X2))
s(mark(X)) → s(X)sel(active(X1), X2) → sel(X1, X2)
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))
sel(mark(X1), X2) → sel(X1, X2)

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

mark#(nil) → active#(nil)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

cons#(X1, active(X2)) → cons#(X1, X2)cons#(mark(X1), X2) → cons#(X1, X2)
cons#(X1, mark(X2)) → cons#(X1, X2)cons#(active(X1), X2) → cons#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

cons#(mark(X1), X2) → cons#(X1, X2)cons#(active(X1), X2) → cons#(X1, X2)

Problem 10: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

cons#(X1, active(X2)) → cons#(X1, X2)cons#(X1, mark(X2)) → cons#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, zWquot, active, mark, from, quot, sel, nil, cons

Strategy

Function Precedence

mark < active < cons# = minus = 0 = s = zWquot = from = sel = quot = cons = nil

Argument Filtering

cons#: collapses to 2
minus: all arguments are removed from minus
0: all arguments are removed from 0
s: all arguments are removed from s
zWquot: 1 2
active: 1
mark: collapses to 1
from: all arguments are removed from from
sel: 1 2
quot: 1 2
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

minus: multiset
0: multiset
s: multiset
zWquot: lexicographic with permutation 1 → 1 2 → 2
active: multiset
from: multiset
sel: lexicographic with permutation 1 → 1 2 → 2
quot: lexicographic with permutation 1 → 2 2 → 1
cons: multiset
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

cons#(X1, active(X2)) → cons#(X1, X2)

Problem 16: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

cons#(X1, mark(X2)) → cons#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Function Precedence

cons# < mark < minus = 0 = s = zWquot = active = from = sel = quot = cons = nil

Argument Filtering

cons#: collapses to 2
minus: all arguments are removed from minus
0: all arguments are removed from 0
s: all arguments are removed from s
zWquot: all arguments are removed from zWquot
active: all arguments are removed from active
mark: 1
from: 1
sel: all arguments are removed from sel
quot: all arguments are removed from quot
cons: 1
nil: all arguments are removed from nil

Status

minus: multiset
0: multiset
s: multiset
zWquot: multiset
active: multiset
mark: multiset
from: lexicographic with permutation 1 → 1
sel: multiset
quot: multiset
cons: lexicographic with permutation 1 → 1
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

cons#(X1, mark(X2)) → cons#(X1, X2)

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

zWquot#(X1, active(X2)) → zWquot#(X1, X2)zWquot#(mark(X1), X2) → zWquot#(X1, X2)
zWquot#(X1, mark(X2)) → zWquot#(X1, X2)zWquot#(active(X1), X2) → zWquot#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

zWquot#(mark(X1), X2) → zWquot#(X1, X2)zWquot#(active(X1), X2) → zWquot#(X1, X2)

Problem 11: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

zWquot#(X1, active(X2)) → zWquot#(X1, X2)zWquot#(X1, mark(X2)) → zWquot#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, zWquot, active, mark, from, quot, sel, nil, cons

Strategy

Function Precedence

mark < zWquot# < active < minus = 0 = s = zWquot = from = sel = quot = cons = nil

Argument Filtering

zWquot#: collapses to 2
minus: collapses to 1
0: all arguments are removed from 0
s: all arguments are removed from s
zWquot: all arguments are removed from zWquot
active: collapses to 1
mark: 1
from: all arguments are removed from from
sel: 2
quot: all arguments are removed from quot
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

0: multiset
s: multiset
zWquot: multiset
mark: lexicographic with permutation 1 → 1
from: multiset
sel: lexicographic with permutation 2 → 1
quot: multiset
cons: multiset
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

zWquot#(X1, mark(X2)) → zWquot#(X1, X2)

Problem 17: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

zWquot#(X1, active(X2)) → zWquot#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Function Precedence

zWquot# < active < minus = 0 = s = zWquot = mark = from = sel = quot = cons = nil

Argument Filtering

zWquot#: collapses to 2
minus: all arguments are removed from minus
0: all arguments are removed from 0
s: all arguments are removed from s
zWquot: all arguments are removed from zWquot
active: 1
mark: 1
from: all arguments are removed from from
sel: all arguments are removed from sel
quot: 1 2
cons: 1 2
nil: all arguments are removed from nil

Status

minus: multiset
0: multiset
s: multiset
zWquot: multiset
active: multiset
mark: lexicographic with permutation 1 → 1
from: multiset
sel: multiset
quot: lexicographic with permutation 1 → 2 2 → 1
cons: lexicographic with permutation 1 → 1 2 → 2
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

zWquot#(X1, active(X2)) → zWquot#(X1, X2)

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

minus#(X1, active(X2)) → minus#(X1, X2)minus#(mark(X1), X2) → minus#(X1, X2)
minus#(X1, mark(X2)) → minus#(X1, X2)minus#(active(X1), X2) → minus#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

minus#(mark(X1), X2) → minus#(X1, X2)minus#(active(X1), X2) → minus#(X1, X2)

Problem 12: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

minus#(X1, active(X2)) → minus#(X1, X2)minus#(X1, mark(X2)) → minus#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, zWquot, active, mark, from, quot, sel, nil, cons

Strategy

Function Precedence

mark < active < minus# < minus = 0 = s = zWquot = from = sel = quot = cons = nil

Argument Filtering

minus: all arguments are removed from minus
0: all arguments are removed from 0
s: all arguments are removed from s
zWquot: all arguments are removed from zWquot
active: collapses to 1
mark: 1
minus#: collapses to 2
from: all arguments are removed from from
sel: 1
quot: 1 2
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

minus: multiset
0: multiset
s: multiset
zWquot: multiset
mark: multiset
from: multiset
sel: lexicographic with permutation 1 → 1
quot: lexicographic with permutation 1 → 2 2 → 1
cons: multiset
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

minus#(X1, mark(X2)) → minus#(X1, X2)

Problem 18: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

minus#(X1, active(X2)) → minus#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Function Precedence

minus# < active < minus = 0 = s = zWquot = mark = from = sel = quot = cons = nil

Argument Filtering

minus: all arguments are removed from minus
0: all arguments are removed from 0
s: all arguments are removed from s
zWquot: 1 2
active: 1
mark: all arguments are removed from mark
minus#: collapses to 2
from: all arguments are removed from from
sel: all arguments are removed from sel
quot: 2
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

minus: multiset
0: multiset
s: multiset
zWquot: lexicographic with permutation 1 → 2 2 → 1
active: multiset
mark: multiset
from: multiset
sel: multiset
quot: lexicographic with permutation 2 → 1
cons: multiset
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

minus#(X1, active(X2)) → minus#(X1, X2)

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

sel#(mark(X1), X2) → sel#(X1, X2)sel#(active(X1), X2) → sel#(X1, X2)
sel#(X1, active(X2)) → sel#(X1, X2)sel#(X1, mark(X2)) → sel#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

sel#(active(X1), X2) → sel#(X1, X2)sel#(mark(X1), X2) → sel#(X1, X2)

Problem 13: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

sel#(X1, active(X2)) → sel#(X1, X2)sel#(X1, mark(X2)) → sel#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, zWquot, active, mark, from, quot, sel, nil, cons

Strategy

Function Precedence

active = mark < minus = 0 = s = zWquot = from = sel# = sel = quot = cons = nil

Argument Filtering

minus: 2
0: all arguments are removed from 0
s: collapses to 1
zWquot: all arguments are removed from zWquot
active: collapses to 1
mark: 1
from: all arguments are removed from from
sel#: collapses to 2
sel: all arguments are removed from sel
quot: all arguments are removed from quot
cons: collapses to 1
nil: all arguments are removed from nil

Status

minus: lexicographic with permutation 2 → 1
0: multiset
zWquot: multiset
mark: multiset
from: multiset
sel: multiset
quot: multiset
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

sel#(X1, mark(X2)) → sel#(X1, X2)

Problem 19: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

sel#(X1, active(X2)) → sel#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Function Precedence

minus = 0 = s = zWquot = active = mark = from = sel# = sel = quot = cons = nil

Argument Filtering

minus: all arguments are removed from minus
0: all arguments are removed from 0
s: all arguments are removed from s
zWquot: all arguments are removed from zWquot
active: 1
mark: all arguments are removed from mark
from: all arguments are removed from from
sel#: 2
sel: 1 2
quot: 1
cons: 1 2
nil: all arguments are removed from nil

Status

minus: multiset
0: multiset
s: multiset
zWquot: multiset
active: multiset
mark: multiset
from: multiset
sel#: lexicographic with permutation 2 → 1
sel: lexicographic with permutation 1 → 1 2 → 2
quot: lexicographic with permutation 1 → 1
cons: lexicographic with permutation 1 → 2 2 → 1
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

sel#(X1, active(X2)) → sel#(X1, X2)

Problem 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

from#(active(X)) → from#(X)from#(mark(X)) → from#(X)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

from#(active(X)) → from#(X)from#(mark(X)) → from#(X)

Problem 8: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

s#(mark(X)) → s#(X)s#(active(X)) → s#(X)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

s#(mark(X)) → s#(X)s#(active(X)) → s#(X)

Problem 9: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

quot#(X1, active(X2)) → quot#(X1, X2)quot#(mark(X1), X2) → quot#(X1, X2)
quot#(active(X1), X2) → quot#(X1, X2)quot#(X1, mark(X2)) → quot#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

quot#(mark(X1), X2) → quot#(X1, X2)quot#(active(X1), X2) → quot#(X1, X2)

Problem 14: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

quot#(X1, active(X2)) → quot#(X1, X2)quot#(X1, mark(X2)) → quot#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, zWquot, active, mark, from, quot, sel, nil, cons

Strategy

Function Precedence

active < minus = 0 = quot# = s = zWquot = mark = from = sel = quot = cons = nil

Argument Filtering

minus: 1 2
0: all arguments are removed from 0
quot#: 1 2
s: collapses to 1
zWquot: all arguments are removed from zWquot
active: 1
mark: collapses to 1
from: collapses to 1
sel: 1 2
quot: 1
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

minus: lexicographic with permutation 1 → 1 2 → 2
0: multiset
quot#: lexicographic with permutation 1 → 1 2 → 2
zWquot: multiset
active: lexicographic with permutation 1 → 1
sel: lexicographic with permutation 1 → 2 2 → 1
quot: lexicographic with permutation 1 → 1
cons: multiset
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

quot#(X1, active(X2)) → quot#(X1, X2)

Problem 20: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

quot#(X1, mark(X2)) → quot#(X1, X2)

Rewrite Rules

active(from(X)) → mark(cons(X, from(s(X))))active(sel(0, cons(X, XS))) → mark(X)
active(sel(s(N), cons(X, XS))) → mark(sel(N, XS))active(minus(X, 0)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))active(quot(0, s(Y))) → mark(0)
active(quot(s(X), s(Y))) → mark(s(quot(minus(X, Y), s(Y))))active(zWquot(XS, nil)) → mark(nil)
active(zWquot(nil, XS)) → mark(nil)active(zWquot(cons(X, XS), cons(Y, YS))) → mark(cons(quot(X, Y), zWquot(XS, YS)))
mark(from(X)) → active(from(mark(X)))mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(0) → active(0)mark(minus(X1, X2)) → active(minus(mark(X1), mark(X2)))
mark(quot(X1, X2)) → active(quot(mark(X1), mark(X2)))mark(zWquot(X1, X2)) → active(zWquot(mark(X1), mark(X2)))
mark(nil) → active(nil)from(mark(X)) → from(X)
from(active(X)) → from(X)cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)s(mark(X)) → s(X)
s(active(X)) → s(X)sel(mark(X1), X2) → sel(X1, X2)
sel(X1, mark(X2)) → sel(X1, X2)sel(active(X1), X2) → sel(X1, X2)
sel(X1, active(X2)) → sel(X1, X2)minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)quot(mark(X1), X2) → quot(X1, X2)
quot(X1, mark(X2)) → quot(X1, X2)quot(active(X1), X2) → quot(X1, X2)
quot(X1, active(X2)) → quot(X1, X2)zWquot(mark(X1), X2) → zWquot(X1, X2)
zWquot(X1, mark(X2)) → zWquot(X1, X2)zWquot(active(X1), X2) → zWquot(X1, X2)
zWquot(X1, active(X2)) → zWquot(X1, X2)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, zWquot, active, mark, from, sel, quot, cons, nil

Strategy

Function Precedence

mark < minus = 0 = quot# = s = zWquot = active = from = sel = quot = cons = nil

Argument Filtering

minus: 1 2
0: all arguments are removed from 0
quot#: collapses to 2
s: all arguments are removed from s
zWquot: all arguments are removed from zWquot
active: all arguments are removed from active
mark: 1
from: collapses to 1
sel: 1 2
quot: 1 2
cons: 1
nil: all arguments are removed from nil

Status

minus: lexicographic with permutation 1 → 1 2 → 2
0: multiset
s: multiset
zWquot: multiset
active: multiset
mark: multiset
sel: lexicographic with permutation 1 → 2 2 → 1
quot: lexicographic with permutation 1 → 2 2 → 1
cons: lexicographic with permutation 1 → 1
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

quot#(X1, mark(X2)) → quot#(X1, X2)