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)