YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (87ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (89ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4 (37ms).
 | – Problem 4 was processed with processor PolynomialLinearRange4 (292ms).
 |    | – Problem 5 was processed with processor DependencyGraph (5ms).
 |    |    | – Problem 6 was processed with processor PolynomialLinearRange4 (137ms).
 |    |    |    | – Problem 7 was processed with processor PolynomialLinearRange4 (72ms).
 |    |    |    |    | – Problem 8 was processed with processor PolynomialLinearRange4 (15ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

if#(false, X, Y) → T(Y)T(minus(x_1, x_2)) → T(x_2)
T(div(minus(X, Y), s(Y))) → div#(minus(X, Y), s(Y))T(div(x_1, x_2)) → T(x_2)
T(minus(x_1, x_2)) → T(x_1)div#(s(X), s(Y)) → geq#(X, Y)
div#(s(X), s(Y)) → if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)T(div(x_1, x_2)) → T(x_1)
geq#(s(X), s(Y)) → geq#(X, Y)minus#(s(X), s(Y)) → minus#(X, Y)
T(s(x_1)) → T(x_1)T(minus(X, Y)) → minus#(X, Y)
if#(true, X, Y) → T(X)

Rewrite Rules

minus(0, Y) → 0minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → truegeq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)if(true, X, Y) → X
if(false, X, Y) → Y

Original Signature

Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, true, false

Strategy

Context-sensitive strategy:
μ(geq) = μ(minus) = μ(geq#) = μ(true) = μ(minus#) = μ(T) = μ(0) = μ(false) = ∅
μ(div) = μ(div#) = μ(s) = μ(if) = μ(if#) = {1}

The following SCCs where found

geq#(s(X), s(Y)) → geq#(X, Y)
minus#(s(X), s(Y)) → minus#(X, Y)
div#(s(X), s(Y)) → if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)T(div(x_1, x_2)) → T(x_1)
T(minus(x_1, x_2)) → T(x_2)if#(false, X, Y) → T(Y)
T(div(minus(X, Y), s(Y))) → div#(minus(X, Y), s(Y))T(s(x_1)) → T(x_1)
T(div(x_1, x_2)) → T(x_2)T(minus(x_1, x_2)) → T(x_1)
if#(true, X, Y) → T(X)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

minus(0, Y) → 0minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → truegeq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)if(true, X, Y) → X
if(false, X, Y) → Y

Original Signature

Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, true, false

Strategy

Context-sensitive strategy:
μ(geq) = μ(minus) = μ(geq#) = μ(true) = μ(minus#) = μ(T) = μ(0) = μ(false) = ∅
μ(div) = μ(div#) = μ(s) = μ(if) = μ(if#) = {1}

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:

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

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

minus(0, Y) → 0minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → truegeq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)if(true, X, Y) → X
if(false, X, Y) → Y

Original Signature

Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, true, false

Strategy

Context-sensitive strategy:
μ(geq) = μ(minus) = μ(geq#) = μ(true) = μ(minus#) = μ(T) = μ(0) = μ(false) = ∅
μ(div) = μ(div#) = μ(s) = μ(if) = μ(if#) = {1}

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:

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

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

div#(s(X), s(Y)) → if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)T(div(x_1, x_2)) → T(x_1)
T(minus(x_1, x_2)) → T(x_2)if#(false, X, Y) → T(Y)
T(div(minus(X, Y), s(Y))) → div#(minus(X, Y), s(Y))T(s(x_1)) → T(x_1)
T(div(x_1, x_2)) → T(x_2)T(minus(x_1, x_2)) → T(x_1)
if#(true, X, Y) → T(X)

Rewrite Rules

minus(0, Y) → 0minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → truegeq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)if(true, X, Y) → X
if(false, X, Y) → Y

Original Signature

Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, true, false

Strategy

Context-sensitive strategy:
μ(geq) = μ(minus) = μ(geq#) = μ(true) = μ(minus#) = μ(T) = μ(0) = μ(false) = ∅
μ(div) = μ(div#) = μ(s) = μ(if) = μ(if#) = {1}

Polynomial Interpretation

Standard Usable rules

geq(0, s(Y)) → falseif(false, X, Y) → Y
if(true, X, Y) → Xdiv(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
minus(0, Y) → 0geq(X, 0) → true
geq(s(X), s(Y)) → geq(X, Y)minus(s(X), s(Y)) → minus(X, Y)
div(0, s(Y)) → 0

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

div#(s(X), s(Y)) → if#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)

Problem 5: DependencyGraph

Dependency Pair Problem

Dependency Pairs

T(div(x_1, x_2)) → T(x_1)if#(false, X, Y) → T(Y)
T(minus(x_1, x_2)) → T(x_2)T(div(minus(X, Y), s(Y))) → div#(minus(X, Y), s(Y))
T(s(x_1)) → T(x_1)T(div(x_1, x_2)) → T(x_2)
T(minus(x_1, x_2)) → T(x_1)if#(true, X, Y) → T(X)

Rewrite Rules

minus(0, Y) → 0minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → truegeq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)if(true, X, Y) → X
if(false, X, Y) → Y

Original Signature

Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, false, true

Strategy

Context-sensitive strategy:
μ(geq) = μ(minus) = μ(geq#) = μ(true) = μ(minus#) = μ(T) = μ(0) = μ(false) = ∅
μ(div) = μ(div#) = μ(s) = μ(if) = μ(if#) = {1}

The following SCCs where found

T(div(x_1, x_2)) → T(x_1)T(minus(x_1, x_2)) → T(x_2)
T(s(x_1)) → T(x_1)T(div(x_1, x_2)) → T(x_2)
T(minus(x_1, x_2)) → T(x_1)

Problem 6: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(div(x_1, x_2)) → T(x_1)T(minus(x_1, x_2)) → T(x_2)
T(s(x_1)) → T(x_1)T(div(x_1, x_2)) → T(x_2)
T(minus(x_1, x_2)) → T(x_1)

Rewrite Rules

minus(0, Y) → 0minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → truegeq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)if(true, X, Y) → X
if(false, X, Y) → Y

Original Signature

Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, false, true

Strategy

Context-sensitive strategy:
μ(geq) = μ(minus) = μ(geq#) = μ(true) = μ(minus#) = μ(T) = μ(0) = μ(false) = ∅
μ(div) = μ(div#) = μ(s) = μ(if) = μ(if#) = {1}

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 7: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(div(x_1, x_2)) → T(x_1)T(minus(x_1, x_2)) → T(x_2)
T(div(x_1, x_2)) → T(x_2)T(minus(x_1, x_2)) → T(x_1)

Rewrite Rules

minus(0, Y) → 0minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → truegeq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)if(true, X, Y) → X
if(false, X, Y) → Y

Original Signature

Termination of terms over the following signature is verified: geq, minus, 0, s, if, div, true, false

Strategy

Context-sensitive strategy:
μ(geq) = μ(minus) = μ(geq#) = μ(true) = μ(minus#) = μ(T) = μ(0) = μ(false) = ∅
μ(div) = μ(div#) = μ(s) = μ(if) = μ(if#) = {1}

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(minus(x_1, x_2)) → T(x_2)T(minus(x_1, x_2)) → T(x_1)

Problem 8: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(div(x_1, x_2)) → T(x_1)T(div(x_1, x_2)) → T(x_2)

Rewrite Rules

minus(0, Y) → 0minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → truegeq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)if(true, X, Y) → X
if(false, X, Y) → Y

Original Signature

Termination of terms over the following signature is verified: geq, 0, minus, s, if, div, false, true

Strategy

Context-sensitive strategy:
μ(geq) = μ(minus) = μ(geq#) = μ(true) = μ(minus#) = μ(T) = μ(0) = μ(false) = ∅
μ(div) = μ(div#) = μ(s) = μ(if) = μ(if#) = {1}

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(div(x_1, x_2)) → T(x_1)T(div(x_1, x_2)) → T(x_2)