YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (1138ms).
 | – Problem 2 was processed with processor SubtermCriterion (2ms).
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).
 | – Problem 5 was processed with processor SubtermCriterion (0ms).
 |    | – Problem 16 was processed with processor SubtermCriterion (1ms).
 | – Problem 6 was processed with processor SubtermCriterion (1ms).
 | – Problem 7 was processed with processor SubtermCriterion (0ms).
 | – Problem 8 was processed with processor SubtermCriterion (0ms).
 | – Problem 9 was processed with processor SubtermCriterion (0ms).
 | – Problem 10 was processed with processor PolynomialLinearRange4iUR (412ms).
 |    | – Problem 17 was processed with processor PolynomialLinearRange4iUR (97ms).
 |    |    | – Problem 21 was processed with processor PolynomialLinearRange4iUR (82ms).
 | – Problem 11 was processed with processor PolynomialLinearRange4iUR (116ms).
 |    | – Problem 18 was processed with processor PolynomialLinearRange4iUR (10ms).
 | – Problem 12 was processed with processor PolynomialLinearRange4iUR (337ms).
 |    | – Problem 19 was processed with processor PolynomialLinearRange4iUR (226ms).
 |    |    | – Problem 22 was processed with processor PolynomialLinearRange4iUR (218ms).
 |    |    |    | – Problem 23 was processed with processor PolynomialLinearRange4iUR (148ms).
 |    |    |    |    | – Problem 24 was processed with processor DependencyGraph (1ms).
 | – Problem 13 was processed with processor PolynomialLinearRange4iUR (127ms).
 |    | – Problem 20 was processed with processor PolynomialLinearRange4iUR (79ms).
 | – Problem 14 was processed with processor SubtermCriterion (0ms).
 | – Problem 15 was processed with processor SubtermCriterion (0ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

-#(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)
log'#(1(x)) → +#(log'(x), 1(#))app#(cons(x, l1), l2) → app#(l1, l2)
inter#(l1, cons(x, l2)) → ifinter#(mem(x, l1), x, l2, l1)sum#(nil) → 0#(#)
mem#(x, cons(y, l)) → if#(eq(x, y), true, mem(x, l))*#(x, +(y, z)) → *#(x, y)
prod#(app(l1, l2)) → prod#(l2)sum#(app(l1, l2)) → sum#(l2)
+#(1(x), 0(y)) → +#(x, y)log#(x) → -#(log'(x), 1(#))
log'#(0(x)) → if#(ge(x, 1(#)), +(log'(x), 1(#)), #)ge#(1(x), 1(y)) → ge#(x, y)
ge#(0(x), 1(y)) → ge#(y, x)*#(*(x, y), z) → *#(y, z)
sum#(cons(x, l)) → sum#(l)inter#(cons(x, l1), l2) → ifinter#(mem(x, l2), x, l1, l2)
log'#(0(x)) → ge#(x, 1(#))ge#(1(x), 0(y)) → ge#(x, y)
eq#(#, 0(y)) → eq#(#, y)*#(1(x), y) → *#(x, y)
log'#(1(x)) → log'#(x)*#(1(x), y) → 0#(*(x, y))
inter#(app(l1, l2), l3) → inter#(l1, l3)log'#(0(x)) → log'#(x)
+#(1(x), 1(y)) → +#(x, y)ge#(#, 0(x)) → ge#(#, x)
ge#(0(x), 1(y)) → not#(ge(y, x))-#(0(x), 0(y)) → 0#(-(x, y))
eq#(0(x), 0(y)) → eq#(x, y)*#(*(x, y), z) → *#(x, *(y, z))
log'#(0(x)) → +#(log'(x), 1(#))+#(+(x, y), z) → +#(y, z)
*#(0(x), y) → 0#(*(x, y))prod#(cons(x, l)) → *#(x, prod(l))
sum#(cons(x, l)) → +#(x, sum(l))+#(+(x, y), z) → +#(x, +(y, z))
+#(0(x), 0(y)) → 0#(+(x, y))inter#(app(l1, l2), l3) → app#(inter(l1, l3), inter(l2, l3))
ifinter#(true, x, l1, l2) → inter#(l1, l2)inter#(cons(x, l1), l2) → mem#(x, l2)
*#(x, +(y, z)) → +#(*(x, y), *(x, z))log#(x) → log'#(x)
eq#(1(x), 1(y)) → eq#(x, y)ifinter#(false, x, l1, l2) → inter#(l1, l2)
*#(0(x), y) → *#(x, y)-#(1(x), 1(y)) → -#(x, y)
sum#(app(l1, l2)) → +#(sum(l1), sum(l2))+#(1(x), 1(y)) → 0#(+(+(x, y), 1(#)))
+#(0(x), 1(y)) → +#(x, y)-#(1(x), 0(y)) → -#(x, y)
inter#(app(l1, l2), l3) → inter#(l2, l3)-#(0(x), 1(y)) → -#(-(x, y), 1(#))
+#(1(x), 1(y)) → +#(+(x, y), 1(#))eq#(0(x), #) → eq#(x, #)
inter#(l1, app(l2, l3)) → app#(inter(l1, l2), inter(l1, l3))*#(1(x), y) → +#(0(*(x, y)), y)
prod#(app(l1, l2)) → *#(prod(l1), prod(l2))inter#(l1, app(l2, l3)) → inter#(l1, l3)
*#(x, +(y, z)) → *#(x, z)prod#(cons(x, l)) → prod#(l)
inter#(l1, cons(x, l2)) → mem#(x, l1)mem#(x, cons(y, l)) → mem#(x, l)
sum#(app(l1, l2)) → sum#(l1)prod#(app(l1, l2)) → prod#(l1)
inter#(l1, app(l2, l3)) → inter#(l1, l2)ge#(0(x), 0(y)) → ge#(x, y)
mem#(x, cons(y, l)) → eq#(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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

The following SCCs where found

log'#(1(x)) → log'#(x)log'#(0(x)) → log'#(x)
sum#(app(l1, l2)) → sum#(l1)sum#(cons(x, l)) → sum#(l)
sum#(app(l1, l2)) → sum#(l2)
eq#(0(x), 0(y)) → eq#(x, y)eq#(1(x), 1(y)) → eq#(x, y)
inter#(l1, app(l2, l3)) → inter#(l1, l3)inter#(l1, app(l2, l3)) → inter#(l1, l2)
ifinter#(true, x, l1, l2) → inter#(l1, l2)inter#(app(l1, l2), l3) → inter#(l2, l3)
inter#(l1, cons(x, l2)) → ifinter#(mem(x, l1), x, l2, l1)ifinter#(false, x, l1, l2) → inter#(l1, l2)
inter#(cons(x, l1), l2) → ifinter#(mem(x, l2), x, l1, l2)inter#(app(l1, l2), l3) → inter#(l1, l3)
+#(0(x), 1(y)) → +#(x, y)+#(0(x), 0(y)) → +#(x, y)
+#(+(x, y), z) → +#(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, z))
eq#(0(x), #) → eq#(x, #)
*#(x, +(y, z)) → *#(x, z)*#(1(x), y) → *#(x, y)
*#(*(x, y), z) → *#(x, *(y, z))*#(*(x, y), z) → *#(y, z)
*#(x, +(y, z)) → *#(x, y)*#(0(x), y) → *#(x, y)
-#(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)
eq#(#, 0(y)) → eq#(#, y)
app#(cons(x, l1), l2) → app#(l1, l2)
mem#(x, cons(y, l)) → mem#(x, l)
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)
prod#(cons(x, l)) → prod#(l)prod#(app(l1, l2)) → prod#(l1)
prod#(app(l1, l2)) → prod#(l2)
ge#(#, 0(x)) → ge#(#, x)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

eq#(#, 0(y)) → eq#(#, 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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

eq#(#, 0(y)) → eq#(#, y)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

sum#(app(l1, l2)) → sum#(l1)sum#(cons(x, l)) → sum#(l)
sum#(app(l1, l2)) → sum#(l2)

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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

sum#(app(l1, l2)) → sum#(l1)sum#(cons(x, l)) → sum#(l)
sum#(app(l1, l2)) → sum#(l2)

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

mem#(x, cons(y, l)) → mem#(x, l)

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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

mem#(x, cons(y, l)) → mem#(x, l)

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

*#(x, +(y, z)) → *#(x, z)*#(1(x), y) → *#(x, y)
*#(*(x, y), z) → *#(x, *(y, z))*#(*(x, y), z) → *#(y, z)
*#(x, +(y, z)) → *#(x, y)*#(0(x), 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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 16: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

*#(x, +(y, z)) → *#(x, 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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, prod, cons, nil, eq

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

log'#(1(x)) → log'#(x)log'#(0(x)) → log'#(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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

log'#(1(x)) → log'#(x)log'#(0(x)) → log'#(x)

Problem 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

eq#(0(x), #) → eq#(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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

eq#(0(x), #) → eq#(x, #)

Problem 8: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

eq#(0(x), 0(y)) → eq#(x, y)eq#(1(x), 1(y)) → eq#(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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 9: 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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 10: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

+#(0(x), 1(y)) → +#(x, y)+#(0(x), 0(y)) → +#(x, y)
+#(+(x, y), z) → +#(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, 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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Polynomial Interpretation

Improved Usable rules

+(+(x, y), z) → +(x, +(y, z))+(0(x), 0(y)) → 0(+(x, y))
+(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:

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

Problem 17: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

+#(0(x), 0(y)) → +#(x, y)+#(+(x, y), z) → +#(y, z)
+#(+(x, y), z) → +#(x, +(y, 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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, prod, cons, nil, eq

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)

Problem 21: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

+#(+(x, y), z) → +#(y, z)+#(+(x, y), z) → +#(x, +(y, 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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

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) → +#(y, z)+#(+(x, y), z) → +#(x, +(y, z))

Problem 11: 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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

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 18: 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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, prod, cons, nil, eq

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 12: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

inter#(l1, app(l2, l3)) → inter#(l1, l3)inter#(l1, app(l2, l3)) → inter#(l1, l2)
ifinter#(true, x, l1, l2) → inter#(l1, l2)inter#(app(l1, l2), l3) → inter#(l2, l3)
inter#(l1, cons(x, l2)) → ifinter#(mem(x, l1), x, l2, l1)ifinter#(false, x, l1, l2) → inter#(l1, l2)
inter#(cons(x, l1), l2) → ifinter#(mem(x, l2), x, l1, l2)inter#(app(l1, l2), l3) → inter#(l1, l3)

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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Polynomial Interpretation

Improved Usable rules

if(false, x, y) → ymem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))if(true, x, y) → x

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

ifinter#(false, x, l1, l2) → inter#(l1, l2)

Problem 19: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

inter#(l1, app(l2, l3)) → inter#(l1, l3)inter#(l1, app(l2, l3)) → inter#(l1, l2)
ifinter#(true, x, l1, l2) → inter#(l1, l2)inter#(l1, cons(x, l2)) → ifinter#(mem(x, l1), x, l2, l1)
inter#(app(l1, l2), l3) → inter#(l2, l3)inter#(app(l1, l2), l3) → inter#(l1, l3)
inter#(cons(x, l1), l2) → ifinter#(mem(x, l2), x, l1, l2)

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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, prod, cons, nil, eq

Strategy

Polynomial Interpretation

Improved Usable rules

if(false, x, y) → ymem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))if(true, x, y) → x

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

inter#(l1, app(l2, l3)) → inter#(l1, l3)inter#(l1, app(l2, l3)) → inter#(l1, l2)
inter#(app(l1, l2), l3) → inter#(l2, l3)inter#(app(l1, l2), l3) → inter#(l1, l3)

Problem 22: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

ifinter#(true, x, l1, l2) → inter#(l1, l2)inter#(l1, cons(x, l2)) → ifinter#(mem(x, l1), x, l2, l1)
inter#(cons(x, l1), l2) → ifinter#(mem(x, l2), x, l1, l2)

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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Polynomial Interpretation

Improved Usable rules

if(false, x, y) → ymem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))if(true, x, y) → x

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

inter#(cons(x, l1), l2) → ifinter#(mem(x, l2), x, l1, l2)

Problem 23: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

ifinter#(true, x, l1, l2) → inter#(l1, l2)inter#(l1, cons(x, l2)) → ifinter#(mem(x, l1), x, l2, l1)

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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, prod, cons, nil, eq

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:

inter#(l1, cons(x, l2)) → ifinter#(mem(x, l1), x, l2, l1)

Problem 24: DependencyGraph

Dependency Pair Problem

Dependency Pairs

ifinter#(true, x, l1, l2) → inter#(l1, l2)

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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

There are no SCCs!

Problem 13: 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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

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 20: 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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, prod, cons, nil, eq

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)-#(0(x), 1(y)) → -#(-(x, y), 1(#))
-#(1(x), 1(y)) → -#(x, y)

Problem 14: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

app#(cons(x, l1), l2) → app#(l1, l2)

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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

app#(cons(x, l1), l2) → app#(l1, l2)

Problem 15: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

prod#(cons(x, l)) → prod#(l)prod#(app(l1, l2)) → prod#(l1)
prod#(app(l1, l2)) → prod#(l2)

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(true) → falsenot(false) → true
if(true, x, y) → xif(false, x, y) → y
eq(#, #) → trueeq(#, 1(y)) → false
eq(1(x), #) → falseeq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → falseeq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, 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, #) → true
ge(#, 0(x)) → ge(#, x)ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))log'(#) → #
log'(1(x)) → +(log'(x), 1(#))log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))inter(x, nil) → nil
inter(nil, x) → nilinter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Original Signature

Termination of terms over the following signature is verified: app, #, log', *, sum, +, true, ge, log, -, inter, not, 1, 0, if, mem, false, ifinter, eq, nil, cons, prod

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

prod#(cons(x, l)) → prod#(l)prod#(app(l1, l2)) → prod#(l1)
prod#(app(l1, l2)) → prod#(l2)