Term Rewriting System R:

   [y, x, u, v, z]
   merge(nil, y) -> y
   merge(x, nil) -> x
   merge(.(x, y), .(u, v)) -> if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
   ++(nil, y) -> y
   ++(.(x, y), z) -> .(x, ++(y, z))
   if(true, x, y) -> x
   if(false, x, y) -> x

Termination of R to be shown.


R contains the following Dependency Pairs: 


   ++'(.(x, y), z) -> ++'(y, z)
   MERGE(.(x, y), .(u, v)) -> IF(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
   MERGE(.(x, y), .(u, v)) -> MERGE(y, .(u, v))
   MERGE(.(x, y), .(u, v)) -> MERGE(.(x, y), v)

Furthermore, R contains two SCCs.


SCC1:

++'(.(x, y), z) -> ++'(y, z)

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(++'(x_1, x_2)) = 1 + x_1 + x_2
POL(.(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   ++'(.(x, y), z) -> ++'(y, z)



 This transformation is resulting in no new subcycles.


SCC2:

MERGE(.(x, y), .(u, v)) -> MERGE(.(x, y), v)
MERGE(.(x, y), .(u, v)) -> MERGE(y, .(u, v))

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(MERGE(x_1, x_2)) = 1 + x_1 + x_2
POL(.(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   MERGE(.(x, y), .(u, v)) -> MERGE(.(x, y), v)
   MERGE(.(x, y), .(u, v)) -> MERGE(y, .(u, v))



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 0.596 seconds.