Term Rewriting System R:

   [x, y, n, m]
   eq(0, 0) -> true
   eq(0, s(x)) -> false
   eq(s(x), 0) -> false
   eq(s(x), s(y)) -> eq(x, y)
   le(0, y) -> true
   le(s(x), 0) -> false
   le(s(x), s(y)) -> le(x, y)
   app(nil, y) -> y
   app(add(n, x), y) -> add(n, app(x, y))
   min(add(n, nil)) -> n
   min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x)))
   if_min(true, add(n, add(m, x))) -> min(add(n, x))
   if_min(false, add(n, add(m, x))) -> min(add(m, x))
   rm(n, nil) -> nil
   rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x))
   if_rm(true, n, add(m, x)) -> rm(n, x)
   if_rm(false, n, add(m, x)) -> add(m, rm(n, x))
   minsort(nil, nil) -> nil
   minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y)
   if_minsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
   if_minsort(false, add(n, x), y) -> minsort(x, add(n, y))

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   APP(add(n, x), y) -> APP(x, y)
   LE(s(x), s(y)) -> LE(x, y)
   RM(n, add(m, x)) -> IF_RM(eq(n, m), n, add(m, x))
   RM(n, add(m, x)) -> EQ(n, m)
   MIN(add(n, add(m, x))) -> IF_MIN(le(n, m), add(n, add(m, x)))
   MIN(add(n, add(m, x))) -> LE(n, m)
   MINSORT(add(n, x), y) -> IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
   MINSORT(add(n, x), y) -> EQ(n, min(add(n, x)))
   MINSORT(add(n, x), y) -> MIN(add(n, x))
   IF_MINSORT(false, add(n, x), y) -> MINSORT(x, add(n, y))
   IF_MINSORT(true, add(n, x), y) -> MINSORT(app(rm(n, x), y), nil)
   IF_MINSORT(true, add(n, x), y) -> APP(rm(n, x), y)
   IF_MINSORT(true, add(n, x), y) -> RM(n, x)
   EQ(s(x), s(y)) -> EQ(x, y)
   IF_MIN(true, add(n, add(m, x))) -> MIN(add(n, x))
   IF_MIN(false, add(n, add(m, x))) -> MIN(add(m, x))
   IF_RM(true, n, add(m, x)) -> RM(n, x)
   IF_RM(false, n, add(m, x)) -> RM(n, x)

Furthermore, R contains six SCCs.


SCC1:

APP(add(n, x), y) -> APP(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(add(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:

   APP(add(n, x), y) -> APP(x, y)



 This transformation is resulting in no new subcycles.


SCC2:

LE(s(x), s(y)) -> LE(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(LE(x_1, x_2)) = 1 + x_1 + x_2
POL(s(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

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



 This transformation is resulting in no new subcycles.


SCC3:

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.


SCC4:

IF_MIN(false, add(n, add(m, x))) -> MIN(add(m, x))
IF_MIN(true, add(n, add(m, x))) -> MIN(add(n, x))
MIN(add(n, add(m, x))) -> IF_MIN(le(n, m), add(n, add(m, x)))

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(add(x_1, x_2)) = 1 + x_2
POL(IF_MIN(x_1, x_2)) = x_2
POL(s(x_1)) = 0
POL(le(x_1, x_2)) = 0
POL(MIN(x_1)) = x_1
POL(true) = 0
POL(0) = 0
POL(false) = 0

 resulting in no subcycles.


SCC5:

IF_RM(false, n, add(m, x)) -> RM(n, x)
IF_RM(true, n, add(m, x)) -> RM(n, x)
RM(n, add(m, x)) -> IF_RM(eq(n, m), n, add(m, x))

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(IF_RM(x_1, x_2, x_3)) = x_3
POL(add(x_1, x_2)) = 1 + x_2
POL(s(x_1)) = 0
POL(eq(x_1, x_2)) = 0
POL(RM(x_1, x_2)) = x_2
POL(true) = 0
POL(0) = 0
POL(false) = 0

 resulting in no subcycles.


SCC6:

IF_MINSORT(true, add(n, x), y) -> MINSORT(app(rm(n, x), y), nil)
IF_MINSORT(false, add(n, x), y) -> MINSORT(x, add(n, y))
MINSORT(add(n, x), y) -> IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)

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

Additionally, the following rules can be oriented: 

   if_rm(true, n, add(m, x)) -> rm(n, x)
   if_rm(false, n, add(m, x)) -> add(m, rm(n, x))
   rm(n, nil) -> nil
   rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x))
   app(add(n, x), y) -> add(n, app(x, y))
   app(nil, y) -> y


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(nil) = 0
POL(add(x_1, x_2)) = 1 + x_2
POL(s(x_1)) = 0
POL(eq(x_1, x_2)) = 0
POL(if_rm(x_1, x_2, x_3)) = x_3
POL(MINSORT(x_1, x_2)) = x_1 + x_2
POL(min(x_1)) = 0
POL(0) = 0
POL(le(x_1, x_2)) = 0
POL(if_min(x_1, x_2)) = 0
POL(rm(x_1, x_2)) = x_2
POL(true) = 0
POL(IF_MINSORT(x_1, x_2, x_3)) = x_2 + x_3
POL(app(x_1, x_2)) = x_1 + x_2
POL(false) = 0

 resulting in one subcycle.


SCC6.Polo1:

MINSORT(add(n, x), y) -> IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) -> MINSORT(x, add(n, y))

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(add(x_1, x_2)) = 1 + x_2
POL(nil) = 0
POL(s(x_1)) = 0
POL(le(x_1, x_2)) = 0
POL(eq(x_1, x_2)) = 0
POL(if_min(x_1, x_2)) = 0
POL(true) = 0
POL(IF_MINSORT(x_1, x_2, x_3)) = x_2
POL(MINSORT(x_1, x_2)) = 1 + x_1
POL(min(x_1)) = 0
POL(0) = 0
POL(false) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 2.340 seconds.