YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (741ms).
 | – Problem 2 was processed with processor SubtermCriterion (3ms).
 | – Problem 3 was processed with processor SubtermCriterion (12ms).
 | – Problem 4 was processed with processor SubtermCriterion (2ms).
 | – Problem 5 was processed with processor SubtermCriterion (2ms).
 | – Problem 6 was processed with processor PolynomialLinearRange4iUR (335ms).
 |    | – Problem 11 was processed with processor PolynomialLinearRange4iUR (144ms).
 |    |    | – Problem 14 was processed with processor DependencyGraph (2ms).
 |    |    |    | – Problem 16 was processed with processor PolynomialLinearRange4iUR (114ms).
 |    |    |    | – Problem 17 was processed with processor PolynomialLinearRange4iUR (159ms).
 | – Problem 7 was processed with processor SubtermCriterion (0ms).
 | – Problem 8 was processed with processor PolynomialLinearRange4iUR (300ms).
 |    | – Problem 12 was processed with processor PolynomialLinearRange4iUR (92ms).
 |    |    | – Problem 15 was processed with processor PolynomialLinearRange4iUR (76ms).
 | – Problem 9 was processed with processor PolynomialLinearRange4iUR (30ms).
 |    | – Problem 13 was processed with processor PolynomialLinearRange4iUR (16ms).
 | – Problem 10 was processed with processor SubtermCriterion (0ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

wb#(n(x, y, z)) → wb#(y)wb#(n(x, y, z)) → wb#(z)
-#(1(x), 1(y)) → 0#(-(x, y))+#(0(x), 0(y)) → +#(x, y)
-#(0(x), 1(y)) → -#(x, y)-#(0(x), 0(y)) → -#(x, y)
wb#(n(x, y, z)) → -#(size(y), size(z))bs#(n(x, y, z)) → bs#(y)
wb#(n(x, y, z)) → and#(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))+#(1(x), 0(y)) → +#(x, y)
bs#(n(x, y, z)) → and#(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))ge#(1(x), 1(y)) → ge#(x, y)
size#(n(x, y, z)) → +#(size(x), size(y))ge#(0(x), 1(y)) → ge#(y, x)
bs#(n(x, y, z)) → ge#(min(z), x)size#(n(x, y, z)) → size#(y)
ge#(1(x), 0(y)) → ge#(x, y)bs#(n(x, y, z)) → ge#(x, max(y))
bs#(n(x, y, z)) → max#(y)wb#(n(x, y, z)) → size#(z)
bs#(n(x, y, z)) → bs#(z)+#(1(x), 1(y)) → +#(x, y)
ge#(#, 0(x)) → ge#(#, x)max#(n(x, y, z)) → max#(z)
+#(x, +(y, z)) → +#(x, y)ge#(0(x), 1(y)) → not#(ge(y, x))
-#(0(x), 0(y)) → 0#(-(x, y))wb#(n(x, y, z)) → and#(wb(y), wb(z))
+#(0(x), 0(y)) → 0#(+(x, y))min#(n(x, y, z)) → min#(y)
wb#(n(x, y, z)) → -#(size(z), size(y))wb#(n(x, y, z)) → if#(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y))))
bs#(n(x, y, z)) → min#(z)size#(n(x, y, z)) → size#(x)
-#(1(x), 1(y)) → -#(x, y)+#(0(x), 1(y)) → +#(x, y)
+#(1(x), 1(y)) → 0#(+(+(x, y), 1(#)))-#(1(x), 0(y)) → -#(x, y)
wb#(n(x, y, z)) → ge#(1(#), -(size(y), size(z)))bs#(n(x, y, z)) → and#(bs(y), bs(z))
+#(x, +(y, z)) → +#(+(x, y), z)-#(0(x), 1(y)) → -#(-(x, y), 1(#))
wb#(n(x, y, z)) → ge#(size(y), size(z))+#(1(x), 1(y)) → +#(+(x, y), 1(#))
wb#(n(x, y, z)) → ge#(1(#), -(size(z), size(y)))size#(n(x, y, z)) → +#(+(size(x), size(y)), 1(#))
wb#(n(x, y, z)) → size#(y)bs#(n(x, y, z)) → and#(ge(x, max(y)), ge(min(z), x))
ge#(0(x), 0(y)) → ge#(x, y)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

The following SCCs where found

wb#(n(x, y, z)) → wb#(y)wb#(n(x, y, z)) → wb#(z)
min#(n(x, y, z)) → min#(y)
size#(n(x, y, z)) → size#(x)size#(n(x, y, z)) → size#(y)
ge#(1(x), 1(y)) → ge#(x, y)ge#(0(x), 1(y)) → ge#(y, x)
ge#(0(x), 0(y)) → ge#(x, y)ge#(1(x), 0(y)) → ge#(x, y)
bs#(n(x, y, z)) → bs#(y)bs#(n(x, y, z)) → bs#(z)
+#(0(x), 1(y)) → +#(x, y)+#(0(x), 0(y)) → +#(x, y)
+#(x, +(y, z)) → +#(+(x, y), z)+#(1(x), 1(y)) → +#(x, y)
+#(1(x), 1(y)) → +#(+(x, y), 1(#))+#(1(x), 0(y)) → +#(x, y)
+#(x, +(y, z)) → +#(x, y)
ge#(#, 0(x)) → ge#(#, x)
max#(n(x, y, z)) → max#(z)
-#(1(x), 0(y)) → -#(x, y)-#(0(x), 1(y)) → -#(x, y)
-#(0(x), 1(y)) → -#(-(x, y), 1(#))-#(1(x), 1(y)) → -#(x, y)
-#(0(x), 0(y)) → -#(x, y)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

wb#(n(x, y, z)) → wb#(y)wb#(n(x, y, z)) → wb#(z)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

wb#(n(x, y, z)) → wb#(y)wb#(n(x, y, z)) → wb#(z)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

min#(n(x, y, z)) → min#(y)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

min#(n(x, y, z)) → min#(y)

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

bs#(n(x, y, z)) → bs#(y)bs#(n(x, y, z)) → bs#(z)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

bs#(n(x, y, z)) → bs#(y)bs#(n(x, y, z)) → bs#(z)

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

ge#(#, 0(x)) → ge#(#, x)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

ge#(#, 0(x)) → ge#(#, x)

Problem 6: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

+#(0(x), 1(y)) → +#(x, y)+#(0(x), 0(y)) → +#(x, y)
+#(x, +(y, z)) → +#(+(x, y), z)+#(1(x), 1(y)) → +#(x, y)
+#(1(x), 1(y)) → +#(+(x, y), 1(#))+#(1(x), 0(y)) → +#(x, y)
+#(x, +(y, z)) → +#(x, y)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Polynomial Interpretation

Improved Usable rules

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

+#(0(x), 0(y)) → +#(x, y)+#(1(x), 0(y)) → +#(x, y)

Problem 11: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

+#(0(x), 1(y)) → +#(x, y)+#(x, +(y, z)) → +#(+(x, y), z)
+#(1(x), 1(y)) → +#(x, y)+#(1(x), 1(y)) → +#(+(x, y), 1(#))
+#(x, +(y, z)) → +#(x, y)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Polynomial Interpretation

Improved Usable rules

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

+#(0(x), 1(y)) → +#(x, y)+#(1(x), 1(y)) → +#(x, y)

Problem 14: DependencyGraph

Dependency Pair Problem

Dependency Pairs

+#(x, +(y, z)) → +#(+(x, y), z)+#(1(x), 1(y)) → +#(+(x, y), 1(#))
+#(x, +(y, z)) → +#(x, y)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

The following SCCs where found

+#(1(x), 1(y)) → +#(+(x, y), 1(#))
+#(x, +(y, z)) → +#(+(x, y), z)+#(x, +(y, z)) → +#(x, y)

Problem 16: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

+#(1(x), 1(y)) → +#(+(x, y), 1(#))

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Polynomial Interpretation

Improved Usable rules

+(0(x), 0(y)) → 0(+(x, y))+(x, +(y, z)) → +(+(x, y), z)
+(1(x), 0(y)) → 1(+(x, y))0(#) → #
+(x, #) → x+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(#, x) → x

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

+#(1(x), 1(y)) → +#(+(x, y), 1(#))

Problem 17: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

+#(x, +(y, z)) → +#(+(x, y), z)+#(x, +(y, z)) → +#(x, y)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Polynomial Interpretation

Improved Usable rules

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

+#(x, +(y, z)) → +#(+(x, y), z)+#(x, +(y, z)) → +#(x, y)

Problem 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

max#(n(x, y, z)) → max#(z)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

max#(n(x, y, z)) → max#(z)

Problem 8: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

-#(1(x), 0(y)) → -#(x, y)-#(0(x), 1(y)) → -#(x, y)
-#(0(x), 1(y)) → -#(-(x, y), 1(#))-#(1(x), 1(y)) → -#(x, y)
-#(0(x), 0(y)) → -#(x, y)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Polynomial Interpretation

Improved Usable rules

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

-#(1(x), 0(y)) → -#(x, y)-#(0(x), 0(y)) → -#(x, y)

Problem 12: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

-#(0(x), 1(y)) → -#(x, y)-#(0(x), 1(y)) → -#(-(x, y), 1(#))
-#(1(x), 1(y)) → -#(x, y)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Polynomial Interpretation

Improved Usable rules

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

-#(0(x), 1(y)) → -#(x, y)-#(1(x), 1(y)) → -#(x, y)

Problem 15: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

-#(0(x), 1(y)) → -#(-(x, y), 1(#))

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Polynomial Interpretation

Improved Usable rules

-(1(x), 1(y)) → 0(-(x, y))0(#) → #
-(0(x), 0(y)) → 0(-(x, y))-(1(x), 0(y)) → 1(-(x, y))
-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))-(x, #) → x
-(#, x) → #

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

-#(0(x), 1(y)) → -#(-(x, y), 1(#))

Problem 9: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

ge#(1(x), 1(y)) → ge#(x, y)ge#(0(x), 1(y)) → ge#(y, x)
ge#(0(x), 0(y)) → ge#(x, y)ge#(1(x), 0(y)) → ge#(x, y)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

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:

ge#(1(x), 1(y)) → ge#(x, y)ge#(0(x), 1(y)) → ge#(y, x)
ge#(1(x), 0(y)) → ge#(x, y)

Problem 13: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

ge#(0(x), 0(y)) → ge#(x, y)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

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:

ge#(0(x), 0(y)) → ge#(x, y)

Problem 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

size#(n(x, y, z)) → size#(x)size#(n(x, y, z)) → size#(y)

Rewrite Rules

0(#) → #+(x, #) → x
+(#, x) → x+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))+(x, +(y, z)) → +(+(x, y), z)
-(x, #) → x-(#, x) → #
-(0(x), 0(y)) → 0(-(x, y))-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))-(1(x), 1(y)) → 0(-(x, y))
not(false) → truenot(true) → false
and(x, true) → xand(x, false) → false
if(true, x, y) → xif(false, x, y) → y
ge(0(x), 0(y)) → ge(x, y)ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → truege(#, 1(x)) → false
ge(#, 0(x)) → ge(#, x)val(l(x)) → x
val(n(x, y, z)) → xmin(l(x)) → x
min(n(x, y, z)) → min(y)max(l(x)) → x
max(n(x, y, z)) → max(z)bs(l(x)) → true
bs(n(x, y, z)) → and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))size(l(x)) → 1(#)
size(n(x, y, z)) → +(+(size(x), size(y)), 1(#))wb(l(x)) → true
wb(n(x, y, z)) → and(if(ge(size(y), size(z)), ge(1(#), -(size(y), size(z))), ge(1(#), -(size(z), size(y)))), and(wb(y), wb(z)))

Original Signature

Termination of terms over the following signature is verified: min, val, #, max, n, +, true, ge, l, bs, size, -, and, not, 1, 0, if, false, wb

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

size#(n(x, y, z)) → size#(x)size#(n(x, y, z)) → size#(y)