YES

The TRS could be proven terminating. The proof took 2371 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (167ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (33ms).
 | – Problem 3 was processed with processor ReductionPairSAT (1262ms).
 |    | – Problem 7 was processed with processor DependencyGraph (2ms).
 | – Problem 4 was processed with processor PolynomialLinearRange4 (120ms).
 | – Problem 5 was processed with processor PolynomialLinearRange4 (14ms).
 |    | – Problem 6 was processed with processor PolynomialLinearRange4 (11ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

2ndspos#(s(N), cons2(X, cons(Y, Z))) → 2ndsneg#(N, Z)2ndsneg#(s(N), cons2(X, cons(Y, Z))) → 2ndspos#(N, Z)
T(from(x_1)) → T(x_1)pi#(X) → 2ndspos#(X, from(0))
pi#(X) → from#(0)times#(s(X), Y) → plus#(Y, times(X, Y))
2ndspos#(s(N), cons(X, Z)) → 2ndspos#(s(N), cons2(X, Z))times#(s(X), Y) → times#(X, Y)
2ndspos#(s(N), cons(X, Z)) → T(Z)2ndsneg#(s(N), cons2(X, cons(Y, Z))) → T(Z)
square#(X) → times#(X, X)2ndsneg#(s(N), cons(X, Z)) → T(Z)
T(s(x_1)) → T(x_1)plus#(s(X), Y) → plus#(X, Y)
2ndspos#(s(N), cons2(X, cons(Y, Z))) → T(Z)T(from(s(X))) → from#(s(X))
2ndsneg#(s(N), cons(X, Z)) → 2ndsneg#(s(N), cons2(X, Z))

Rewrite Rules

from(X) → cons(X, from(s(X)))2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, Z)) → 2ndspos(s(N), cons2(X, Z))2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil2ndsneg(s(N), cons(X, Z)) → 2ndsneg(s(N), cons2(X, Z))
2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Yplus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

Original Signature

Termination of terms over the following signature is verified: posrecip, negrecip, plus, cons2, rnil, from, rcons, 2ndspos, 0, s, times, 2ndsneg, square, pi, cons

Strategy

Context-sensitive strategy:
μ(rnil) = μ(T) = μ(0) = μ(nil) = ∅
μ(posrecip) = μ(negrecip) = μ(from#) = μ(square#) = μ(pi#) = μ(from) = μ(s) = μ(square) = μ(pi) = μ(cons) = {1}
μ(cons2) = {2}
μ(plus) = μ(2ndspos#) = μ(2ndsneg#) = μ(rcons) = μ(2ndspos) = μ(times#) = μ(times) = μ(2ndsneg) = μ(plus#) = {1, 2}

The following SCCs where found

T(s(x_1)) → T(x_1)T(from(x_1)) → T(x_1)
2ndspos#(s(N), cons2(X, cons(Y, Z))) → 2ndsneg#(N, Z)2ndsneg#(s(N), cons2(X, cons(Y, Z))) → 2ndspos#(N, Z)
2ndspos#(s(N), cons(X, Z)) → 2ndspos#(s(N), cons2(X, Z))2ndsneg#(s(N), cons(X, Z)) → 2ndsneg#(s(N), cons2(X, Z))
plus#(s(X), Y) → plus#(X, Y)
times#(s(X), Y) → times#(X, Y)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

times#(s(X), Y) → times#(X, Y)

Rewrite Rules

from(X) → cons(X, from(s(X)))2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, Z)) → 2ndspos(s(N), cons2(X, Z))2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil2ndsneg(s(N), cons(X, Z)) → 2ndsneg(s(N), cons2(X, Z))
2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Yplus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

Original Signature

Termination of terms over the following signature is verified: posrecip, negrecip, plus, cons2, rnil, from, rcons, 2ndspos, 0, s, times, 2ndsneg, square, pi, cons

Strategy

Context-sensitive strategy:
μ(rnil) = μ(T) = μ(0) = μ(nil) = ∅
μ(posrecip) = μ(negrecip) = μ(from#) = μ(square#) = μ(pi#) = μ(from) = μ(s) = μ(square) = μ(pi) = μ(cons) = {1}
μ(cons2) = {2}
μ(plus) = μ(2ndspos#) = μ(2ndsneg#) = μ(rcons) = μ(2ndspos) = μ(times#) = μ(2ndsneg) = μ(times) = μ(plus#) = {1, 2}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

times#(s(X), Y) → times#(X, Y)

Problem 3: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

2ndspos#(s(N), cons2(X, cons(Y, Z))) → 2ndsneg#(N, Z)2ndsneg#(s(N), cons2(X, cons(Y, Z))) → 2ndspos#(N, Z)
2ndspos#(s(N), cons(X, Z)) → 2ndspos#(s(N), cons2(X, Z))2ndsneg#(s(N), cons(X, Z)) → 2ndsneg#(s(N), cons2(X, Z))

Rewrite Rules

from(X) → cons(X, from(s(X)))2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, Z)) → 2ndspos(s(N), cons2(X, Z))2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil2ndsneg(s(N), cons(X, Z)) → 2ndsneg(s(N), cons2(X, Z))
2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Yplus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

Original Signature

Termination of terms over the following signature is verified: posrecip, negrecip, plus, cons2, rnil, from, rcons, 2ndspos, 0, s, times, 2ndsneg, square, pi, cons

Strategy

Context-sensitive strategy:
μ(rnil) = μ(T) = μ(0) = μ(nil) = ∅
μ(posrecip) = μ(negrecip) = μ(from#) = μ(square#) = μ(pi#) = μ(from) = μ(s) = μ(square) = μ(pi) = μ(cons) = {1}
μ(cons2) = {2}
μ(plus) = μ(2ndspos#) = μ(2ndsneg#) = μ(rcons) = μ(2ndspos) = μ(times#) = μ(2ndsneg) = μ(times) = μ(plus#) = {1, 2}

Function Precedence

2ndspos# < 0 < times < rcons < cons2 < plus < 2ndsneg < cons < posrecip = negrecip = rnil = 2ndsneg# = from = 2ndspos = s = square = pi

Argument Filtering

plus: 1 2
posrecip: all arguments are removed from posrecip
negrecip: all arguments are removed from negrecip
cons2: collapses to 2
2ndspos#: collapses to 1
rnil: all arguments are removed from rnil
2ndsneg#: 1
from: collapses to 1
rcons: collapses to 1
2ndspos: all arguments are removed from 2ndspos
0: all arguments are removed from 0
s: 1
times: 1 2
2ndsneg: collapses to 1
square: all arguments are removed from square
pi: all arguments are removed from pi
cons: collapses to 1

Status

plus: lexicographic with permutation 1 → 2 2 → 1
posrecip: multiset
negrecip: multiset
rnil: multiset
2ndsneg#: multiset
2ndspos: multiset
0: multiset
s: multiset
times: lexicographic with permutation 1 → 2 2 → 1
square: multiset
pi: multiset

Usable Rules

plus(0, Y) → Y2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
times(0, Y) → 02ndspos(0, Z) → rnil
plus(s(X), Y) → s(plus(X, Y))2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
from(X) → cons(X, from(s(X)))times(s(X), Y) → plus(Y, times(X, Y))
2ndsneg(0, Z) → rnil2ndspos(s(N), cons(X, Z)) → 2ndspos(s(N), cons2(X, Z))
2ndsneg(s(N), cons(X, Z)) → 2ndsneg(s(N), cons2(X, Z))

Eliminated dependency pairs

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

2ndsneg#(s(N), cons2(X, cons(Y, Z))) → 2ndspos#(N, Z)

Problem 7: DependencyGraph

Dependency Pair Problem

Dependency Pairs

2ndspos#(s(N), cons2(X, cons(Y, Z))) → 2ndsneg#(N, Z)2ndsneg#(s(N), cons(X, Z)) → 2ndsneg#(s(N), cons2(X, Z))
2ndspos#(s(N), cons(X, Z)) → 2ndspos#(s(N), cons2(X, Z))

Rewrite Rules

from(X) → cons(X, from(s(X)))2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, Z)) → 2ndspos(s(N), cons2(X, Z))2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil2ndsneg(s(N), cons(X, Z)) → 2ndsneg(s(N), cons2(X, Z))
2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Yplus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

Original Signature

Termination of terms over the following signature is verified: posrecip, negrecip, plus, cons2, rnil, from, rcons, 2ndspos, 0, s, times, 2ndsneg, square, pi, cons

Strategy

Context-sensitive strategy:
μ(rnil) = μ(T) = μ(0) = μ(nil) = ∅
μ(posrecip) = μ(negrecip) = μ(from#) = μ(square#) = μ(pi#) = μ(from) = μ(s) = μ(square) = μ(pi) = μ(cons) = {1}
μ(cons2) = {2}
μ(plus) = μ(2ndspos#) = μ(2ndsneg#) = μ(rcons) = μ(2ndspos) = μ(times#) = μ(times) = μ(2ndsneg) = μ(plus#) = {1, 2}

There are no SCCs!

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

plus#(s(X), Y) → plus#(X, Y)

Rewrite Rules

from(X) → cons(X, from(s(X)))2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, Z)) → 2ndspos(s(N), cons2(X, Z))2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil2ndsneg(s(N), cons(X, Z)) → 2ndsneg(s(N), cons2(X, Z))
2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Yplus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

Original Signature

Termination of terms over the following signature is verified: posrecip, negrecip, plus, cons2, rnil, from, rcons, 2ndspos, 0, s, times, 2ndsneg, square, pi, cons

Strategy

Context-sensitive strategy:
μ(rnil) = μ(T) = μ(0) = μ(nil) = ∅
μ(posrecip) = μ(negrecip) = μ(from#) = μ(square#) = μ(pi#) = μ(from) = μ(s) = μ(square) = μ(pi) = μ(cons) = {1}
μ(cons2) = {2}
μ(plus) = μ(2ndspos#) = μ(2ndsneg#) = μ(rcons) = μ(2ndspos) = μ(times#) = μ(2ndsneg) = μ(times) = μ(plus#) = {1, 2}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

plus#(s(X), Y) → plus#(X, Y)

Problem 5: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(s(x_1)) → T(x_1)T(from(x_1)) → T(x_1)

Rewrite Rules

from(X) → cons(X, from(s(X)))2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, Z)) → 2ndspos(s(N), cons2(X, Z))2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil2ndsneg(s(N), cons(X, Z)) → 2ndsneg(s(N), cons2(X, Z))
2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Yplus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

Original Signature

Termination of terms over the following signature is verified: posrecip, negrecip, plus, cons2, rnil, from, rcons, 2ndspos, 0, s, times, 2ndsneg, square, pi, cons

Strategy

Context-sensitive strategy:
μ(rnil) = μ(T) = μ(0) = μ(nil) = ∅
μ(posrecip) = μ(negrecip) = μ(from#) = μ(square#) = μ(pi#) = μ(from) = μ(s) = μ(square) = μ(pi) = μ(cons) = {1}
μ(cons2) = {2}
μ(plus) = μ(2ndspos#) = μ(2ndsneg#) = μ(rcons) = μ(2ndspos) = μ(times#) = μ(2ndsneg) = μ(times) = μ(plus#) = {1, 2}

Polynomial Interpretation

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(from(x_1)) → T(x_1)

Problem 6: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(s(x_1)) → T(x_1)

Rewrite Rules

from(X) → cons(X, from(s(X)))2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, Z)) → 2ndspos(s(N), cons2(X, Z))2ndspos(s(N), cons2(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))
2ndsneg(0, Z) → rnil2ndsneg(s(N), cons(X, Z)) → 2ndsneg(s(N), cons2(X, Z))
2ndsneg(s(N), cons2(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Yplus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)

Original Signature

Termination of terms over the following signature is verified: posrecip, negrecip, plus, cons2, rnil, from, rcons, 2ndspos, 0, s, times, 2ndsneg, square, pi, cons

Strategy

Context-sensitive strategy:
μ(rnil) = μ(T) = μ(0) = μ(nil) = ∅
μ(posrecip) = μ(negrecip) = μ(from#) = μ(square#) = μ(pi#) = μ(from) = μ(s) = μ(square) = μ(pi) = μ(cons) = {1}
μ(cons2) = {2}
μ(plus) = μ(2ndspos#) = μ(2ndsneg#) = μ(rcons) = μ(2ndspos) = μ(times#) = μ(times) = μ(2ndsneg) = μ(plus#) = {1, 2}

Polynomial Interpretation

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)