YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (85ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (51ms).
 | – Problem 3 was processed with processor ReductionPairSAT (675ms).
 |    | – Problem 7 was processed with processor DependencyGraph (0ms).
 | – Problem 4 was processed with processor PolynomialLinearRange4 (30ms).
 |    | – Problem 6 was processed with processor PolynomialLinearRange4 (9ms).
 | – Problem 5 was processed with processor PolynomialLinearRange4 (92ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

from(X)cons(X, from(s(X)))2ndspos(0, Z)rnil
2ndspos(s(N), cons(X, cons(Y, Z)))rcons(posrecip(Y), 2ndsneg(N, Z))2ndsneg(0, Z)rnil
2ndsneg(s(N), cons(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, rnil, from, rcons, 2ndspos, 0, s, 2ndsneg, times, square, pi, cons

Strategy

Context-sensitive strategy:
μ(rnil) = μ(T) = μ(0) = μ(nil) = ∅
μ(negrecip) = μ(posrecip) = μ(from#) = μ(square#) = μ(pi#) = μ(from) = μ(s) = μ(square) = μ(pi) = μ(cons) = {1}
μ(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)

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

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

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

Problem 2: 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, cons(Y, Z)))rcons(posrecip(Y), 2ndsneg(N, Z))2ndsneg(0, Z)rnil
2ndsneg(s(N), cons(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, rnil, from, rcons, 2ndspos, 0, s, 2ndsneg, times, square, pi, cons

Strategy

Context-sensitive strategy:
μ(rnil) = μ(T) = μ(0) = μ(nil) = ∅
μ(negrecip) = μ(posrecip) = μ(from#) = μ(square#) = μ(pi#) = μ(from) = μ(s) = μ(square) = μ(pi) = μ(cons) = {1}
μ(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 3: ReductionPairSAT



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

from(X)cons(X, from(s(X)))2ndspos(0, Z)rnil
2ndspos(s(N), cons(X, cons(Y, Z)))rcons(posrecip(Y), 2ndsneg(N, Z))2ndsneg(0, Z)rnil
2ndsneg(s(N), cons(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, rnil, from, rcons, 2ndspos, 0, s, 2ndsneg, times, square, pi, cons

Strategy

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


Function Precedence

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

Argument Filtering

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

Status

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

Usable Rules

plus(0, Y) → Ytimes(0, Y) → 0
2ndspos(0, Z) → rnilplus(s(X), Y) → s(plus(X, Y))
from(X) → cons(X, from(s(X)))times(s(X), Y) → plus(Y, times(X, Y))
2ndsneg(0, Z) → rnil2ndsneg(s(N), cons(X, cons(Y, Z))) → rcons(negrecip(Y), 2ndspos(N, Z))
2ndspos(s(N), cons(X, cons(Y, Z))) → rcons(posrecip(Y), 2ndsneg(N, Z))

Eliminated dependency pairs

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

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

Problem 7: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

from(X)cons(X, from(s(X)))2ndspos(0, Z)rnil
2ndspos(s(N), cons(X, cons(Y, Z)))rcons(posrecip(Y), 2ndsneg(N, Z))2ndsneg(0, Z)rnil
2ndsneg(s(N), cons(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, rnil, from, rcons, 2ndspos, 0, s, 2ndsneg, times, square, pi, cons

Strategy

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


There are no SCCs!

Problem 4: 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, cons(Y, Z)))rcons(posrecip(Y), 2ndsneg(N, Z))2ndsneg(0, Z)rnil
2ndsneg(s(N), cons(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, rnil, from, rcons, 2ndspos, 0, s, 2ndsneg, times, square, pi, cons

Strategy

Context-sensitive strategy:
μ(rnil) = μ(T) = μ(0) = μ(nil) = ∅
μ(negrecip) = μ(posrecip) = μ(from#) = μ(square#) = μ(pi#) = μ(from) = μ(s) = μ(square) = μ(pi) = μ(cons) = {1}
μ(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(s(x_1))T(x_1)

Problem 6: PolynomialLinearRange4



Dependency Pair Problem

Dependency Pairs

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, cons(Y, Z)))rcons(posrecip(Y), 2ndsneg(N, Z))2ndsneg(0, Z)rnil
2ndsneg(s(N), cons(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, rnil, from, rcons, 2ndspos, 0, s, 2ndsneg, times, square, pi, cons

Strategy

Context-sensitive strategy:
μ(rnil) = μ(T) = μ(0) = μ(nil) = ∅
μ(negrecip) = μ(posrecip) = μ(from#) = μ(square#) = μ(pi#) = μ(from) = μ(s) = μ(square) = μ(pi) = μ(cons) = {1}
μ(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(from(x_1))T(x_1)

Problem 5: 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, cons(Y, Z)))rcons(posrecip(Y), 2ndsneg(N, Z))2ndsneg(0, Z)rnil
2ndsneg(s(N), cons(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, rnil, from, rcons, 2ndspos, 0, s, 2ndsneg, times, square, pi, cons

Strategy

Context-sensitive strategy:
μ(rnil) = μ(T) = μ(0) = μ(nil) = ∅
μ(negrecip) = μ(posrecip) = μ(from#) = μ(square#) = μ(pi#) = μ(from) = μ(s) = μ(square) = μ(pi) = μ(cons) = {1}
μ(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)