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

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

       →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

The following dependency pair can be strictly oriented:

EQ(s(x), s(y)) -> EQ(x, 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

         ↳AFS

           →DP Problem 5

             ↳Dependency Graph

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

       →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

         ↳AFS

       →DP Problem 2

         ↳Argument Filtering and Ordering

       →DP Problem 3

         ↳Nar

       →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

The following dependency pairs can be strictly oriented:

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

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:

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

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 6

             ↳Dependency Graph

       →DP Problem 3

         ↳Nar

       →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

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Narrowing Transformation

       →DP Problem 4

         ↳Remaining

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

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

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

four new Dependency Pairs are created:

MEM(0, cons(0, l)) -> IFMEM(true, 0, l)
MEM(0, cons(s(x''), l)) -> IFMEM(false, 0, l)
MEM(s(x''), cons(0, l)) -> IFMEM(false, s(x''), l)
MEM(s(x''), cons(s(y''), l)) -> IFMEM(eq(x'', y''), s(x''), l)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 7

             ↳Instantiation Transformation

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

MEM(s(x''), cons(s(y''), l)) -> IFMEM(eq(x'', y''), s(x''), l)
MEM(s(x''), cons(0, l)) -> IFMEM(false, s(x''), l)
MEM(0, cons(s(x''), l)) -> IFMEM(false, 0, l)
IFMEM(false, x, l) -> MEM(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

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

IFMEM(false, x, l) -> MEM(x, l)

three new Dependency Pairs are created:

IFMEM(false, 0, l'') -> MEM(0, l'')
IFMEM(false, s(x''''), l'') -> MEM(s(x''''), l'')
IFMEM(false, s(x'''''), l'') -> MEM(s(x'''''), l'')

The transformation is resulting in two new DP problems:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 7

             ↳Inst

...

               →DP Problem 8

                 ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

IFMEM(false, s(x'''''), l'') -> MEM(s(x'''''), l'')
MEM(s(x''), cons(0, l)) -> IFMEM(false, s(x''), l)
IFMEM(false, s(x''''), l'') -> MEM(s(x''''), l'')
MEM(s(x''), cons(s(y''), l)) -> IFMEM(eq(x'', y''), s(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

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

IFMEM(false, s(x''''), l'') -> MEM(s(x''''), l'')

two new Dependency Pairs are created:

IFMEM(false, s(x'''''), cons(0, l''')) -> MEM(s(x'''''), cons(0, l'''))
IFMEM(false, s(x'''''), cons(s(y''''), l''')) -> MEM(s(x'''''), cons(s(y''''), l'''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 7

             ↳Inst

...

               →DP Problem 10

                 ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

MEM(s(x''), cons(s(y''), l)) -> IFMEM(eq(x'', y''), s(x''), l)
IFMEM(false, s(x'''''), cons(s(y''''), l''')) -> MEM(s(x'''''), cons(s(y''''), l'''))
IFMEM(false, s(x'''''), cons(0, l''')) -> MEM(s(x'''''), cons(0, l'''))
MEM(s(x''), cons(0, l)) -> IFMEM(false, s(x''), l)
IFMEM(false, s(x'''''), l'') -> MEM(s(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

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

IFMEM(false, s(x'''''), l'') -> MEM(s(x'''''), l'')

two new Dependency Pairs are created:

IFMEM(false, s(x''''''), cons(0, l''')) -> MEM(s(x''''''), cons(0, l'''))
IFMEM(false, s(x''''''), cons(s(y''''), l''')) -> MEM(s(x''''''), cons(s(y''''), l'''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 7

             ↳Inst

...

               →DP Problem 12

                 ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

IFMEM(false, s(x''''''), cons(s(y''''), l''')) -> MEM(s(x''''''), cons(s(y''''), l'''))
IFMEM(false, s(x''''''), cons(0, l''')) -> MEM(s(x''''''), cons(0, l'''))
IFMEM(false, s(x'''''), cons(s(y''''), l''')) -> MEM(s(x'''''), cons(s(y''''), l'''))
MEM(s(x''), cons(0, l)) -> IFMEM(false, s(x''), l)
IFMEM(false, s(x'''''), cons(0, l''')) -> MEM(s(x'''''), cons(0, l'''))
MEM(s(x''), cons(s(y''), l)) -> IFMEM(eq(x'', y''), s(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

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

MEM(s(x''), cons(0, l)) -> IFMEM(false, s(x''), l)

two new Dependency Pairs are created:

MEM(s(x'''), cons(0, cons(0, l'''''))) -> IFMEM(false, s(x'''), cons(0, l'''''))
MEM(s(x'''), cons(0, cons(s(y''''''), l'''''))) -> IFMEM(false, s(x'''), cons(s(y''''''), l'''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 7

             ↳Inst

...

               →DP Problem 14

                 ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

IFMEM(false, s(x'''''), cons(s(y''''), l''')) -> MEM(s(x'''''), cons(s(y''''), l'''))
MEM(s(x'''), cons(0, cons(s(y''''''), l'''''))) -> IFMEM(false, s(x'''), cons(s(y''''''), l'''''))
IFMEM(false, s(x''''''), cons(0, l''')) -> MEM(s(x''''''), cons(0, l'''))
MEM(s(x'''), cons(0, cons(0, l'''''))) -> IFMEM(false, s(x'''), cons(0, l'''''))
IFMEM(false, s(x'''''), cons(0, l''')) -> MEM(s(x'''''), cons(0, l'''))
MEM(s(x''), cons(s(y''), l)) -> IFMEM(eq(x'', y''), s(x''), l)
IFMEM(false, s(x''''''), cons(s(y''''), l''')) -> MEM(s(x''''''), cons(s(y''''), 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

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

MEM(s(x''), cons(s(y''), l)) -> IFMEM(eq(x'', y''), s(x''), l)

two new Dependency Pairs are created:

MEM(s(x'''), cons(s(y'''), cons(0, l'''''))) -> IFMEM(eq(x''', y'''), s(x'''), cons(0, l'''''))
MEM(s(x'''), cons(s(y'''), cons(s(y''''''), l'''''))) -> IFMEM(eq(x''', y'''), s(x'''), cons(s(y''''''), l'''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

       →DP Problem 4

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
MEM(s(x'''), cons(s(y'''), cons(s(y''''''), l'''''))) -> IFMEM(eq(x''', y'''), s(x'''), cons(s(y''''''), l'''''))
IFMEM(false, s(x''''''), cons(s(y''''), l''')) -> MEM(s(x''''''), cons(s(y''''), l'''))
MEM(s(x'''), cons(0, cons(s(y''''''), l'''''))) -> IFMEM(false, s(x'''), cons(s(y''''''), l'''''))
IFMEM(false, s(x''''''), cons(0, l''')) -> MEM(s(x''''''), cons(0, l'''))
MEM(s(x'''), cons(0, cons(0, l'''''))) -> IFMEM(false, s(x'''), cons(0, l'''''))
IFMEM(false, s(x'''''), cons(0, l''')) -> MEM(s(x'''''), cons(0, l'''))
MEM(s(x'''), cons(s(y'''), cons(0, l'''''))) -> IFMEM(eq(x''', y'''), s(x'''), cons(0, l'''''))
IFMEM(false, s(x'''''), cons(s(y''''), l''')) -> MEM(s(x'''''), cons(s(y''''), 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

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 7

             ↳Inst

...

               →DP Problem 9

                 ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

IFMEM(false, 0, l'') -> MEM(0, l'')
MEM(0, cons(s(x''), l)) -> IFMEM(false, 0, 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

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

IFMEM(false, 0, l'') -> MEM(0, l'')

one new Dependency Pair is created:

IFMEM(false, 0, cons(s(x''''), l''')) -> MEM(0, cons(s(x''''), l'''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 7

             ↳Inst

...

               →DP Problem 11

                 ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

IFMEM(false, 0, cons(s(x''''), l''')) -> MEM(0, cons(s(x''''), l'''))
MEM(0, cons(s(x''), l)) -> IFMEM(false, 0, 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

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

MEM(0, cons(s(x''), l)) -> IFMEM(false, 0, l)

one new Dependency Pair is created:

MEM(0, cons(s(x''), cons(s(x''''''), l'''''))) -> IFMEM(false, 0, cons(s(x''''''), l'''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 7

             ↳Inst

...

               →DP Problem 13

                 ↳Argument Filtering and Ordering

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

MEM(0, cons(s(x''), cons(s(x''''''), l'''''))) -> IFMEM(false, 0, cons(s(x''''''), l'''''))
IFMEM(false, 0, cons(s(x''''), l''')) -> MEM(0, cons(s(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

The following dependency pair can be strictly oriented:

MEM(0, cons(s(x''), cons(s(x''''''), l'''''))) -> IFMEM(false, 0, cons(s(x''''''), l'''''))

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:

MEM(x₁, x₂) -> x₂
cons(x₁, x₂) -> cons(x₁, x₂)
IFMEM(x₁, x₂, x₃) -> x₃
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 7

             ↳Inst

...

               →DP Problem 16

                 ↳Dependency Graph

       →DP Problem 4

         ↳Remaining

Dependency Pair:

IFMEM(false, 0, cons(s(x''''), l''')) -> MEM(0, cons(s(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

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

       →DP Problem 4

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
MEM(s(x'''), cons(s(y'''), cons(s(y''''''), l'''''))) -> IFMEM(eq(x''', y'''), s(x'''), cons(s(y''''''), l'''''))
IFMEM(false, s(x''''''), cons(s(y''''), l''')) -> MEM(s(x''''''), cons(s(y''''), l'''))
MEM(s(x'''), cons(0, cons(s(y''''''), l'''''))) -> IFMEM(false, s(x'''), cons(s(y''''''), l'''''))
IFMEM(false, s(x''''''), cons(0, l''')) -> MEM(s(x''''''), cons(0, l'''))
MEM(s(x'''), cons(0, cons(0, l'''''))) -> IFMEM(false, s(x'''), cons(0, l'''''))
IFMEM(false, s(x'''''), cons(0, l''')) -> MEM(s(x'''''), cons(0, l'''))
MEM(s(x'''), cons(s(y'''), cons(0, l'''''))) -> IFMEM(eq(x''', y'''), s(x'''), cons(0, l'''''))
IFMEM(false, s(x'''''), cons(s(y''''), l''')) -> MEM(s(x'''''), cons(s(y''''), 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:05 minutes