Termination w.r.t. Q proof of /tmp/tmp2tC0DH/big.xml

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 AND

    ↳5 QDP

        ↳6 QDPOrderProof (⇔)

        ↳7 QDP

        ↳8 PisEmptyProof (⇔)

        ↳9 TRUE

    ↳10 QDP

        ↳11 QDPOrderProof (⇔)

        ↳12 QDP

        ↳13 PisEmptyProof (⇔)

        ↳14 TRUE

    ↳15 QDP

        ↳16 QDPOrderProof (⇔)

        ↳17 QDP

        ↳18 QDPOrderProof (⇔)

        ↳19 QDP

        ↳20 QDPOrderProof (⇔)

        ↳21 QDP

        ↳22 QDPOrderProof (⇔)

        ↳23 QDP

        ↳24 PisEmptyProof (⇔)

        ↳25 TRUE

    ↳26 QDP

        ↳27 QDPOrderProof (⇔)

        ↳28 QDP

        ↳29 PisEmptyProof (⇔)

        ↳30 TRUE

    ↳31 QDP

        ↳32 QDPOrderProof (⇔)

        ↳33 QDP

        ↳34 PisEmptyProof (⇔)

        ↳35 TRUE

    ↳36 QDP

        ↳37 QDPOrderProof (⇔)

        ↳38 QDP

        ↳39 QDPOrderProof (⇔)

        ↳40 QDP

        ↳41 PisEmptyProof (⇔)

        ↳42 TRUE

    ↳43 QDP

        ↳44 QDPOrderProof (⇔)

        ↳45 QDP

        ↳46 PisEmptyProof (⇔)

        ↳47 TRUE

    ↳48 QDP

        ↳49 QDPOrderProof (⇔)

        ↳50 QDP

        ↳51 QDPOrderProof (⇔)

        ↳52 QDP

        ↳53 QDPOrderProof (⇔)

        ↳54 QDP

        ↳55 QDPOrderProof (⇔)

        ↳56 QDP

        ↳57 PisEmptyProof (⇔)

        ↳58 TRUE

    ↳59 QDP

        ↳60 QDPOrderProof (⇔)

        ↳61 QDP

        ↳62 DependencyGraphProof (⇔)

        ↳63 AND

            ↳64 QDP

                ↳65 QDPOrderProof (⇔)

                ↳66 QDP

                ↳67 PisEmptyProof (⇔)

                ↳68 TRUE

            ↳69 QDP

                ↳70 QDPOrderProof (⇔)

                ↳71 QDP

                ↳72 QDPOrderProof (⇔)

                ↳73 QDP

                ↳74 PisEmptyProof (⇔)

                ↳75 TRUE

    ↳76 QDP

        ↳77 QDPOrderProof (⇔)

        ↳78 QDP

        ↳79 QDPOrderProof (⇔)

        ↳80 QDP

        ↳81 QDPOrderProof (⇔)

        ↳82 QDP

        ↳83 QDPOrderProof (⇔)

        ↳84 QDP

        ↳85 QDPOrderProof (⇔)

        ↳86 QDP

        ↳87 PisEmptyProof (⇔)

        ↳88 TRUE

    ↳89 QDP

        ↳90 QDPOrderProof (⇔)

        ↳91 QDP

        ↳92 QDPOrderProof (⇔)

        ↳93 QDP

        ↳94 PisEmptyProof (⇔)

        ↳95 TRUE

    ↳96 QDP

        ↳97 QDPOrderProof (⇔)

        ↳98 QDP

        ↳99 QDPOrderProof (⇔)

        ↳100 QDP

        ↳101 QDPOrderProof (⇔)

        ↳102 QDP

        ↳103 QDPOrderProof (⇔)

        ↳104 QDP

        ↳105 PisEmptyProof (⇔)

        ↳106 TRUE

    ↳107 QDP

        ↳108 QDPOrderProof (⇔)

        ↳109 QDP

        ↳110 QDPOrderProof (⇔)

        ↳111 QDP

        ↳112 PisEmptyProof (⇔)

        ↳113 TRUE

    ↳114 QDP

        ↳115 QDPOrderProof (⇔)

        ↳116 QDP

        ↳117 QDPOrderProof (⇔)

        ↳118 QDP

        ↳119 PisEmptyProof (⇔)

        ↳120 TRUE

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following 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)

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+¹(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)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 14 SCCs with 26 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP(cons(x, l1), l2) → APP(l1, l2)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

APP(cons(x, l1), l2) → APP(l1, l2)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
APP(x0, x1, x2) = APP(x0)

Tags:
APP has argument tags [3,1,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(9) TRUE

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(#, 0(x)) → GE(#, x)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

GE(#, 0(x)) → GE(#, x)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
GE(x0, x1, x2) = GE(x2)

Tags:
GE has argument tags [0,3,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(12) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(13) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(14) TRUE

(15) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(0(x), 1(y)) → GE(y, x)
GE(0(x), 0(y)) → GE(x, y)
GE(1(x), 0(y)) → GE(x, y)
GE(1(x), 1(y)) → GE(x, y)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(16) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

GE(1(x), 1(y)) → GE(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
GE(x0, x1, x2) = GE(x1, x2)

Tags:
GE has argument tags [1,1,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(17) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(0(x), 1(y)) → GE(y, x)
GE(0(x), 0(y)) → GE(x, y)
GE(1(x), 0(y)) → GE(x, y)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(18) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

GE(0(x), 1(y)) → GE(y, x)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
GE(x0, x1, x2) = GE(x1, x2)

Tags:
GE has argument tags [2,1,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(19) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(0(x), 0(y)) → GE(x, y)
GE(1(x), 0(y)) → GE(x, y)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(20) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

GE(0(x), 0(y)) → GE(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
GE(x0, x1, x2) = GE(x1)

Tags:
GE has argument tags [2,1,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(21) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(1(x), 0(y)) → GE(x, y)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(22) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

GE(1(x), 0(y)) → GE(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
GE(x0, x1, x2) = GE(x1)

Tags:
GE has argument tags [3,3,3] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(23) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(24) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(25) TRUE

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

EQ(0(x), #) → EQ(x, #)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(27) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

EQ(0(x), #) → EQ(x, #)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
EQ(x0, x1, x2) = EQ(x0, x1, x2)

Tags:
EQ has argument tags [1,1,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(28) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(29) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(30) TRUE

(31) Obligation:

Q DP problem:
The TRS P consists of the following rules:

EQ(#, 0(y)) → EQ(#, y)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(32) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

EQ(#, 0(y)) → EQ(#, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
EQ(x0, x1, x2) = EQ(x2)

Tags:
EQ has argument tags [0,3,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(33) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(34) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(35) TRUE

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

EQ(0(x), 0(y)) → EQ(x, y)
EQ(1(x), 1(y)) → EQ(x, y)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(37) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

EQ(0(x), 0(y)) → EQ(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
EQ(x0, x1, x2) = EQ(x1, x2)

Tags:
EQ has argument tags [3,0,3] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

EQ(1(x), 1(y)) → EQ(x, y)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(39) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

EQ(1(x), 1(y)) → EQ(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
EQ(x0, x1, x2) = EQ(x0, x1, x2)

Tags:
EQ has argument tags [2,3,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(40) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(41) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(42) TRUE

(43) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MEM(x, cons(y, l)) → MEM(x, l)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(44) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

MEM(x, cons(y, l)) → MEM(x, l)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
MEM(x0, x1, x2) = MEM(x0, x2)

Tags:
MEM has argument tags [3,2,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(45) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(46) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(47) TRUE

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(49) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

INTER(l1, cons(x, l2)) → IFINTER(mem(x, l1), x, l2, l1)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
INTER(x0, x1, x2) = INTER(x0, x1, x2)
IFINTER(x0, x1, x2, x3, x4) = IFINTER(x3, x4)

Tags:
INTER has argument tags [4,4,1] and root tag 0
IFINTER has argument tags [0,3,1,4,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were 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

(50) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INTER(app(l1, l2), l3) → INTER(l2, l3)
INTER(app(l1, l2), l3) → 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)
IFINTER(true, x, l1, l2) → INTER(l1, l2)
IFINTER(false, x, l1, l2) → INTER(l1, l2)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(51) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

INTER(l1, app(l2, l3)) → INTER(l1, l2)
INTER(l1, app(l2, l3)) → INTER(l1, l3)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
INTER(x0, x1, x2) = INTER(x0, x2)
IFINTER(x0, x1, x2, x3, x4) = IFINTER(x4)

Tags:
INTER has argument tags [6,0,6] and root tag 0
IFINTER has argument tags [0,3,6,7,6] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(52) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INTER(app(l1, l2), l3) → INTER(l2, l3)
INTER(app(l1, l2), l3) → INTER(l1, l3)
INTER(cons(x, l1), l2) → IFINTER(mem(x, l2), x, l1, l2)
IFINTER(true, x, l1, l2) → INTER(l1, l2)
IFINTER(false, x, l1, l2) → INTER(l1, l2)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(53) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

INTER(app(l1, l2), l3) → INTER(l2, l3)
INTER(app(l1, l2), l3) → INTER(l1, l3)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
INTER(x0, x1, x2) = INTER(x1)
IFINTER(x0, x1, x2, x3, x4) = IFINTER(x0, x1)

Tags:
INTER has argument tags [0,0,0] and root tag 0
IFINTER has argument tags [0,0,6,0,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(54) Obligation:

Q DP problem:
The TRS P consists of the following rules:

INTER(cons(x, l1), l2) → IFINTER(mem(x, l2), x, l1, l2)
IFINTER(true, x, l1, l2) → INTER(l1, l2)
IFINTER(false, x, l1, l2) → INTER(l1, l2)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(55) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

INTER(cons(x, l1), l2) → IFINTER(mem(x, l2), x, l1, l2)
IFINTER(true, x, l1, l2) → INTER(l1, l2)
IFINTER(false, x, l1, l2) → INTER(l1, l2)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
INTER(x0, x1, x2) = INTER(x0, x1)
IFINTER(x0, x1, x2, x3, x4) = IFINTER(x3)

Tags:
INTER has argument tags [0,0,0] and root tag 0
IFINTER has argument tags [5,0,4,0,1] and root tag 1

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(56) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(57) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(58) TRUE

(59) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(60) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
-¹(x0, x1, x2) = -¹(x0, x2)

Tags:
-¹ has argument tags [2,1,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(61) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(62) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.

(63) Complex Obligation (AND)

(64) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(65) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
-¹(x0, x1, x2) = -¹(x1)

Tags:
-¹ has argument tags [0,0,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(66) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(67) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(68) TRUE

(69) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(70) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
-¹(x0, x1, x2) = -¹(x0, x2)

Tags:
-¹ has argument tags [0,3,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(71) Obligation:

Q DP problem:
The TRS P consists of the following rules:

-¹(0(x), 0(y)) → -¹(x, y)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(72) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

-¹(0(x), 0(y)) → -¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
-¹(x0, x1, x2) = -¹(x0, x1, x2)

Tags:
-¹ has argument tags [2,3,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(73) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(74) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(75) TRUE

(76) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(77) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+¹(x0, x1, x2) = +¹(x0, x1, x2)

Tags:
+¹ has argument tags [1,2,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were 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(#) → #

(78) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(79) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+¹(x0, x1, x2) = +¹(x0, x1)

Tags:
+¹ has argument tags [1,2,3] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were 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(#) → #

(80) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(81) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+¹(x0, x1, x2) = +¹(x0, x1, x2)

Tags:
+¹ has argument tags [0,2,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were 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(#) → #

(82) Obligation:

Q DP problem:
The TRS P consists of the following rules:

+¹(0(x), 0(y)) → +¹(x, y)
+¹(+(x, y), z) → +¹(x, +(y, z))

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(83) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

+¹(0(x), 0(y)) → +¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+¹(x0, x1, x2) = +¹(x1)

Tags:
+¹ has argument tags [1,1,2] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(84) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(85) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
+¹(x0, x1, x2) = +¹(x1)

Tags:
+¹ has argument tags [1,1,3] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(86) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(87) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(88) TRUE

(89) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM(app(l1, l2)) → SUM(l1)
SUM(cons(x, l)) → SUM(l)
SUM(app(l1, l2)) → SUM(l2)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(90) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

SUM(cons(x, l)) → SUM(l)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
SUM(x0, x1) = SUM(x1)

Tags:
SUM has argument tags [1,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(91) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUM(app(l1, l2)) → SUM(l1)
SUM(app(l1, l2)) → SUM(l2)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(92) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

SUM(app(l1, l2)) → SUM(l1)
SUM(app(l1, l2)) → SUM(l2)

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

The following usable rules [FROCOS05] were oriented: none

(93) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(94) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(95) TRUE

(96) Obligation:

Q DP problem:
The TRS P consists of the following rules:

*¹(1(x), y) → *¹(x, y)
*¹(0(x), y) → *¹(x, y)
*¹(*(x, y), z) → *¹(x, *(y, z))
*¹(*(x, y), z) → *¹(y, z)
*¹(x, +(y, z)) → *¹(x, y)
*¹(x, +(y, z)) → *¹(x, z)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(97) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

*¹(0(x), y) → *¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
*¹(x0, x1, x2) = *¹(x1)

Tags:
*¹ has argument tags [0,2,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(98) Obligation:

Q DP problem:
The TRS P consists of the following rules:

*¹(1(x), y) → *¹(x, y)
*¹(*(x, y), z) → *¹(x, *(y, z))
*¹(*(x, y), z) → *¹(y, z)
*¹(x, +(y, z)) → *¹(x, y)
*¹(x, +(y, z)) → *¹(x, z)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(99) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

*¹(1(x), y) → *¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
*¹(x0, x1, x2) = *¹(x0)

Tags:
*¹ has argument tags [0,0,3] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(100) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(101) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

*¹(*(x, y), z) → *¹(x, *(y, z))
*¹(*(x, y), z) → *¹(y, z)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
*¹(x0, x1, x2) = *¹(x1)

Tags:
*¹ has argument tags [0,0,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(102) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(103) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
*¹(x0, x1, x2) = *¹(x0)

Tags:
*¹ has argument tags [1,1,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(104) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(105) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(106) TRUE

(107) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PROD(app(l1, l2)) → PROD(l1)
PROD(cons(x, l)) → PROD(l)
PROD(app(l1, l2)) → PROD(l2)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(108) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PROD(cons(x, l)) → PROD(l)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
PROD(x0, x1) = PROD(x1)

Tags:
PROD has argument tags [1,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(109) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PROD(app(l1, l2)) → PROD(l1)
PROD(app(l1, l2)) → PROD(l2)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(110) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PROD(app(l1, l2)) → PROD(l1)
PROD(app(l1, l2)) → PROD(l2)

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

The following usable rules [FROCOS05] were oriented: none

(111) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(112) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(113) TRUE

(114) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOG'(0(x)) → LOG'(x)
LOG'(1(x)) → LOG'(x)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(115) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

LOG'(0(x)) → LOG'(x)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
LOG'(x0, x1) = LOG'(x1)

Tags:
LOG' has argument tags [0,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(116) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOG'(1(x)) → LOG'(x)

The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(117) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

LOG'(1(x)) → LOG'(x)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
LOG'(x0, x1) = LOG'(x1)

Tags:
LOG' has argument tags [1,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(118) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following 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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(119) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.