Term Rewriting System R:

   [x, n, h, t, m, pid, store]
   fstsplit(0, x) -> nil
   fstsplit(s(n), nil) -> nil
   fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
   sndsplit(0, x) -> x
   sndsplit(s(n), nil) -> nil
   sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
   empty(nil) -> true
   empty(cons(h, t)) -> false
   leq(0, m) -> true
   leq(s(n), 0) -> false
   leq(s(n), s(m)) -> leq(n, m)
   length(nil) -> 0
   length(cons(h, t)) -> s(length(t))
   app(nil, x) -> x
   app(cons(h, t), x) -> cons(h, app(t, x))
   map_f(pid, nil) -> nil
   map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
   process(store, m) -> if1(store, m, leq(m, length(store)))
   if1(store, m, true) -> if2(store, m, empty(fstsplit(m, store)))
   if1(store, m, false) -> if3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
   if2(store, m, false) -> process(app(map_f(self, nil), sndsplit(m, store)), m)
   if3(store, m, false) -> process(sndsplit(m, app(map_f(self, nil), store)), m)

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: 


   LENGTH(cons(h, t)) -> LENGTH(t)
   MAP_F(pid, cons(h, t)) -> APP(f(pid, h), map_f(pid, t))
   MAP_F(pid, cons(h, t)) -> MAP_F(pid, t)
   IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
   IF1(store, m, true) -> EMPTY(fstsplit(m, store))
   IF1(store, m, true) -> FSTSPLIT(m, store)
   IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
   IF1(store, m, false) -> EMPTY(fstsplit(m, app(map_f(self, nil), store)))
   IF1(store, m, false) -> FSTSPLIT(m, app(map_f(self, nil), store))
   IF1(store, m, false) -> APP(map_f(self, nil), store)
   IF1(store, m, false) -> MAP_F(self, nil)
   IF2(store, m, false) -> PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
   IF2(store, m, false) -> APP(map_f(self, nil), sndsplit(m, store))
   IF2(store, m, false) -> MAP_F(self, nil)
   IF2(store, m, false) -> SNDSPLIT(m, store)
   FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)
   IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
   IF3(store, m, false) -> SNDSPLIT(m, app(map_f(self, nil), store))
   IF3(store, m, false) -> APP(map_f(self, nil), store)
   IF3(store, m, false) -> MAP_F(self, nil)
   APP(cons(h, t), x) -> APP(t, x)
   SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)
   LEQ(s(n), s(m)) -> LEQ(n, m)
   PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
   PROCESS(store, m) -> LEQ(m, length(store))
   PROCESS(store, m) -> LENGTH(store)

Furthermore, R contains seven SCCs.


SCC1:

LENGTH(cons(h, t)) -> LENGTH(t)

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

The following Dependency Pairs can be deleted:

   LENGTH(cons(h, t)) -> LENGTH(t)



 This transformation is resulting in no new subcycles.


SCC2:

FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)

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(FSTSPLIT(x_1, x_2)) = 1 + x_1 + x_2
POL(s(x_1)) = 1 + x_1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)



 This transformation is resulting in no new subcycles.


SCC3:

LEQ(s(n), s(m)) -> LEQ(n, m)

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

The following Dependency Pairs can be deleted:

   LEQ(s(n), s(m)) -> LEQ(n, m)



 This transformation is resulting in no new subcycles.


SCC4:

SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)

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(SNDSPLIT(x_1, x_2)) = 1 + x_1 + x_2
POL(s(x_1)) = 1 + x_1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)



 This transformation is resulting in no new subcycles.


SCC5:

APP(cons(h, t), x) -> APP(t, x)

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

The following Dependency Pairs can be deleted:

   APP(cons(h, t), x) -> APP(t, x)



 This transformation is resulting in no new subcycles.


SCC6:

MAP_F(pid, cons(h, t)) -> MAP_F(pid, t)

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

The following Dependency Pairs can be deleted:

   MAP_F(pid, cons(h, t)) -> MAP_F(pid, t)



 This transformation is resulting in no new subcycles.


SCC7:

IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF2(store, m, false) -> PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(map_f(self, nil), store))))
one new Dependency Pair
is created:


   IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(nil, store))))

The transformation is resulting in one subcycle:


SCC7.Rewr1:

IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(nil, store))))
IF2(store, m, false) -> PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   IF2(store, m, false) -> PROCESS(app(map_f(self, nil), sndsplit(m, store)), m)
one new Dependency Pair
is created:


   IF2(store, m, false) -> PROCESS(app(nil, sndsplit(m, store)), m)

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1:

IF2(store, m, false) -> PROCESS(app(nil, sndsplit(m, store)), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(nil, store))))

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   IF3(store, m, false) -> PROCESS(sndsplit(m, app(map_f(self, nil), store)), m)
one new Dependency Pair
is created:


   IF3(store, m, false) -> PROCESS(sndsplit(m, app(nil, store)), m)

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1:

IF3(store, m, false) -> PROCESS(sndsplit(m, app(nil, store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(nil, store))))
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF2(store, m, false) -> PROCESS(app(nil, sndsplit(m, store)), m)

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, app(nil, store))))
one new Dependency Pair
is created:


   IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1:

IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
IF2(store, m, false) -> PROCESS(app(nil, sndsplit(m, store)), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF3(store, m, false) -> PROCESS(sndsplit(m, app(nil, store)), m)

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   IF2(store, m, false) -> PROCESS(app(nil, sndsplit(m, store)), m)
one new Dependency Pair
is created:


   IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1:

IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF3(store, m, false) -> PROCESS(sndsplit(m, app(nil, store)), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   IF3(store, m, false) -> PROCESS(sndsplit(m, app(nil, store)), m)
one new Dependency Pair
is created:


   IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1:

IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)

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

   IF1(store, m, true) -> IF2(store, m, empty(fstsplit(m, store)))
three new Dependency Pairs
are created:


   IF1(store', 0, true) -> IF2(store', 0, empty(nil))
   IF1(nil, s(n'), true) -> IF2(nil, s(n'), empty(nil))
   IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1:

IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
IF1(nil, s(n'), true) -> IF2(nil, s(n'), empty(nil))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store', 0, true) -> IF2(store', 0, empty(nil))
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   IF1(store', 0, true) -> IF2(store', 0, empty(nil))
one new Dependency Pair
is created:


   IF1(store', 0, true) -> IF2(store', 0, true)

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1.Rewr1:

IF1(nil, s(n'), true) -> IF2(nil, s(n'), empty(nil))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   IF1(nil, s(n'), true) -> IF2(nil, s(n'), empty(nil))
one new Dependency Pair
is created:


   IF1(nil, s(n'), true) -> IF2(nil, s(n'), true)

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1.Rewr1.Rewr1:

IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
one new Dependency Pair
is created:


   IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1.Rewr1.Rewr1.Rewr1:

IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)

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

   PROCESS(store, m) -> IF1(store, m, leq(m, length(store)))
three new Dependency Pairs
are created:


   PROCESS(store', 0) -> IF1(store', 0, true)
   PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
   PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1.Rewr1.Rewr1.Rewr1.Nar1:

PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)

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

   IF1(store, m, false) -> IF3(store, m, empty(fstsplit(m, store)))
three new Dependency Pairs
are created:


   IF1(store', 0, false) -> IF3(store', 0, empty(nil))
   IF1(nil, s(n'), false) -> IF3(nil, s(n'), empty(nil))
   IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1.Rewr1.Rewr1.Rewr1.Nar1.Nar1:

IF1(nil, s(n'), false) -> IF3(nil, s(n'), empty(nil))
IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(store', 0, false) -> IF3(store', 0, empty(nil))
PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   IF1(store', 0, false) -> IF3(store', 0, empty(nil))
one new Dependency Pair
is created:


   IF1(store', 0, false) -> IF3(store', 0, true)

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1.Rewr1.Rewr1.Rewr1.Nar1.Nar1.Rewr1:

IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
PROCESS(nil, m) -> IF1(nil, m, leq(m, 0))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(nil, s(n'), false) -> IF3(nil, s(n'), empty(nil))

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   IF1(nil, s(n'), false) -> IF3(nil, s(n'), empty(nil))
one new Dependency Pair
is created:


   IF1(nil, s(n'), false) -> IF3(nil, s(n'), true)

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1.Rewr1.Rewr1.Rewr1.Nar1.Nar1.Rewr1.Rewr1:

IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), empty(cons(h', fstsplit(n', t'))))
one new Dependency Pair
is created:


   IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1.Rewr1.Rewr1.Rewr1.Nar1.Nar1.Rewr1.Rewr1.Rewr1:

IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)

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

   IF2(store, m, false) -> PROCESS(sndsplit(m, store), m)
three new Dependency Pairs
are created:


   IF2(store', 0, false) -> PROCESS(store', 0)
   IF2(nil, s(n'), false) -> PROCESS(nil, s(n'))
   IF2(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1.Rewr1.Rewr1.Rewr1.Nar1.Nar1.Rewr1.Rewr1.Rewr1.Nar1:

IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)
IF2(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)

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

   IF3(store, m, false) -> PROCESS(sndsplit(m, store), m)
three new Dependency Pairs
are created:


   IF3(store', 0, false) -> PROCESS(store', 0)
   IF3(nil, s(n'), false) -> PROCESS(nil, s(n'))
   IF3(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1.Rewr1.Rewr1.Rewr1.Nar1.Nar1.Rewr1.Rewr1.Rewr1.Nar1.Nar1:

IF2(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
IF3(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))
IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)

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

   PROCESS(cons(h', t'), m) -> IF1(cons(h', t'), m, leq(m, s(length(t'))))
one new Dependency Pair
is created:


   PROCESS(cons(h'', t''), s(n''')) -> IF1(cons(h'', t''), s(n'''), leq(s(n'''), s(length(t''))))

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1.Rewr1.Rewr1.Rewr1.Nar1.Nar1.Rewr1.Rewr1.Rewr1.Nar1.Nar1.Inst1:

IF3(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))
IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h'', t''), s(n''')) -> IF1(cons(h'', t''), s(n'''), leq(s(n'''), s(length(t''))))
IF2(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   PROCESS(cons(h'', t''), s(n''')) -> IF1(cons(h'', t''), s(n'''), leq(s(n'''), s(length(t''))))
one new Dependency Pair
is created:


   PROCESS(cons(h'', t''), s(n''')) -> IF1(cons(h'', t''), s(n'''), leq(n''', length(t'')))

The transformation is resulting in one subcycle:


SCC7.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Rewr1.Nar1.Rewr1.Rewr1.Rewr1.Nar1.Nar1.Rewr1.Rewr1.Rewr1.Nar1.Nar1.Inst1.Rewr1:

IF1(cons(h', t'), s(n'), false) -> IF3(cons(h', t'), s(n'), false)
IF2(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))
IF1(cons(h', t'), s(n'), true) -> IF2(cons(h', t'), s(n'), false)
PROCESS(cons(h'', t''), s(n''')) -> IF1(cons(h'', t''), s(n'''), leq(n''', length(t'')))
IF3(cons(h', t'), s(n'), false) -> PROCESS(sndsplit(n', t'), s(n'))

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

Additionally, the following rules can be oriented: 

   sndsplit(0, x) -> x
   sndsplit(s(n), nil) -> nil
   sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(nil) = 0
POL(s(x_1)) = 0
POL(length(x_1)) = 0
POL(IF3(x_1, x_2, x_3)) = x_1
POL(IF1(x_1, x_2, x_3)) = 1 + x_1
POL(0) = 0
POL(IF2(x_1, x_2, x_3)) = x_1
POL(cons(x_1, x_2)) = 1 + x_2
POL(sndsplit(x_1, x_2)) = x_2
POL(true) = 0
POL(PROCESS(x_1, x_2)) = 1 + x_1
POL(leq(x_1, x_2)) = 0
POL(false) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 18.401 seconds.