Term Rewriting System R:
[x, n, h, t, m, pid, st1, in2, st2, in3, st3]
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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st1, in2, st2, in3, st3, m) -> if1(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st1)))
ring(st1, in2, st2, in3, st3, m) -> if2(st1, in2, st2, in3, st3, m, leq(m, length(st2)))
ring(st1, in2, st2, in3, st3, m) -> if5(st1, in2, st2, in3, st3, m, empty(mapf(two, head(in2))))
ring(st1, in2, st2, in3, st3, m) -> if6(st1, in2, st2, in3, st3, m, leq(m, length(st3)))
ring(st1, in2, st2, in3, st3, m) -> if9(st1, in2, st2, in3, st3, m, empty(mapf(three, head(in3))))
if1(st1, in2, st2, in3, st3, m, false) -> ring(sndsplit(m, st1), cons(fstsplit(m, st1), in2), st2, in3, st3, m)
if2(st1, in2, st2, in3, st3, m, true) -> if3(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st2)))
if2(st1, in2, st2, in3, st3, m, false) -> if4(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(two, head(in2)), st2))))
if3(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, sndsplit(m, st2), cons(fstsplit(m, st2), in3), st3, m)
if4(st1, in2, st2, in3, st3, m, false) -> ring(st1, tail(in2), sndsplit(m, app(mapf(two, head(in2)), st2)), cons(fstsplit(m, app(mapf(two, head(in2)), st2)), in3), st3, m)
if5(st1, in2, st2, in3, st3, m, true) -> ring(st1, tail(in2), st2, in3, st3, m)
if6(st1, in2, st2, in3, st3, m, true) -> if7(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st3)))
if6(st1, in2, st2, in3, st3, m, false) -> if8(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(three, head(in3)), st3))))
if7(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, in3, sndsplit(m, st3), m)
if8(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, tail(in3), sndsplit(m, app(mapf(three, head(in3)), st3)), m)
if9(st1, in2, st2, in3, st3, m, true) -> ring(st1, in2, st2, tail(in3), st3, m)

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)
SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)
LEQ(s(n), s(m)) -> LEQ(n, m)
LENGTH(cons(h, t)) -> LENGTH(t)
APP(cons(h, t), x) -> APP(t, x)
MAPF(pid, cons(h, t)) -> APP(f(pid, h), mapf(pid, t))
MAPF(pid, cons(h, t)) -> MAPF(pid, t)
RING(st1, in2, st2, in3, st3, m) -> IF1(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st1)))
RING(st1, in2, st2, in3, st3, m) -> EMPTY(fstsplit(m, st1))
RING(st1, in2, st2, in3, st3, m) -> FSTSPLIT(m, st1)
RING(st1, in2, st2, in3, st3, m) -> IF2(st1, in2, st2, in3, st3, m, leq(m, length(st2)))
RING(st1, in2, st2, in3, st3, m) -> LEQ(m, length(st2))
RING(st1, in2, st2, in3, st3, m) -> LENGTH(st2)
RING(st1, in2, st2, in3, st3, m) -> IF5(st1, in2, st2, in3, st3, m, empty(mapf(two, head(in2))))
RING(st1, in2, st2, in3, st3, m) -> EMPTY(mapf(two, head(in2)))
RING(st1, in2, st2, in3, st3, m) -> MAPF(two, head(in2))
RING(st1, in2, st2, in3, st3, m) -> HEAD(in2)
RING(st1, in2, st2, in3, st3, m) -> IF6(st1, in2, st2, in3, st3, m, leq(m, length(st3)))
RING(st1, in2, st2, in3, st3, m) -> LEQ(m, length(st3))
RING(st1, in2, st2, in3, st3, m) -> LENGTH(st3)
RING(st1, in2, st2, in3, st3, m) -> IF9(st1, in2, st2, in3, st3, m, empty(mapf(three, head(in3))))
RING(st1, in2, st2, in3, st3, m) -> EMPTY(mapf(three, head(in3)))
RING(st1, in2, st2, in3, st3, m) -> MAPF(three, head(in3))
RING(st1, in2, st2, in3, st3, m) -> HEAD(in3)
IF1(st1, in2, st2, in3, st3, m, false) -> RING(sndsplit(m, st1), cons(fstsplit(m, st1), in2), st2, in3, st3, m)
IF1(st1, in2, st2, in3, st3, m, false) -> SNDSPLIT(m, st1)
IF1(st1, in2, st2, in3, st3, m, false) -> FSTSPLIT(m, st1)
IF2(st1, in2, st2, in3, st3, m, true) -> IF3(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st2)))
IF2(st1, in2, st2, in3, st3, m, true) -> EMPTY(fstsplit(m, st2))
IF2(st1, in2, st2, in3, st3, m, true) -> FSTSPLIT(m, st2)
IF2(st1, in2, st2, in3, st3, m, false) -> IF4(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(two, head(in2)), st2))))
IF2(st1, in2, st2, in3, st3, m, false) -> EMPTY(fstsplit(m, app(mapf(two, head(in2)), st2)))
IF2(st1, in2, st2, in3, st3, m, false) -> FSTSPLIT(m, app(mapf(two, head(in2)), st2))
IF2(st1, in2, st2, in3, st3, m, false) -> APP(mapf(two, head(in2)), st2)
IF2(st1, in2, st2, in3, st3, m, false) -> MAPF(two, head(in2))
IF2(st1, in2, st2, in3, st3, m, false) -> HEAD(in2)
IF3(st1, in2, st2, in3, st3, m, false) -> RING(st1, in2, sndsplit(m, st2), cons(fstsplit(m, st2), in3), st3, m)
IF3(st1, in2, st2, in3, st3, m, false) -> SNDSPLIT(m, st2)
IF3(st1, in2, st2, in3, st3, m, false) -> FSTSPLIT(m, st2)
IF4(st1, in2, st2, in3, st3, m, false) -> RING(st1, tail(in2), sndsplit(m, app(mapf(two, head(in2)), st2)), cons(fstsplit(m, app(mapf(two, head(in2)), st2)), in3), st3, m)
IF4(st1, in2, st2, in3, st3, m, false) -> TAIL(in2)
IF4(st1, in2, st2, in3, st3, m, false) -> SNDSPLIT(m, app(mapf(two, head(in2)), st2))
IF4(st1, in2, st2, in3, st3, m, false) -> APP(mapf(two, head(in2)), st2)
IF4(st1, in2, st2, in3, st3, m, false) -> MAPF(two, head(in2))
IF4(st1, in2, st2, in3, st3, m, false) -> HEAD(in2)
IF4(st1, in2, st2, in3, st3, m, false) -> FSTSPLIT(m, app(mapf(two, head(in2)), st2))
IF5(st1, in2, st2, in3, st3, m, true) -> RING(st1, tail(in2), st2, in3, st3, m)
IF5(st1, in2, st2, in3, st3, m, true) -> TAIL(in2)
IF6(st1, in2, st2, in3, st3, m, true) -> IF7(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st3)))
IF6(st1, in2, st2, in3, st3, m, true) -> EMPTY(fstsplit(m, st3))
IF6(st1, in2, st2, in3, st3, m, true) -> FSTSPLIT(m, st3)
IF6(st1, in2, st2, in3, st3, m, false) -> IF8(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(three, head(in3)), st3))))
IF6(st1, in2, st2, in3, st3, m, false) -> EMPTY(fstsplit(m, app(mapf(three, head(in3)), st3)))
IF6(st1, in2, st2, in3, st3, m, false) -> FSTSPLIT(m, app(mapf(three, head(in3)), st3))
IF6(st1, in2, st2, in3, st3, m, false) -> APP(mapf(three, head(in3)), st3)
IF6(st1, in2, st2, in3, st3, m, false) -> MAPF(three, head(in3))
IF6(st1, in2, st2, in3, st3, m, false) -> HEAD(in3)
IF7(st1, in2, st2, in3, st3, m, false) -> RING(st1, in2, st2, in3, sndsplit(m, st3), m)
IF7(st1, in2, st2, in3, st3, m, false) -> SNDSPLIT(m, st3)
IF8(st1, in2, st2, in3, st3, m, false) -> RING(st1, in2, st2, tail(in3), sndsplit(m, app(mapf(three, head(in3)), st3)), m)
IF8(st1, in2, st2, in3, st3, m, false) -> TAIL(in3)
IF8(st1, in2, st2, in3, st3, m, false) -> SNDSPLIT(m, app(mapf(three, head(in3)), st3))
IF8(st1, in2, st2, in3, st3, m, false) -> APP(mapf(three, head(in3)), st3)
IF8(st1, in2, st2, in3, st3, m, false) -> MAPF(three, head(in3))
IF8(st1, in2, st2, in3, st3, m, false) -> HEAD(in3)
IF9(st1, in2, st2, in3, st3, m, true) -> RING(st1, in2, st2, tail(in3), st3, m)
IF9(st1, in2, st2, in3, st3, m, true) -> TAIL(in3)

Furthermore, R contains seven SCCs.


   R
DPs
       →DP Problem 1
Usable Rules (Innermost)
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
       →DP Problem 7
UsableRules


Dependency Pair:

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


Rules:


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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st1, in2, st2, in3, st3, m) -> if1(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st1)))
ring(st1, in2, st2, in3, st3, m) -> if2(st1, in2, st2, in3, st3, m, leq(m, length(st2)))
ring(st1, in2, st2, in3, st3, m) -> if5(st1, in2, st2, in3, st3, m, empty(mapf(two, head(in2))))
ring(st1, in2, st2, in3, st3, m) -> if6(st1, in2, st2, in3, st3, m, leq(m, length(st3)))
ring(st1, in2, st2, in3, st3, m) -> if9(st1, in2, st2, in3, st3, m, empty(mapf(three, head(in3))))
if1(st1, in2, st2, in3, st3, m, false) -> ring(sndsplit(m, st1), cons(fstsplit(m, st1), in2), st2, in3, st3, m)
if2(st1, in2, st2, in3, st3, m, true) -> if3(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st2)))
if2(st1, in2, st2, in3, st3, m, false) -> if4(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(two, head(in2)), st2))))
if3(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, sndsplit(m, st2), cons(fstsplit(m, st2), in3), st3, m)
if4(st1, in2, st2, in3, st3, m, false) -> ring(st1, tail(in2), sndsplit(m, app(mapf(two, head(in2)), st2)), cons(fstsplit(m, app(mapf(two, head(in2)), st2)), in3), st3, m)
if5(st1, in2, st2, in3, st3, m, true) -> ring(st1, tail(in2), st2, in3, st3, m)
if6(st1, in2, st2, in3, st3, m, true) -> if7(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st3)))
if6(st1, in2, st2, in3, st3, m, false) -> if8(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(three, head(in3)), st3))))
if7(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, in3, sndsplit(m, st3), m)
if8(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, tail(in3), sndsplit(m, app(mapf(three, head(in3)), st3)), m)
if9(st1, in2, st2, in3, st3, m, true) -> ring(st1, in2, st2, tail(in3), st3, m)


Strategy:

innermost




As we are in the innermost case, we can delete all 35 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
           →DP Problem 8
Size-Change Principle
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
       →DP Problem 7
UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. FSTSPLIT(s(n), cons(h, t)) -> FSTSPLIT(n, t)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)
s(x1) -> s(x1)

We obtain no new DP problems.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
Usable Rules (Innermost)
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
       →DP Problem 7
UsableRules


Dependency Pair:

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


Rules:


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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st1, in2, st2, in3, st3, m) -> if1(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st1)))
ring(st1, in2, st2, in3, st3, m) -> if2(st1, in2, st2, in3, st3, m, leq(m, length(st2)))
ring(st1, in2, st2, in3, st3, m) -> if5(st1, in2, st2, in3, st3, m, empty(mapf(two, head(in2))))
ring(st1, in2, st2, in3, st3, m) -> if6(st1, in2, st2, in3, st3, m, leq(m, length(st3)))
ring(st1, in2, st2, in3, st3, m) -> if9(st1, in2, st2, in3, st3, m, empty(mapf(three, head(in3))))
if1(st1, in2, st2, in3, st3, m, false) -> ring(sndsplit(m, st1), cons(fstsplit(m, st1), in2), st2, in3, st3, m)
if2(st1, in2, st2, in3, st3, m, true) -> if3(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st2)))
if2(st1, in2, st2, in3, st3, m, false) -> if4(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(two, head(in2)), st2))))
if3(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, sndsplit(m, st2), cons(fstsplit(m, st2), in3), st3, m)
if4(st1, in2, st2, in3, st3, m, false) -> ring(st1, tail(in2), sndsplit(m, app(mapf(two, head(in2)), st2)), cons(fstsplit(m, app(mapf(two, head(in2)), st2)), in3), st3, m)
if5(st1, in2, st2, in3, st3, m, true) -> ring(st1, tail(in2), st2, in3, st3, m)
if6(st1, in2, st2, in3, st3, m, true) -> if7(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st3)))
if6(st1, in2, st2, in3, st3, m, false) -> if8(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(three, head(in3)), st3))))
if7(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, in3, sndsplit(m, st3), m)
if8(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, tail(in3), sndsplit(m, app(mapf(three, head(in3)), st3)), m)
if9(st1, in2, st2, in3, st3, m, true) -> ring(st1, in2, st2, tail(in3), st3, m)


Strategy:

innermost




As we are in the innermost case, we can delete all 35 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
           →DP Problem 9
Size-Change Principle
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
       →DP Problem 7
UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. SNDSPLIT(s(n), cons(h, t)) -> SNDSPLIT(n, t)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)
s(x1) -> s(x1)

We obtain no new DP problems.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
Usable Rules (Innermost)
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
       →DP Problem 7
UsableRules


Dependency Pair:

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


Rules:


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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st1, in2, st2, in3, st3, m) -> if1(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st1)))
ring(st1, in2, st2, in3, st3, m) -> if2(st1, in2, st2, in3, st3, m, leq(m, length(st2)))
ring(st1, in2, st2, in3, st3, m) -> if5(st1, in2, st2, in3, st3, m, empty(mapf(two, head(in2))))
ring(st1, in2, st2, in3, st3, m) -> if6(st1, in2, st2, in3, st3, m, leq(m, length(st3)))
ring(st1, in2, st2, in3, st3, m) -> if9(st1, in2, st2, in3, st3, m, empty(mapf(three, head(in3))))
if1(st1, in2, st2, in3, st3, m, false) -> ring(sndsplit(m, st1), cons(fstsplit(m, st1), in2), st2, in3, st3, m)
if2(st1, in2, st2, in3, st3, m, true) -> if3(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st2)))
if2(st1, in2, st2, in3, st3, m, false) -> if4(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(two, head(in2)), st2))))
if3(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, sndsplit(m, st2), cons(fstsplit(m, st2), in3), st3, m)
if4(st1, in2, st2, in3, st3, m, false) -> ring(st1, tail(in2), sndsplit(m, app(mapf(two, head(in2)), st2)), cons(fstsplit(m, app(mapf(two, head(in2)), st2)), in3), st3, m)
if5(st1, in2, st2, in3, st3, m, true) -> ring(st1, tail(in2), st2, in3, st3, m)
if6(st1, in2, st2, in3, st3, m, true) -> if7(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st3)))
if6(st1, in2, st2, in3, st3, m, false) -> if8(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(three, head(in3)), st3))))
if7(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, in3, sndsplit(m, st3), m)
if8(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, tail(in3), sndsplit(m, app(mapf(three, head(in3)), st3)), m)
if9(st1, in2, st2, in3, st3, m, true) -> ring(st1, in2, st2, tail(in3), st3, m)


Strategy:

innermost




As we are in the innermost case, we can delete all 35 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
           →DP Problem 10
Size-Change Principle
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
       →DP Problem 7
UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. LEQ(s(n), s(m)) -> LEQ(n, m)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
Usable Rules (Innermost)
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
       →DP Problem 7
UsableRules


Dependency Pair:

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


Rules:


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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st1, in2, st2, in3, st3, m) -> if1(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st1)))
ring(st1, in2, st2, in3, st3, m) -> if2(st1, in2, st2, in3, st3, m, leq(m, length(st2)))
ring(st1, in2, st2, in3, st3, m) -> if5(st1, in2, st2, in3, st3, m, empty(mapf(two, head(in2))))
ring(st1, in2, st2, in3, st3, m) -> if6(st1, in2, st2, in3, st3, m, leq(m, length(st3)))
ring(st1, in2, st2, in3, st3, m) -> if9(st1, in2, st2, in3, st3, m, empty(mapf(three, head(in3))))
if1(st1, in2, st2, in3, st3, m, false) -> ring(sndsplit(m, st1), cons(fstsplit(m, st1), in2), st2, in3, st3, m)
if2(st1, in2, st2, in3, st3, m, true) -> if3(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st2)))
if2(st1, in2, st2, in3, st3, m, false) -> if4(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(two, head(in2)), st2))))
if3(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, sndsplit(m, st2), cons(fstsplit(m, st2), in3), st3, m)
if4(st1, in2, st2, in3, st3, m, false) -> ring(st1, tail(in2), sndsplit(m, app(mapf(two, head(in2)), st2)), cons(fstsplit(m, app(mapf(two, head(in2)), st2)), in3), st3, m)
if5(st1, in2, st2, in3, st3, m, true) -> ring(st1, tail(in2), st2, in3, st3, m)
if6(st1, in2, st2, in3, st3, m, true) -> if7(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st3)))
if6(st1, in2, st2, in3, st3, m, false) -> if8(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(three, head(in3)), st3))))
if7(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, in3, sndsplit(m, st3), m)
if8(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, tail(in3), sndsplit(m, app(mapf(three, head(in3)), st3)), m)
if9(st1, in2, st2, in3, st3, m, true) -> ring(st1, in2, st2, tail(in3), st3, m)


Strategy:

innermost




As we are in the innermost case, we can delete all 35 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
           →DP Problem 11
Size-Change Principle
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
       →DP Problem 7
UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. LENGTH(cons(h, t)) -> LENGTH(t)
and get the following Size-Change Graph(s):
{1} , {1}
1>1

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)

We obtain no new DP problems.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
Usable Rules (Innermost)
       →DP Problem 6
UsableRules
       →DP Problem 7
UsableRules


Dependency Pair:

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


Rules:


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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st1, in2, st2, in3, st3, m) -> if1(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st1)))
ring(st1, in2, st2, in3, st3, m) -> if2(st1, in2, st2, in3, st3, m, leq(m, length(st2)))
ring(st1, in2, st2, in3, st3, m) -> if5(st1, in2, st2, in3, st3, m, empty(mapf(two, head(in2))))
ring(st1, in2, st2, in3, st3, m) -> if6(st1, in2, st2, in3, st3, m, leq(m, length(st3)))
ring(st1, in2, st2, in3, st3, m) -> if9(st1, in2, st2, in3, st3, m, empty(mapf(three, head(in3))))
if1(st1, in2, st2, in3, st3, m, false) -> ring(sndsplit(m, st1), cons(fstsplit(m, st1), in2), st2, in3, st3, m)
if2(st1, in2, st2, in3, st3, m, true) -> if3(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st2)))
if2(st1, in2, st2, in3, st3, m, false) -> if4(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(two, head(in2)), st2))))
if3(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, sndsplit(m, st2), cons(fstsplit(m, st2), in3), st3, m)
if4(st1, in2, st2, in3, st3, m, false) -> ring(st1, tail(in2), sndsplit(m, app(mapf(two, head(in2)), st2)), cons(fstsplit(m, app(mapf(two, head(in2)), st2)), in3), st3, m)
if5(st1, in2, st2, in3, st3, m, true) -> ring(st1, tail(in2), st2, in3, st3, m)
if6(st1, in2, st2, in3, st3, m, true) -> if7(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st3)))
if6(st1, in2, st2, in3, st3, m, false) -> if8(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(three, head(in3)), st3))))
if7(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, in3, sndsplit(m, st3), m)
if8(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, tail(in3), sndsplit(m, app(mapf(three, head(in3)), st3)), m)
if9(st1, in2, st2, in3, st3, m, true) -> ring(st1, in2, st2, tail(in3), st3, m)


Strategy:

innermost




As we are in the innermost case, we can delete all 35 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
           →DP Problem 12
Size-Change Principle
       →DP Problem 6
UsableRules
       →DP Problem 7
UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. APP(cons(h, t), x) -> APP(t, x)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2=2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2=2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)

We obtain no new DP problems.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
Usable Rules (Innermost)
       →DP Problem 7
UsableRules


Dependency Pair:

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


Rules:


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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st1, in2, st2, in3, st3, m) -> if1(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st1)))
ring(st1, in2, st2, in3, st3, m) -> if2(st1, in2, st2, in3, st3, m, leq(m, length(st2)))
ring(st1, in2, st2, in3, st3, m) -> if5(st1, in2, st2, in3, st3, m, empty(mapf(two, head(in2))))
ring(st1, in2, st2, in3, st3, m) -> if6(st1, in2, st2, in3, st3, m, leq(m, length(st3)))
ring(st1, in2, st2, in3, st3, m) -> if9(st1, in2, st2, in3, st3, m, empty(mapf(three, head(in3))))
if1(st1, in2, st2, in3, st3, m, false) -> ring(sndsplit(m, st1), cons(fstsplit(m, st1), in2), st2, in3, st3, m)
if2(st1, in2, st2, in3, st3, m, true) -> if3(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st2)))
if2(st1, in2, st2, in3, st3, m, false) -> if4(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(two, head(in2)), st2))))
if3(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, sndsplit(m, st2), cons(fstsplit(m, st2), in3), st3, m)
if4(st1, in2, st2, in3, st3, m, false) -> ring(st1, tail(in2), sndsplit(m, app(mapf(two, head(in2)), st2)), cons(fstsplit(m, app(mapf(two, head(in2)), st2)), in3), st3, m)
if5(st1, in2, st2, in3, st3, m, true) -> ring(st1, tail(in2), st2, in3, st3, m)
if6(st1, in2, st2, in3, st3, m, true) -> if7(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st3)))
if6(st1, in2, st2, in3, st3, m, false) -> if8(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(three, head(in3)), st3))))
if7(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, in3, sndsplit(m, st3), m)
if8(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, tail(in3), sndsplit(m, app(mapf(three, head(in3)), st3)), m)
if9(st1, in2, st2, in3, st3, m, true) -> ring(st1, in2, st2, tail(in3), st3, m)


Strategy:

innermost




As we are in the innermost case, we can delete all 35 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
           →DP Problem 13
Size-Change Principle
       →DP Problem 7
UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. MAPF(pid, cons(h, t)) -> MAPF(pid, t)
and get the following Size-Change Graph(s):
{1} , {1}
1=1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1=1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)

We obtain no new DP problems.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
       →DP Problem 7
Usable Rules (Innermost)


Dependency Pairs:

IF4(st1, in2, st2, in3, st3, m, false) -> RING(st1, tail(in2), sndsplit(m, app(mapf(two, head(in2)), st2)), cons(fstsplit(m, app(mapf(two, head(in2)), st2)), in3), st3, m)
IF2(st1, in2, st2, in3, st3, m, false) -> IF4(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(two, head(in2)), st2))))
IF8(st1, in2, st2, in3, st3, m, false) -> RING(st1, in2, st2, tail(in3), sndsplit(m, app(mapf(three, head(in3)), st3)), m)
IF6(st1, in2, st2, in3, st3, m, false) -> IF8(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(three, head(in3)), st3))))
IF9(st1, in2, st2, in3, st3, m, true) -> RING(st1, in2, st2, tail(in3), st3, m)
RING(st1, in2, st2, in3, st3, m) -> IF9(st1, in2, st2, in3, st3, m, empty(mapf(three, head(in3))))
IF7(st1, in2, st2, in3, st3, m, false) -> RING(st1, in2, st2, in3, sndsplit(m, st3), m)
IF6(st1, in2, st2, in3, st3, m, true) -> IF7(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st3)))
RING(st1, in2, st2, in3, st3, m) -> IF6(st1, in2, st2, in3, st3, m, leq(m, length(st3)))
IF5(st1, in2, st2, in3, st3, m, true) -> RING(st1, tail(in2), st2, in3, st3, m)
RING(st1, in2, st2, in3, st3, m) -> IF5(st1, in2, st2, in3, st3, m, empty(mapf(two, head(in2))))
IF3(st1, in2, st2, in3, st3, m, false) -> RING(st1, in2, sndsplit(m, st2), cons(fstsplit(m, st2), in3), st3, m)
IF2(st1, in2, st2, in3, st3, m, true) -> IF3(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st2)))
RING(st1, in2, st2, in3, st3, m) -> IF2(st1, in2, st2, in3, st3, m, leq(m, length(st2)))
IF1(st1, in2, st2, in3, st3, m, false) -> RING(sndsplit(m, st1), cons(fstsplit(m, st1), in2), st2, in3, st3, m)
RING(st1, in2, st2, in3, st3, m) -> IF1(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st1)))


Rules:


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))
mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st1, in2, st2, in3, st3, m) -> if1(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st1)))
ring(st1, in2, st2, in3, st3, m) -> if2(st1, in2, st2, in3, st3, m, leq(m, length(st2)))
ring(st1, in2, st2, in3, st3, m) -> if5(st1, in2, st2, in3, st3, m, empty(mapf(two, head(in2))))
ring(st1, in2, st2, in3, st3, m) -> if6(st1, in2, st2, in3, st3, m, leq(m, length(st3)))
ring(st1, in2, st2, in3, st3, m) -> if9(st1, in2, st2, in3, st3, m, empty(mapf(three, head(in3))))
if1(st1, in2, st2, in3, st3, m, false) -> ring(sndsplit(m, st1), cons(fstsplit(m, st1), in2), st2, in3, st3, m)
if2(st1, in2, st2, in3, st3, m, true) -> if3(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st2)))
if2(st1, in2, st2, in3, st3, m, false) -> if4(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(two, head(in2)), st2))))
if3(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, sndsplit(m, st2), cons(fstsplit(m, st2), in3), st3, m)
if4(st1, in2, st2, in3, st3, m, false) -> ring(st1, tail(in2), sndsplit(m, app(mapf(two, head(in2)), st2)), cons(fstsplit(m, app(mapf(two, head(in2)), st2)), in3), st3, m)
if5(st1, in2, st2, in3, st3, m, true) -> ring(st1, tail(in2), st2, in3, st3, m)
if6(st1, in2, st2, in3, st3, m, true) -> if7(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st3)))
if6(st1, in2, st2, in3, st3, m, false) -> if8(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(three, head(in3)), st3))))
if7(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, in3, sndsplit(m, st3), m)
if8(st1, in2, st2, in3, st3, m, false) -> ring(st1, in2, st2, tail(in3), sndsplit(m, app(mapf(three, head(in3)), st3)), m)
if9(st1, in2, st2, in3, st3, m, true) -> ring(st1, in2, st2, tail(in3), st3, m)


Strategy:

innermost




As we are in the innermost case, we can delete all 16 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
       →DP Problem 7
UsableRules
           →DP Problem 14
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

IF4(st1, in2, st2, in3, st3, m, false) -> RING(st1, tail(in2), sndsplit(m, app(mapf(two, head(in2)), st2)), cons(fstsplit(m, app(mapf(two, head(in2)), st2)), in3), st3, m)
IF2(st1, in2, st2, in3, st3, m, false) -> IF4(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(two, head(in2)), st2))))
IF8(st1, in2, st2, in3, st3, m, false) -> RING(st1, in2, st2, tail(in3), sndsplit(m, app(mapf(three, head(in3)), st3)), m)
IF6(st1, in2, st2, in3, st3, m, false) -> IF8(st1, in2, st2, in3, st3, m, empty(fstsplit(m, app(mapf(three, head(in3)), st3))))
IF9(st1, in2, st2, in3, st3, m, true) -> RING(st1, in2, st2, tail(in3), st3, m)
RING(st1, in2, st2, in3, st3, m) -> IF9(st1, in2, st2, in3, st3, m, empty(mapf(three, head(in3))))
IF7(st1, in2, st2, in3, st3, m, false) -> RING(st1, in2, st2, in3, sndsplit(m, st3), m)
IF6(st1, in2, st2, in3, st3, m, true) -> IF7(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st3)))
RING(st1, in2, st2, in3, st3, m) -> IF6(st1, in2, st2, in3, st3, m, leq(m, length(st3)))
IF5(st1, in2, st2, in3, st3, m, true) -> RING(st1, tail(in2), st2, in3, st3, m)
RING(st1, in2, st2, in3, st3, m) -> IF5(st1, in2, st2, in3, st3, m, empty(mapf(two, head(in2))))
IF3(st1, in2, st2, in3, st3, m, false) -> RING(st1, in2, sndsplit(m, st2), cons(fstsplit(m, st2), in3), st3, m)
IF2(st1, in2, st2, in3, st3, m, true) -> IF3(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st2)))
RING(st1, in2, st2, in3, st3, m) -> IF2(st1, in2, st2, in3, st3, m, leq(m, length(st2)))
IF1(st1, in2, st2, in3, st3, m, false) -> RING(sndsplit(m, st1), cons(fstsplit(m, st1), in2), st2, in3, st3, m)
RING(st1, in2, st2, in3, st3, m) -> IF1(st1, in2, st2, in3, st3, m, empty(fstsplit(m, st1)))


Rules:


mapf(pid, nil) -> nil
mapf(pid, cons(h, t)) -> app(f(pid, h), mapf(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
fstsplit(0, x) -> nil
fstsplit(s(n), nil) -> nil
sndsplit(0, x) -> x
sndsplit(s(n), nil) -> nil
sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
app(nil, x) -> x
app(cons(h, t), x) -> cons(h, app(t, x))
empty(cons(h, t)) -> false
empty(nil) -> true
length(cons(h, t)) -> s(length(t))
length(nil) -> 0
leq(0, m) -> true
leq(s(n), 0) -> false
leq(s(n), s(m)) -> leq(n, m)


Strategy:

innermost



The Proof could not be continued due to a Timeout.
Innermost Termination of R could not be shown.
Duration:
1:00 minutes