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.


R contains the following Dependency Pairs: 


   APP(app(l1, l2), l3) -> APP(l1, app(l2, l3))
   APP(app(l1, l2), l3) -> APP(l2, l3)
   APP(cons(x, l1), l2) -> APP(l1, l2)
   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)
   MEM(x, cons(y, l)) -> IFMEM(eq(x, y), x, l)
   MEM(x, cons(y, l)) -> EQ(x, y)
   IFINTER(false, x, l1, l2) -> INTER(l1, l2)
   IFINTER(true, x, l1, l2) -> INTER(l1, l2)
   EQ(s(x), s(y)) -> EQ(x, y)
   IFMEM(false, x, l) -> MEM(x, l)

Furthermore, R contains four SCCs.


SCC1:

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

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(nil) = 1
POL(APP(x_1, x_2)) = 1 + x_1 + x_2
POL(app(x_1, x_2)) = x_1 + x_2
POL(cons(x_1, x_2)) = x_1 + x_2

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

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


 This transformation is resulting in one new subcycle:


SCC1.MRR1:

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)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(APP(x_1, x_2)) = x_1 + x_2
POL(app(x_1, x_2)) = x_1 + x_2
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

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

No rules of R can be deleted.


 This transformation is resulting in one new subcycle:


SCC1.MRR1.MRR1:

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

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(APP(x_1, x_2)) = 1 + x_1 + x_2
POL(app(x_1, x_2)) = 1 + x_1 + x_2
POL(cons(x_1, x_2)) = x_1 + x_2

The following Dependency Pairs can be deleted:

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

No rules of R can be deleted.


 This transformation is resulting in one new subcycle:


SCC1.MRR1.MRR1.MRR1:

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

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(APP(x_1, x_2)) = x_1
POL(app(x_1, x_2)) = 1 + x_1
POL(cons(x_1, x_2)) = 0

 resulting in no subcycles.


SCC2:

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

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(EQ(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

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



 This transformation is resulting in no new subcycles.


SCC3:

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

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   eq(s(x), 0) -> false
   eq(0, s(x)) -> false
   eq(0, 0) -> true
   eq(s(x), s(y)) -> eq(x, y)


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(eq(x_1, x_2)) = x_2
POL(MEM(x_1, x_2)) = x_2
POL(true) = 0
POL(IFMEM(x_1, x_2, x_3)) = x_1 + x_3
POL(0) = 1
POL(false) = 1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

 resulting in no subcycles.


SCC4:

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

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(nil) = 0
POL(ifmem(x_1, x_2, x_3)) = 0
POL(s(x_1)) = 0
POL(eq(x_1, x_2)) = 0
POL(true) = 0
POL(IFINTER(x_1, x_2, x_3, x_4)) = 1 + x_3 + x_4
POL(mem(x_1, x_2)) = 0
POL(0) = 0
POL(INTER(x_1, x_2)) = x_1 + x_2
POL(app(x_1, x_2)) = x_1 + x_2
POL(false) = 0
POL(cons(x_1, x_2)) = 1 + x_2

 resulting in one subcycle.


SCC4.Polo1:

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

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(INTER(x_1, x_2)) = 1 + x_1 + x_2
POL(app(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

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



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 1.354 seconds.