Termination Proof using AProVE

Term Rewriting System R:
[x, y, l, l1, l2, l3]
if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

EQ(s(x), s(y)) -> EQ(x, y)
APP(cons(x, l1), l2) -> APP(l1, l2)
APP(app(l1, l2), l3) -> APP(l1, app(l2, l3))
APP(app(l1, l2), l3) -> APP(l2, l3)
MEM(x, cons(y, l)) -> IFMEM(eq(x, y), x, l)
MEM(x, cons(y, l)) -> EQ(x, y)
IFMEM(false, x, l) -> MEM(x, l)
INTER(app(l1, l2), l3) -> APP(inter(l1, l3), inter(l2, l3))
INTER(app(l1, l2), l3) -> INTER(l1, l3)
INTER(app(l1, l2), l3) -> INTER(l2, l3)
INTER(l1, app(l2, l3)) -> APP(inter(l1, l2), inter(l1, l3))
INTER(l1, app(l2, l3)) -> INTER(l1, l2)
INTER(l1, app(l2, l3)) -> INTER(l1, l3)
INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2)
INTER(cons(x, l1), l2) -> MEM(x, l2)
INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1)
INTER(l1, cons(x, l2)) -> MEM(x, l1)
IFINTER(true, x, l1, l2) -> INTER(l1, l2)
IFINTER(false, x, l1, l2) -> INTER(l1, l2)

Furthermore, R contains four SCCs.

     ↳DPs

       →DP Problem 1

         ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pair:

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

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

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

one new Dependency Pair is created:

EQ(s(s(x'')), s(s(y''))) -> EQ(s(x''), s(y''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 5

             ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pair:

EQ(s(s(x'')), s(s(y''))) -> EQ(s(x''), s(y''))

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

EQ(s(s(x'')), s(s(y''))) -> EQ(s(x''), s(y''))

one new Dependency Pair is created:

EQ(s(s(s(x''''))), s(s(s(y'''')))) -> EQ(s(s(x'''')), s(s(y'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 5

             ↳FwdInst

...

               →DP Problem 6

                 ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pair:

EQ(s(s(s(x''''))), s(s(s(y'''')))) -> EQ(s(s(x'''')), s(s(y'''')))

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

The following dependency pair can be strictly oriented:

EQ(s(s(s(x''''))), s(s(s(y'''')))) -> EQ(s(s(x'''')), s(s(y'''')))

There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

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

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 5

             ↳FwdInst

...

               →DP Problem 7

                 ↳Dependency Graph

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pair:

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

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

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

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

two new Dependency Pairs are created:

APP(cons(x, cons(x'', l1'')), l2'') -> APP(cons(x'', l1''), l2'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 8

             ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x'', l1'')), l2'') -> APP(cons(x'', l1''), l2'')
APP(app(l1, l2), l3) -> APP(l2, l3)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

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

three new Dependency Pairs are created:

APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(app(l1, cons(x'', cons(x'''', l1''''))), l3') -> APP(cons(x'', cons(x'''', l1'''')), l3')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 8

             ↳FwdInst

...

               →DP Problem 9

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(cons(x, cons(x'', l1'')), l2'') -> APP(cons(x'', l1''), l2'')
APP(app(l1, cons(x'', cons(x'''', l1''''))), l3') -> APP(cons(x'', cons(x'''', l1'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

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

two new Dependency Pairs are created:

APP(cons(x, cons(x'''', cons(x''''', l1''''))), l2'''') -> APP(cons(x'''', cons(x''''', l1'''')), l2'''')
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 8

             ↳FwdInst

...

               →DP Problem 10

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(cons(x, cons(x'''', cons(x''''', l1''''))), l2'''') -> APP(cons(x'''', cons(x''''', l1'''')), l2'''')
APP(app(l1, cons(x'', cons(x'''', l1''''))), l3') -> APP(cons(x'', cons(x'''', l1'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(app(l1, cons(x'', cons(x'''', l1''''))), l3') -> APP(cons(x'', cons(x'''', l1'''')), l3')

two new Dependency Pairs are created:

APP(app(l1, cons(x''', cons(x''''', cons(x'''''''', l1'''''')))), l3'') -> APP(cons(x''', cons(x''''', cons(x'''''''', l1''''''))), l3'')
APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(l1'''''', l2''''''))), l3'')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 8

             ↳FwdInst

...

               →DP Problem 11

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(l1'''''', l2''''''))), l3'')
APP(cons(x, cons(x'''', cons(x''''', l1''''))), l2'''') -> APP(cons(x'''', cons(x''''', l1'''')), l2'''')
APP(app(l1, cons(x''', cons(x''''', cons(x'''''''', l1'''''')))), l3'') -> APP(cons(x''', cons(x''''', cons(x'''''''', l1''''''))), l3'')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

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

two new Dependency Pairs are created:

APP(cons(x, cons(x''''0, cons(x'''''0, cons(x'''''''', l1'''''')))), l2'''''') -> APP(cons(x''''0, cons(x'''''0, cons(x'''''''', l1''''''))), l2'''''')
APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 8

             ↳FwdInst

...

               →DP Problem 12

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)
APP(cons(x, cons(x''''0, cons(x'''''0, cons(x'''''''', l1'''''')))), l2'''''') -> APP(cons(x''''0, cons(x'''''0, cons(x'''''''', l1''''''))), l2'''''')
APP(app(l1, cons(x''', cons(x''''', cons(x'''''''', l1'''''')))), l3'') -> APP(cons(x''', cons(x''''', cons(x'''''''', l1''''''))), l3'')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(l1'''''', l2''''''))), l3'')

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(app(l1, cons(x''', cons(x''''', cons(x'''''''', l1'''''')))), l3'') -> APP(cons(x''', cons(x''''', cons(x'''''''', l1''''''))), l3'')

two new Dependency Pairs are created:

APP(app(l1, cons(x'''', cons(x'''''', cons(x'''''''''', cons(x''''''''''', l1''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x'''''''''', cons(x''''''''''', l1'''''''')))), l3''')
APP(app(l1, cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2'''''''')))), l3''')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 8

             ↳FwdInst

...

               →DP Problem 13

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

APP(app(l1, cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2'''''''')))), l3''')
APP(cons(x, cons(x''''0, cons(x'''''0, cons(x'''''''', l1'''''')))), l2'''''') -> APP(cons(x''''0, cons(x'''''0, cons(x'''''''', l1''''''))), l2'''''')
APP(app(l1, cons(x'''', cons(x'''''', cons(x'''''''''', cons(x''''''''''', l1''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x'''''''''', cons(x''''''''''', l1'''''''')))), l3''')
APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(l1'''''', l2''''''))), l3'')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

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

two new Dependency Pairs are created:

APP(cons(x, cons(x''''0'', cons(x'''''0'', cons(x'''''''''', cons(x''''''''''', l1''''''''))))), l2'''''''') -> APP(cons(x''''0'', cons(x'''''0'', cons(x'''''''''', cons(x''''''''''', l1'''''''')))), l2'''''''')
APP(cons(x, cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2''''''''))))), l2''''''0) -> APP(cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2'''''''')))), l2''''''0)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 8

             ↳FwdInst

...

               →DP Problem 14

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

APP(cons(x, cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2''''''''))))), l2''''''0) -> APP(cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2'''''''')))), l2''''''0)
APP(cons(x, cons(x''''0'', cons(x'''''0'', cons(x'''''''''', cons(x''''''''''', l1''''''''))))), l2'''''''') -> APP(cons(x''''0'', cons(x'''''0'', cons(x'''''''''', cons(x''''''''''', l1'''''''')))), l2'''''''')
APP(app(l1, cons(x'''', cons(x'''''', cons(x'''''''''', cons(x''''''''''', l1''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x'''''''''', cons(x''''''''''', l1'''''''')))), l3''')
APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(l1'''''', l2''''''))), l3'')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)
APP(app(l1, cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2'''''''')))), l3''')

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(app(l1, cons(x'''', cons(x'''''', cons(x'''''''''', cons(x''''''''''', l1''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x'''''''''', cons(x''''''''''', l1'''''''')))), l3''')

two new Dependency Pairs are created:

APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l3'''')
APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''))))), l3'''')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 8

             ↳FwdInst

...

               →DP Problem 15

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''))))), l3'''')
APP(cons(x, cons(x''''0'', cons(x'''''0'', cons(x'''''''''', cons(x''''''''''', l1''''''''))))), l2'''''''') -> APP(cons(x''''0'', cons(x'''''0'', cons(x'''''''''', cons(x''''''''''', l1'''''''')))), l2'''''''')
APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l3'''')
APP(app(l1, cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2'''''''')))), l3''')
APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(l1'''''', l2''''''))), l3'')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)
APP(cons(x, cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2''''''''))))), l2''''''0) -> APP(cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2'''''''')))), l2''''''0)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

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

two new Dependency Pairs are created:

APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l2'''''''''')
APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''''))))), l2'''''''''')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 8

             ↳FwdInst

...

               →DP Problem 16

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''''))))), l2'''''''''')
APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l2'''''''''')
APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l3'''')
APP(app(l1, cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2'''''''')))), l3''')
APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(l1'''''', l2''''''))), l3'')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)
APP(cons(x, cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2''''''''))))), l2''''''0) -> APP(cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2'''''''')))), l2''''''0)
APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''))))), l3'''')

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l3'''')

two new Dependency Pairs are created:

APP(app(l1, cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0'', cons(x''''''''''''''0, cons(x'''''''''''''''', l1''''''''''''))))))), l3''''') -> APP(cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0'', cons(x''''''''''''''0, cons(x'''''''''''''''', l1'''''''''''')))))), l3''''')
APP(app(l1, cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0', cons(x''''''''''''''', app(l1'''''''''''', l2'''''''''''''))))))), l3''''') -> APP(cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0', cons(x''''''''''''''', app(l1'''''''''''', l2''''''''''''')))))), l3''''')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
APP(app(l1, cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0', cons(x''''''''''''''', app(l1'''''''''''', l2'''''''''''''))))))), l3''''') -> APP(cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0', cons(x''''''''''''''', app(l1'''''''''''', l2''''''''''''')))))), l3''''')
APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l2'''''''''')
APP(app(l1, cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0'', cons(x''''''''''''''0, cons(x'''''''''''''''', l1''''''''''''))))))), l3''''') -> APP(cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0'', cons(x''''''''''''''0, cons(x'''''''''''''''', l1'''''''''''')))))), l3''''')
APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''))))), l3'''')
APP(app(l1, cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2'''''''')))), l3''')
APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(l1'''''', l2''''''))), l3'')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)
APP(cons(x, cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2''''''''))))), l2''''''0) -> APP(cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2'''''''')))), l2''''''0)
APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''''))))), l2'''''''''')

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:
innermost
Dependency Pairs:
IFMEM(false, x, l) -> MEM(x, l)
MEM(x, cons(y, l)) -> IFMEM(eq(x, y), x, l)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:
innermost
Dependency Pairs:
IFINTER(false, x, l1, l2) -> INTER(l1, l2)
INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1)
IFINTER(true, x, l1, l2) -> INTER(l1, l2)
INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2)
INTER(l1, app(l2, l3)) -> INTER(l1, l3)
INTER(app(l1, l2), l3) -> INTER(l2, l3)
INTER(l1, app(l2, l3)) -> INTER(l1, l2)
INTER(app(l1, l2), l3) -> INTER(l1, l3)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:
innermost

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
APP(app(l1, cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0', cons(x''''''''''''''', app(l1'''''''''''', l2'''''''''''''))))))), l3''''') -> APP(cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0', cons(x''''''''''''''', app(l1'''''''''''', l2''''''''''''')))))), l3''''')
APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l2'''''''''')
APP(app(l1, cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0'', cons(x''''''''''''''0, cons(x'''''''''''''''', l1''''''''''''))))))), l3''''') -> APP(cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0'', cons(x''''''''''''''0, cons(x'''''''''''''''', l1'''''''''''')))))), l3''''')
APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''))))), l3'''')
APP(app(l1, cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2'''''''')))), l3''')
APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(l1'''''', l2''''''))), l3'')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)
APP(cons(x, cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2''''''''))))), l2''''''0) -> APP(cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2'''''''')))), l2''''''0)
APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''''))))), l2'''''''''')

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:
innermost
Dependency Pairs:
IFMEM(false, x, l) -> MEM(x, l)
MEM(x, cons(y, l)) -> IFMEM(eq(x, y), x, l)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:
innermost
Dependency Pairs:
IFINTER(false, x, l1, l2) -> INTER(l1, l2)
INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1)
IFINTER(true, x, l1, l2) -> INTER(l1, l2)
INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2)
INTER(l1, app(l2, l3)) -> INTER(l1, l3)
INTER(app(l1, l2), l3) -> INTER(l2, l3)
INTER(l1, app(l2, l3)) -> INTER(l1, l2)
INTER(app(l1, l2), l3) -> INTER(l1, l3)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:
innermost

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
APP(app(l1, cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0', cons(x''''''''''''''', app(l1'''''''''''', l2'''''''''''''))))))), l3''''') -> APP(cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0', cons(x''''''''''''''', app(l1'''''''''''', l2''''''''''''')))))), l3''''')
APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1'''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''0, cons(x'''''''''''''', l1''''''''''))))), l2'''''''''')
APP(app(l1, cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0'', cons(x''''''''''''''0, cons(x'''''''''''''''', l1''''''''''''))))))), l3''''') -> APP(cons(x'''''', cons(x'''''''', cons(x''''''''''0'', cons(x'''''''''''0'', cons(x''''''''''''''0, cons(x'''''''''''''''', l1'''''''''''')))))), l3''''')
APP(app(l1, cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''')))))), l3'''') -> APP(cons(x''''', cons(x''''''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''))))), l3'''')
APP(app(l1, cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2''''''''))))), l3''') -> APP(cons(x'''', cons(x'''''', cons(x''''''''', app(l1'''''''', l2'''''''')))), l3''')
APP(app(l1, cons(x''', cons(x'''''', app(l1'''''', l2'''''')))), l3'') -> APP(cons(x''', cons(x'''''', app(l1'''''', l2''''''))), l3'')
APP(app(l1, cons(x'', app(l1'''', l2''''))), l3') -> APP(cons(x'', app(l1'''', l2'''')), l3')
APP(app(l1, app(l1'', l2'')), l3'') -> APP(app(l1'', l2''), l3'')
APP(cons(x, app(l1'', l2'')), l20) -> APP(app(l1'', l2''), l20)
APP(cons(x, cons(x''', app(l1'''', l2''''))), l2''0) -> APP(cons(x''', app(l1'''', l2'''')), l2''0)
APP(cons(x, cons(x''''0, cons(x'''''', app(l1'''''', l2'''''')))), l2''''0) -> APP(cons(x''''0, cons(x'''''', app(l1'''''', l2''''''))), l2''''0)
APP(cons(x, cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2''''''''))))), l2''''''0) -> APP(cons(x''''0'', cons(x'''''0', cons(x''''''''', app(l1'''''''', l2'''''''')))), l2''''''0)
APP(cons(x, cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2''''''''''')))))), l2'''''''''') -> APP(cons(x''''0'''', cons(x'''''0'''', cons(x''''''''''0, cons(x'''''''''''', app(l1'''''''''', l2'''''''''''))))), l2'''''''''')

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:
innermost
Dependency Pairs:
IFMEM(false, x, l) -> MEM(x, l)
MEM(x, cons(y, l)) -> IFMEM(eq(x, y), x, l)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:
innermost
Dependency Pairs:
IFINTER(false, x, l1, l2) -> INTER(l1, l2)
INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1)
IFINTER(true, x, l1, l2) -> INTER(l1, l2)
INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2)
INTER(l1, app(l2, l3)) -> INTER(l1, l3)
INTER(app(l1, l2), l3) -> INTER(l2, l3)
INTER(l1, app(l2, l3)) -> INTER(l1, l2)
INTER(app(l1, l2), l3) -> INTER(l1, l3)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
eq(0, 0) -> true
eq(0, s(x)) -> false
eq(s(x), 0) -> false
eq(s(x), s(y)) -> eq(x, y)
app(nil, l) -> l
app(cons(x, l1), l2) -> cons(x, app(l1, l2))
app(app(l1, l2), l3) -> app(l1, app(l2, l3))
mem(x, nil) -> false
mem(x, cons(y, l)) -> ifmem(eq(x, y), x, l)
ifmem(true, x, l) -> true
ifmem(false, x, l) -> 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)

Strategy:
innermost

Innermost Termination of R could not be shown.
Duration:
0:03 minutes