Termination Proof using AProVE

Term Rewriting System R:
[x, y, z, l, l1, l2, l3]
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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

+'(0(x), 0(y)) -> 0'(+(x, y))
+'(0(x), 0(y)) -> +'(x, y)
+'(0(x), 1(y)) -> +'(x, y)
+'(1(x), 0(y)) -> +'(x, y)
+'(1(x), 1(y)) -> 0'(+(+(x, y), 1(#)))
+'(1(x), 1(y)) -> +'(+(x, y), 1(#))
+'(1(x), 1(y)) -> +'(x, y)
+'(+(x, y), z) -> +'(x, +(y, z))
+'(+(x, y), z) -> +'(y, z)
-'(0(x), 0(y)) -> 0'(-(x, y))
-'(0(x), 0(y)) -> -'(x, y)
-'(0(x), 1(y)) -> -'(-(x, y), 1(#))
-'(0(x), 1(y)) -> -'(x, y)
-'(1(x), 0(y)) -> -'(x, y)
-'(1(x), 1(y)) -> 0'(-(x, y))
-'(1(x), 1(y)) -> -'(x, y)
EQ(#, 0(y)) -> EQ(#, y)
EQ(0(x), #) -> EQ(x, #)
EQ(1(x), 1(y)) -> EQ(x, y)
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(0(x), 1(y)) -> GE(y, x)
GE(1(x), 0(y)) -> GE(x, y)
GE(1(x), 1(y)) -> GE(x, y)
GE(#, 0(x)) -> GE(#, x)
LOG(x) -> -'(log'(x), 1(#))
LOG(x) -> LOG'(x)
LOG'(1(x)) -> +'(log'(x), 1(#))
LOG'(1(x)) -> LOG'(x)
LOG'(0(x)) -> IF(ge(x, 1(#)), +(log'(x), 1(#)), #)
LOG'(0(x)) -> GE(x, 1(#))
LOG'(0(x)) -> +'(log'(x), 1(#))
LOG'(0(x)) -> LOG'(x)
*'(0(x), y) -> 0'(*(x, y))
*'(0(x), y) -> *'(x, y)
*'(1(x), y) -> +'(0(*(x, y)), y)
*'(1(x), y) -> 0'(*(x, y))
*'(1(x), y) -> *'(x, y)
*'(*(x, y), z) -> *'(x, *(y, z))
*'(*(x, y), z) -> *'(y, z)
*'(x, +(y, z)) -> +'(*(x, y), *(x, z))
*'(x, +(y, z)) -> *'(x, y)
*'(x, +(y, z)) -> *'(x, z)
APP(cons(x, l1), l2) -> APP(l1, l2)
SUM(nil) -> 0'(#)
SUM(cons(x, l)) -> +'(x, sum(l))
SUM(cons(x, l)) -> SUM(l)
SUM(app(l1, l2)) -> +'(sum(l1), sum(l2))
SUM(app(l1, l2)) -> SUM(l1)
SUM(app(l1, l2)) -> SUM(l2)
PROD(cons(x, l)) -> *'(x, prod(l))
PROD(cons(x, l)) -> PROD(l)
PROD(app(l1, l2)) -> *'(prod(l1), prod(l2))
PROD(app(l1, l2)) -> PROD(l1)
PROD(app(l1, l2)) -> PROD(l2)
MEM(x, cons(y, l)) -> IF(eq(x, y), true, mem(x, l))
MEM(x, cons(y, l)) -> EQ(x, y)
MEM(x, cons(y, l)) -> MEM(x, l)
INTER(app(l1, l2), l3) -> APP(inter(l1, l3), inter(l2, l3))
INTER(app(l1, l2), l3) -> INTER(l1, l3)
INTER(app(l1, l2), l3) -> INTER(l2, l3)
INTER(l1, app(l2, l3)) -> APP(inter(l1, l2), inter(l1, l3))
INTER(l1, app(l2, l3)) -> INTER(l1, l2)
INTER(l1, app(l2, l3)) -> INTER(l1, l3)
INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2)
INTER(cons(x, l1), l2) -> MEM(x, l2)
INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1)
INTER(l1, cons(x, l2)) -> MEM(x, l1)
IFINTER(true, x, l1, l2) -> INTER(l1, l2)
IFINTER(false, x, l1, l2) -> INTER(l1, l2)

Furthermore, R contains 14 SCCs.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pairs:

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

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pairs can be strictly oriented:

+'(1(x), 1(y)) -> +'(x, y)
+'(1(x), 1(y)) -> +'(+(x, y), 1(#))
+'(1(x), 0(y)) -> +'(x, y)
+'(0(x), 1(y)) -> +'(x, y)

The following usable rules w.r.t. to the AFS can be oriented:

+(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))
0(#) -> #

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(#) = 0

POL(0(x₁)) = x₁

POL(1(x₁)) = 1 + x₁

POL(+(x₁, x₂)) = x₁ + x₂

POL(+'(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

+'(x₁, x₂) -> +'(x₁, x₂)
1(x₁) -> 1(x₁)
0(x₁) -> 0(x₁)
+(x₁, x₂) -> +(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 15

             ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pairs:

+'(+(x, y), z) -> +'(y, z)
+'(+(x, y), z) -> +'(x, +(y, z))
+'(0(x), 0(y)) -> +'(x, y)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

+'(0(x), 0(y)) -> +'(x, y)

The following usable rules w.r.t. to the AFS can be oriented:

+(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))
0(#) -> #

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(#) = 0

POL(0(x₁)) = 1 + x₁

POL(1(x₁)) = 1 + x₁

POL(+(x₁, x₂)) = x₁ + x₂

POL(+'(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

+'(x₁, x₂) -> +'(x₁, x₂)
0(x₁) -> 0(x₁)
+(x₁, x₂) -> +(x₁, x₂)
1(x₁) -> 1(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 15

             ↳AFS

...

               →DP Problem 16

                 ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pairs:

+'(+(x, y), z) -> +'(y, z)
+'(+(x, y), z) -> +'(x, +(y, z))

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

+'(+(x, y), z) -> +'(y, z)

The following usable rules w.r.t. to the AFS can be oriented:

+(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))
0(#) -> #

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(#) = 0

POL(0(x₁)) = x₁

POL(1(x₁)) = 1 + x₁

POL(+(x₁, x₂)) = 1 + x₁ + x₂

POL(+'(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

+'(x₁, x₂) -> +'(x₁, x₂)
+(x₁, x₂) -> +(x₁, x₂)
0(x₁) -> 0(x₁)
1(x₁) -> 1(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 15

             ↳AFS

...

               →DP Problem 17

                 ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

+'(+(x, y), z) -> +'(x, +(y, z))

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

+'(+(x, y), z) -> +'(x, +(y, z))

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(+(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

+'(x₁, x₂) -> x₁
+(x₁, x₂) -> +(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 15

             ↳AFS

...

               →DP Problem 18

                 ↳Dependency Graph

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Argument Filtering and Ordering

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pairs:

-'(1(x), 1(y)) -> -'(x, y)
-'(1(x), 0(y)) -> -'(x, y)
-'(0(x), 1(y)) -> -'(x, y)
-'(0(x), 1(y)) -> -'(-(x, y), 1(#))
-'(0(x), 0(y)) -> -'(x, y)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pairs can be strictly oriented:

-'(1(x), 1(y)) -> -'(x, y)
-'(1(x), 0(y)) -> -'(x, y)
-'(0(x), 1(y)) -> -'(x, y)
-'(0(x), 1(y)) -> -'(-(x, y), 1(#))
-'(0(x), 0(y)) -> -'(x, y)

The following usable rules w.r.t. to the AFS can be oriented:

-(#, 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))
0(#) -> #

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(#) = 0

POL(-'(x₁, x₂)) = 1 + x₁ + x₂

POL(0(x₁)) = 1 + x₁

POL(1(x₁)) = 1 + x₁

POL(-(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

-'(x₁, x₂) -> -'(x₁, x₂)
0(x₁) -> 0(x₁)
1(x₁) -> 1(x₁)
-(x₁, x₂) -> -(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 19

             ↳Dependency Graph

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Argument Filtering and Ordering

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

EQ(#, 0(y)) -> EQ(#, y)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

EQ(#, 0(y)) -> EQ(#, y)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(#) = 0

POL(EQ(x₁, x₂)) = x₁ + x₂

POL(0(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

EQ(x₁, x₂) -> EQ(x₁, x₂)
0(x₁) -> 0(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 20

             ↳Dependency Graph

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳Argument Filtering and Ordering

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

EQ(0(x), #) -> EQ(x, #)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

EQ(0(x), #) -> EQ(x, #)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(#) = 0

POL(EQ(x₁, x₂)) = x₁ + x₂

POL(0(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

EQ(x₁, x₂) -> EQ(x₁, x₂)
0(x₁) -> 0(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

           →DP Problem 21

             ↳Dependency Graph

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳Argument Filtering and Ordering

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

GE(#, 0(x)) -> GE(#, x)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

GE(#, 0(x)) -> GE(#, x)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(#) = 0

POL(0(x₁)) = 1 + x₁

POL(GE(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

GE(x₁, x₂) -> GE(x₁, x₂)
0(x₁) -> 0(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

           →DP Problem 22

             ↳Dependency Graph

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳Argument Filtering and Ordering

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

APP(cons(x, l1), l2) -> APP(l1, l2)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

APP(cons(x, l1), l2) -> APP(l1, l2)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(cons(x₁, x₂)) = 1 + x₁ + x₂

POL(APP(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

APP(x₁, x₂) -> APP(x₁, x₂)
cons(x₁, x₂) -> cons(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

           →DP Problem 23

             ↳Dependency Graph

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Argument Filtering and Ordering

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pairs:

*'(x, +(y, z)) -> *'(x, z)
*'(x, +(y, z)) -> *'(x, y)
*'(*(x, y), z) -> *'(y, z)
*'(*(x, y), z) -> *'(x, *(y, z))
*'(1(x), y) -> *'(x, y)
*'(0(x), y) -> *'(x, y)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pairs can be strictly oriented:

*'(*(x, y), z) -> *'(y, z)
*'(*(x, y), z) -> *'(x, *(y, z))

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0(x₁)) = x₁

POL(1(x₁)) = x₁

POL(*(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

*'(x₁, x₂) -> x₁
*(x₁, x₂) -> *(x₁, x₂)
0(x₁) -> 0(x₁)
1(x₁) -> 1(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

           →DP Problem 24

             ↳Argument Filtering and Ordering

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pairs:

*'(x, +(y, z)) -> *'(x, z)
*'(x, +(y, z)) -> *'(x, y)
*'(1(x), y) -> *'(x, y)
*'(0(x), y) -> *'(x, y)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pairs can be strictly oriented:

*'(x, +(y, z)) -> *'(x, z)
*'(x, +(y, z)) -> *'(x, y)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0(x₁)) = x₁

POL(*'(x₁, x₂)) = x₁ + x₂

POL(1(x₁)) = x₁

POL(+(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

*'(x₁, x₂) -> *'(x₁, x₂)
+(x₁, x₂) -> +(x₁, x₂)
0(x₁) -> 0(x₁)
1(x₁) -> 1(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

           →DP Problem 24

             ↳AFS

...

               →DP Problem 25

                 ↳Argument Filtering and Ordering

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pairs:

*'(1(x), y) -> *'(x, y)
*'(0(x), y) -> *'(x, y)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

*'(0(x), y) -> *'(x, y)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0(x₁)) = 1 + x₁

POL(*'(x₁, x₂)) = x₁ + x₂

POL(1(x₁)) = x₁

resulting in one new DP problem.
Used Argument Filtering System:

*'(x₁, x₂) -> *'(x₁, x₂)
0(x₁) -> 0(x₁)
1(x₁) -> 1(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

           →DP Problem 24

             ↳AFS

...

               →DP Problem 26

                 ↳Argument Filtering and Ordering

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

*'(1(x), y) -> *'(x, y)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

*'(1(x), y) -> *'(x, y)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(*'(x₁, x₂)) = x₁ + x₂

POL(1(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

*'(x₁, x₂) -> *'(x₁, x₂)
1(x₁) -> 1(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

           →DP Problem 24

             ↳AFS

...

               →DP Problem 27

                 ↳Dependency Graph

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳Argument Filtering and Ordering

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pairs:

SUM(app(l1, l2)) -> SUM(l2)
SUM(app(l1, l2)) -> SUM(l1)
SUM(cons(x, l)) -> SUM(l)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pairs can be strictly oriented:

SUM(app(l1, l2)) -> SUM(l2)
SUM(app(l1, l2)) -> SUM(l1)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(SUM(x₁)) = x₁

POL(cons(x₁, x₂)) = x₁ + x₂

POL(app(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

SUM(x₁) -> SUM(x₁)
app(x₁, x₂) -> app(x₁, x₂)
cons(x₁, x₂) -> cons(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

           →DP Problem 28

             ↳Argument Filtering and Ordering

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

SUM(cons(x, l)) -> SUM(l)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

SUM(cons(x, l)) -> SUM(l)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(SUM(x₁)) = x₁

POL(cons(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

SUM(x₁) -> SUM(x₁)
cons(x₁, x₂) -> cons(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

           →DP Problem 28

             ↳AFS

...

               →DP Problem 29

                 ↳Dependency Graph

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳Argument Filtering and Ordering

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pairs:

EQ(0(x), 0(y)) -> EQ(x, y)
EQ(1(x), 1(y)) -> EQ(x, y)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

EQ(0(x), 0(y)) -> EQ(x, y)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(EQ(x₁, x₂)) = x₁ + x₂

POL(0(x₁)) = 1 + x₁

POL(1(x₁)) = x₁

resulting in one new DP problem.
Used Argument Filtering System:

EQ(x₁, x₂) -> EQ(x₁, x₂)
0(x₁) -> 0(x₁)
1(x₁) -> 1(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

           →DP Problem 30

             ↳Argument Filtering and Ordering

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

EQ(1(x), 1(y)) -> EQ(x, y)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

EQ(1(x), 1(y)) -> EQ(x, y)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(EQ(x₁, x₂)) = x₁ + x₂

POL(1(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

EQ(x₁, x₂) -> EQ(x₁, x₂)
1(x₁) -> 1(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

           →DP Problem 30

             ↳AFS

...

               →DP Problem 31

                 ↳Dependency Graph

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳Argument Filtering and Ordering

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pairs:

GE(1(x), 1(y)) -> GE(x, y)
GE(1(x), 0(y)) -> GE(x, y)
GE(0(x), 1(y)) -> GE(y, x)
GE(0(x), 0(y)) -> GE(x, y)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pairs can be strictly oriented:

GE(1(x), 1(y)) -> GE(x, y)
GE(1(x), 0(y)) -> GE(x, y)
GE(0(x), 1(y)) -> GE(y, x)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0(x₁)) = x₁

POL(GE(x₁, x₂)) = 1 + x₁ + x₂

POL(1(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

GE(x₁, x₂) -> GE(x₁, x₂)
1(x₁) -> 1(x₁)
0(x₁) -> 0(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

           →DP Problem 32

             ↳Argument Filtering and Ordering

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

GE(0(x), 0(y)) -> GE(x, y)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

GE(0(x), 0(y)) -> GE(x, y)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0(x₁)) = 1 + x₁

POL(GE(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

GE(x₁, x₂) -> GE(x₁, x₂)
0(x₁) -> 0(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

           →DP Problem 32

             ↳AFS

...

               →DP Problem 33

                 ↳Dependency Graph

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳Argument Filtering and Ordering

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pairs:

PROD(app(l1, l2)) -> PROD(l2)
PROD(app(l1, l2)) -> PROD(l1)
PROD(cons(x, l)) -> PROD(l)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

PROD(cons(x, l)) -> PROD(l)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(cons(x₁, x₂)) = 1 + x₁ + x₂

POL(app(x₁, x₂)) = x₁ + x₂

POL(PROD(x₁)) = x₁

resulting in one new DP problem.
Used Argument Filtering System:

PROD(x₁) -> PROD(x₁)
cons(x₁, x₂) -> cons(x₁, x₂)
app(x₁, x₂) -> app(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

           →DP Problem 34

             ↳Argument Filtering and Ordering

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pairs:

PROD(app(l1, l2)) -> PROD(l2)
PROD(app(l1, l2)) -> PROD(l1)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pairs can be strictly oriented:

PROD(app(l1, l2)) -> PROD(l2)
PROD(app(l1, l2)) -> PROD(l1)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(app(x₁, x₂)) = 1 + x₁ + x₂

POL(PROD(x₁)) = x₁

resulting in one new DP problem.
Used Argument Filtering System:

PROD(x₁) -> PROD(x₁)
app(x₁, x₂) -> app(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

           →DP Problem 34

             ↳AFS

...

               →DP Problem 35

                 ↳Dependency Graph

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳Argument Filtering and Ordering

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

MEM(x, cons(y, l)) -> MEM(x, l)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

MEM(x, cons(y, l)) -> MEM(x, l)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(MEM(x₁, x₂)) = x₁ + x₂

POL(cons(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

MEM(x₁, x₂) -> MEM(x₁, x₂)
cons(x₁, x₂) -> cons(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

           →DP Problem 36

             ↳Dependency Graph

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳Argument Filtering and Ordering

       →DP Problem 14

         ↳AFS

Dependency Pairs:

LOG'(0(x)) -> LOG'(x)
LOG'(1(x)) -> LOG'(x)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

LOG'(0(x)) -> LOG'(x)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(LOG'(x₁)) = x₁

POL(0(x₁)) = 1 + x₁

POL(1(x₁)) = x₁

resulting in one new DP problem.
Used Argument Filtering System:

LOG'(x₁) -> LOG'(x₁)
0(x₁) -> 0(x₁)
1(x₁) -> 1(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

           →DP Problem 37

             ↳Argument Filtering and Ordering

       →DP Problem 14

         ↳AFS

Dependency Pair:

LOG'(1(x)) -> LOG'(x)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pair can be strictly oriented:

LOG'(1(x)) -> LOG'(x)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(LOG'(x₁)) = x₁

POL(1(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

LOG'(x₁) -> LOG'(x₁)
1(x₁) -> 1(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

           →DP Problem 37

             ↳AFS

...

               →DP Problem 38

                 ↳Dependency Graph

       →DP Problem 14

         ↳AFS

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳Argument Filtering and Ordering

Dependency Pairs:

IFINTER(false, x, l1, l2) -> INTER(l1, l2)
INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1)
IFINTER(true, x, l1, l2) -> INTER(l1, l2)
INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2)
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)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pairs can be strictly oriented:

IFINTER(false, x, l1, l2) -> INTER(l1, l2)
IFINTER(true, x, l1, l2) -> INTER(l1, l2)

The following usable rules w.r.t. to the AFS can be oriented:

mem(x, nil) -> false
mem(x, cons(y, l)) -> if(eq(x, y), true, mem(x, l))
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(1(x), 0(y)) -> false
eq(0(x), 0(y)) -> eq(x, y)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(if(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(mem) = 0

POL(eq) = 0

POL(false) = 0

POL(cons(x₁, x₂)) = 1 + x₁ + x₂

POL(true) = 0

POL(IFINTER(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₃ + x₄

POL(INTER(x₁, x₂)) = x₁ + x₂

POL(app(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

IFINTER(x₁, x₂, x₃, x₄) -> IFINTER(x₁, x₂, x₃, x₄)
INTER(x₁, x₂) -> INTER(x₁, x₂)
app(x₁, x₂) -> app(x₁, x₂)
cons(x₁, x₂) -> cons(x₁, x₂)
mem(x₁, x₂) -> mem
if(x₁, x₂, x₃) -> if(x₁, x₂, x₃)
eq(x₁, x₂) -> eq

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

           →DP Problem 39

             ↳Dependency Graph

Dependency Pairs:

INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1)
INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2)
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)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

           →DP Problem 39

             ↳DGraph

...

               →DP Problem 40

                 ↳Argument Filtering and Ordering

Dependency Pairs:

INTER(l1, app(l2, l3)) -> INTER(l1, l2)
INTER(app(l1, l2), l3) -> INTER(l2, l3)
INTER(app(l1, l2), l3) -> INTER(l1, l3)
INTER(l1, app(l2, l3)) -> INTER(l1, l3)

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

The following dependency pairs can be strictly oriented:

INTER(l1, app(l2, l3)) -> INTER(l1, l2)
INTER(app(l1, l2), l3) -> INTER(l2, l3)
INTER(app(l1, l2), l3) -> INTER(l1, l3)
INTER(l1, app(l2, l3)) -> INTER(l1, l3)

There are no usable rules w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(INTER(x₁, x₂)) = x₁ + x₂

POL(app(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

INTER(x₁, x₂) -> INTER(x₁, x₂)
app(x₁, x₂) -> app(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳AFS

       →DP Problem 8

         ↳AFS

       →DP Problem 9

         ↳AFS

       →DP Problem 10

         ↳AFS

       →DP Problem 11

         ↳AFS

       →DP Problem 12

         ↳AFS

       →DP Problem 13

         ↳AFS

       →DP Problem 14

         ↳AFS

           →DP Problem 39

             ↳DGraph

...

               →DP Problem 41

                 ↳Dependency Graph

Dependency Pair:

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) -> false
not(false) -> true
if(true, x, y) -> x
if(false, x, y) -> y
eq(#, #) -> true
eq(#, 1(y)) -> false
eq(1(x), #) -> false
eq(#, 0(y)) -> eq(#, y)
eq(0(x), #) -> eq(x, #)
eq(1(x), 1(y)) -> eq(x, y)
eq(0(x), 1(y)) -> false
eq(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) -> nil
inter(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)

Using the Dependency Graph resulted in no new DP problems.

Termination of R successfully shown.
Duration:
0:01 minutes

POL(#)	= 0
POL(0(x₁))	= x₁
POL(1(x₁))	= 1 + x₁
POL(+(x₁, x₂))	= x₁ + x₂
POL(+'(x₁, x₂))	= 1 + x₁ + x₂

POL(#)	= 0
POL(-'(x₁, x₂))	= 1 + x₁ + x₂
POL(0(x₁))	= 1 + x₁
POL(1(x₁))	= 1 + x₁
POL(-(x₁, x₂))	= x₁ + x₂

POL(#)	= 0
POL(EQ(x₁, x₂))	= x₁ + x₂
POL(0(x₁))	= 1 + x₁

POL(cons(x₁, x₂))	= 1 + x₁ + x₂
POL(APP(x₁, x₂))	= x₁ + x₂

POL(0(x₁))	= x₁
POL(*'(x₁, x₂))	= x₁ + x₂
POL(1(x₁))	= x₁
POL(+(x₁, x₂))	= 1 + x₁ + x₂

POL(SUM(x₁))	= x₁
POL(cons(x₁, x₂))	= x₁ + x₂
POL(app(x₁, x₂))	= 1 + x₁ + x₂

POL(0(x₁))	= x₁
POL(GE(x₁, x₂))	= 1 + x₁ + x₂
POL(1(x₁))	= 1 + x₁

POL(app(x₁, x₂))	= 1 + x₁ + x₂
POL(PROD(x₁))	= x₁

POL(MEM(x₁, x₂))	= x₁ + x₂
POL(cons(x₁, x₂))	= 1 + x₁ + x₂

POL(LOG'(x₁))	= x₁
POL(0(x₁))	= 1 + x₁
POL(1(x₁))	= x₁

POL(if(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(mem)	= 0
POL(eq)	= 0
POL(false)	= 0
POL(cons(x₁, x₂))	= 1 + x₁ + x₂
POL(true)	= 0
POL(IFINTER(x₁, x₂, x₃, x₄))	= 1 + x₁ + x₂ + x₃ + x₄
POL(INTER(x₁, x₂))	= x₁ + x₂
POL(app(x₁, x₂))	= x₁ + x₂