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)

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

         ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

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)

The following dependency pair can be strictly oriented:

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

There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 5

             ↳Dependency Graph

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polynomial Ordering

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

Dependency Pairs:

APP(app(l1, l2), l3) -> APP(l2, l3)
APP(app(l1, l2), l3) -> APP(l1, 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)

The following dependency pairs can be strictly oriented:

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

There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(nil) = 0

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 6

             ↳Polynomial Ordering

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

Dependency Pair:

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)

The following dependency pair can be strictly oriented:

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

There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 6

             ↳Polo

...

               →DP Problem 7

                 ↳Dependency Graph

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polynomial Ordering

       →DP Problem 4

         ↳Polo

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)

The following dependency pair can be strictly oriented:

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

There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(eq(x₁, x₂)) = 0

POL(0) = 0

POL(false) = 0

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

POL(IFMEM(x₁, x₂, x₃)) = x₃

POL(true) = 0

POL(s(x₁)) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

             ↳Dependency Graph

       →DP Problem 4

         ↳Polo

Dependency Pair:

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)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polynomial Ordering

Dependency Pairs:

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

Rules:

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)

The following dependency pairs can be strictly oriented:

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

There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(mem(x₁, x₂)) = 0

POL(eq(x₁, x₂)) = 0

POL(0) = 0

POL(false) = 0

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

POL(ifmem(x₁, x₂, x₃)) = 0

POL(nil) = 0

POL(true) = 0

POL(s(x₁)) = 0

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

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

           →DP Problem 9

             ↳Polynomial Ordering

Dependency Pairs:

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)

The following dependency pairs can be strictly oriented:

INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1)
INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2)

There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(mem(x₁, x₂)) = 0

POL(eq(x₁, x₂)) = 0

POL(0) = 0

POL(false) = 0

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

POL(ifmem(x₁, x₂, x₃)) = 0

POL(nil) = 0

POL(true) = 0

POL(s(x₁)) = 0

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

           →DP Problem 9

             ↳Polo

...

               →DP Problem 10

                 ↳Dependency Graph

Dependency Pairs:

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

Using the Dependency Graph resulted in no new DP problems.

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

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

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

POL(MEM(x₁, x₂))	= x₂
POL(eq(x₁, x₂))	= 0
POL(0)	= 0
POL(false)	= 0
POL(cons(x₁, x₂))	= 1 + x₂
POL(IFMEM(x₁, x₂, x₃))	= x₃
POL(true)	= 0
POL(s(x₁))	= 0