Termination Proof using AProVE

Term Rewriting System R:
[x, n, h, t, m, pid, st₁, in₂, st₂, in₃, st₃]
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))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

Termination of R to be shown.

     ↳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)
MAP_F(pid, cons(h, t)) -> APP(f(pid, h), map_f(pid, t))
MAP_F(pid, cons(h, t)) -> MAP_F(pid, t)
RING(st₁, in₂, st₂, in₃, st₃, m) -> IF₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
RING(st₁, in₂, st₂, in₃, st₃, m) -> EMPTY(fstsplit(m, st₁))
RING(st₁, in₂, st₂, in₃, st₃, m) -> FSTSPLIT(m, st₁)
RING(st₁, in₂, st₂, in₃, st₃, m) -> IF₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
RING(st₁, in₂, st₂, in₃, st₃, m) -> LEQ(m, length(st₂))
RING(st₁, in₂, st₂, in₃, st₃, m) -> LENGTH(st₂)
RING(st₁, in₂, st₂, in₃, st₃, m) -> IF₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
RING(st₁, in₂, st₂, in₃, st₃, m) -> EMPTY(map_f(two, head(in₂)))
RING(st₁, in₂, st₂, in₃, st₃, m) -> MAP_F(two, head(in₂))
RING(st₁, in₂, st₂, in₃, st₃, m) -> HEAD(in₂)
RING(st₁, in₂, st₂, in₃, st₃, m) -> IF₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
RING(st₁, in₂, st₂, in₃, st₃, m) -> LEQ(m, length(st₃))
RING(st₁, in₂, st₂, in₃, st₃, m) -> LENGTH(st₃)
RING(st₁, in₂, st₂, in₃, st₃, m) -> IF₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
RING(st₁, in₂, st₂, in₃, st₃, m) -> EMPTY(map_f(three, head(in₃)))
RING(st₁, in₂, st₂, in₃, st₃, m) -> MAP_F(three, head(in₃))
RING(st₁, in₂, st₂, in₃, st₃, m) -> HEAD(in₃)
IF₁(st₁, in₂, st₂, in₃, st₃, m, false) -> RING(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
IF₁(st₁, in₂, st₂, in₃, st₃, m, false) -> SNDSPLIT(m, st₁)
IF₁(st₁, in₂, st₂, in₃, st₃, m, false) -> FSTSPLIT(m, st₁)
IF₂(st₁, in₂, st₂, in₃, st₃, m, true) -> IF₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
IF₂(st₁, in₂, st₂, in₃, st₃, m, true) -> EMPTY(fstsplit(m, st₂))
IF₂(st₁, in₂, st₂, in₃, st₃, m, true) -> FSTSPLIT(m, st₂)
IF₂(st₁, in₂, st₂, in₃, st₃, m, false) -> IF₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
IF₂(st₁, in₂, st₂, in₃, st₃, m, false) -> EMPTY(fstsplit(m, app(map_f(two, head(in₂)), st₂)))
IF₂(st₁, in₂, st₂, in₃, st₃, m, false) -> FSTSPLIT(m, app(map_f(two, head(in₂)), st₂))
IF₂(st₁, in₂, st₂, in₃, st₃, m, false) -> APP(map_f(two, head(in₂)), st₂)
IF₂(st₁, in₂, st₂, in₃, st₃, m, false) -> MAP_F(two, head(in₂))
IF₂(st₁, in₂, st₂, in₃, st₃, m, false) -> HEAD(in₂)
IF₃(st₁, in₂, st₂, in₃, st₃, m, false) -> RING(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
IF₃(st₁, in₂, st₂, in₃, st₃, m, false) -> SNDSPLIT(m, st₂)
IF₃(st₁, in₂, st₂, in₃, st₃, m, false) -> FSTSPLIT(m, st₂)
IF₄(st₁, in₂, st₂, in₃, st₃, m, false) -> RING(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
IF₄(st₁, in₂, st₂, in₃, st₃, m, false) -> TAIL(in₂)
IF₄(st₁, in₂, st₂, in₃, st₃, m, false) -> SNDSPLIT(m, app(map_f(two, head(in₂)), st₂))
IF₄(st₁, in₂, st₂, in₃, st₃, m, false) -> APP(map_f(two, head(in₂)), st₂)
IF₄(st₁, in₂, st₂, in₃, st₃, m, false) -> MAP_F(two, head(in₂))
IF₄(st₁, in₂, st₂, in₃, st₃, m, false) -> HEAD(in₂)
IF₄(st₁, in₂, st₂, in₃, st₃, m, false) -> FSTSPLIT(m, app(map_f(two, head(in₂)), st₂))
IF₅(st₁, in₂, st₂, in₃, st₃, m, true) -> RING(st₁, tail(in₂), st₂, in₃, st₃, m)
IF₅(st₁, in₂, st₂, in₃, st₃, m, true) -> TAIL(in₂)
IF₆(st₁, in₂, st₂, in₃, st₃, m, true) -> IF₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
IF₆(st₁, in₂, st₂, in₃, st₃, m, true) -> EMPTY(fstsplit(m, st₃))
IF₆(st₁, in₂, st₂, in₃, st₃, m, true) -> FSTSPLIT(m, st₃)
IF₆(st₁, in₂, st₂, in₃, st₃, m, false) -> IF₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
IF₆(st₁, in₂, st₂, in₃, st₃, m, false) -> EMPTY(fstsplit(m, app(map_f(three, head(in₃)), st₃)))
IF₆(st₁, in₂, st₂, in₃, st₃, m, false) -> FSTSPLIT(m, app(map_f(three, head(in₃)), st₃))
IF₆(st₁, in₂, st₂, in₃, st₃, m, false) -> APP(map_f(three, head(in₃)), st₃)
IF₆(st₁, in₂, st₂, in₃, st₃, m, false) -> MAP_F(three, head(in₃))
IF₆(st₁, in₂, st₂, in₃, st₃, m, false) -> HEAD(in₃)
IF₇(st₁, in₂, st₂, in₃, st₃, m, false) -> RING(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
IF₇(st₁, in₂, st₂, in₃, st₃, m, false) -> SNDSPLIT(m, st₃)
IF₈(st₁, in₂, st₂, in₃, st₃, m, false) -> RING(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
IF₈(st₁, in₂, st₂, in₃, st₃, m, false) -> TAIL(in₃)
IF₈(st₁, in₂, st₂, in₃, st₃, m, false) -> SNDSPLIT(m, app(map_f(three, head(in₃)), st₃))
IF₈(st₁, in₂, st₂, in₃, st₃, m, false) -> APP(map_f(three, head(in₃)), st₃)
IF₈(st₁, in₂, st₂, in₃, st₃, m, false) -> MAP_F(three, head(in₃))
IF₈(st₁, in₂, st₂, in₃, st₃, m, false) -> HEAD(in₃)
IF₉(st₁, in₂, st₂, in₃, st₃, m, true) -> RING(st₁, in₂, st₂, tail(in₃), st₃, m)
IF₉(st₁, in₂, st₂, in₃, st₃, m, true) -> TAIL(in₃)

Furthermore, R contains seven SCCs.

     ↳DPs

       →DP Problem 1

         ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

The following dependency pair can be strictly oriented:

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

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(cons(x₁, x₂)) = 0

POL(FSTSPLIT(x₁, x₂)) = x₁

POL(s(x₁)) = 1 + x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 8

             ↳Dependency Graph

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

Dependency Pair:

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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polynomial Ordering

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

The following dependency pair can be strictly oriented:

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

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(SNDSPLIT(x₁, x₂)) = x₁

POL(cons(x₁, x₂)) = 0

POL(s(x₁)) = 1 + x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 9

             ↳Dependency Graph

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

Dependency Pair:

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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polynomial Ordering

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

The following dependency pair can be strictly oriented:

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

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(LEQ(x₁, x₂)) = x₁

POL(s(x₁)) = 1 + x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 10

             ↳Dependency Graph

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

Dependency Pair:

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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polynomial Ordering

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

The following dependency pair can be strictly oriented:

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

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(cons(x₁, x₂)) = 1 + x₂

POL(LENGTH(x₁)) = x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

           →DP Problem 11

             ↳Dependency Graph

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

Dependency Pair:

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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polynomial Ordering

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

The following dependency pair can be strictly oriented:

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

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(cons(x₁, x₂)) = 1 + x₂

POL(APP(x₁, x₂)) = x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

           →DP Problem 12

             ↳Dependency Graph

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining

Dependency Pair:

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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polynomial Ordering

       →DP Problem 7

         ↳Remaining

Dependency Pair:

MAP_F(pid, cons(h, t)) -> MAP_F(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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

The following dependency pair can be strictly oriented:

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

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(MAP_F(x₁, x₂)) = x₂

POL(cons(x₁, x₂)) = 1 + x₂

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

           →DP Problem 13

             ↳Dependency Graph

       →DP Problem 7

         ↳Remaining

Dependency Pair:

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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

       →DP Problem 6

         ↳Polo

       →DP Problem 7

         ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

IF₄(st₁, in₂, st₂, in₃, st₃, m, false) -> RING(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
IF₂(st₁, in₂, st₂, in₃, st₃, m, false) -> IF₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
IF₈(st₁, in₂, st₂, in₃, st₃, m, false) -> RING(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
IF₆(st₁, in₂, st₂, in₃, st₃, m, false) -> IF₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
IF₉(st₁, in₂, st₂, in₃, st₃, m, true) -> RING(st₁, in₂, st₂, tail(in₃), st₃, m)
RING(st₁, in₂, st₂, in₃, st₃, m) -> IF₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
IF₇(st₁, in₂, st₂, in₃, st₃, m, false) -> RING(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
IF₆(st₁, in₂, st₂, in₃, st₃, m, true) -> IF₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
RING(st₁, in₂, st₂, in₃, st₃, m) -> IF₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
IF₅(st₁, in₂, st₂, in₃, st₃, m, true) -> RING(st₁, tail(in₂), st₂, in₃, st₃, m)
RING(st₁, in₂, st₂, in₃, st₃, m) -> IF₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
IF₃(st₁, in₂, st₂, in₃, st₃, m, false) -> RING(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
IF₂(st₁, in₂, st₂, in₃, st₃, m, true) -> IF₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
RING(st₁, in₂, st₂, in₃, st₃, m) -> IF₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
IF₁(st₁, in₂, st₂, in₃, st₃, m, false) -> RING(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
RING(st₁, in₂, st₂, in₃, st₃, m) -> IF₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))

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))
map_f(pid, nil) -> nil
map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
head(cons(h, t)) -> h
tail(cons(h, t)) -> t
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₁(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₁)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₂(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₂)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₅(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(two, head(in₂))))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₆(st₁, in₂, st₂, in₃, st₃, m, leq(m, length(st₃)))
ring(st₁, in₂, st₂, in₃, st₃, m) -> if₉(st₁, in₂, st₂, in₃, st₃, m, empty(map_f(three, head(in₃))))
if₁(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(sndsplit(m, st₁), cons(fstsplit(m, st₁), in₂), st₂, in₃, st₃, m)
if₂(st₁, in₂, st₂, in₃, st₃, m, true) -> if₃(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₂)))
if₂(st₁, in₂, st₂, in₃, st₃, m, false) -> if₄(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(two, head(in₂)), st₂))))
if₃(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, sndsplit(m, st₂), cons(fstsplit(m, st₂), in₃), st₃, m)
if₄(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, tail(in₂), sndsplit(m, app(map_f(two, head(in₂)), st₂)), cons(fstsplit(m, app(map_f(two, head(in₂)), st₂)), in₃), st₃, m)
if₅(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, tail(in₂), st₂, in₃, st₃, m)
if₆(st₁, in₂, st₂, in₃, st₃, m, true) -> if₇(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, st₃)))
if₆(st₁, in₂, st₂, in₃, st₃, m, false) -> if₈(st₁, in₂, st₂, in₃, st₃, m, empty(fstsplit(m, app(map_f(three, head(in₃)), st₃))))
if₇(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, in₃, sndsplit(m, st₃), m)
if₈(st₁, in₂, st₂, in₃, st₃, m, false) -> ring(st₁, in₂, st₂, tail(in₃), sndsplit(m, app(map_f(three, head(in₃)), st₃)), m)
if₉(st₁, in₂, st₂, in₃, st₃, m, true) -> ring(st₁, in₂, st₂, tail(in₃), st₃, m)

Termination of R could not be shown.
Duration:
0:56 minutes

POL(cons(x₁, x₂))	= 0
POL(FSTSPLIT(x₁, x₂))	= x₁
POL(s(x₁))	= 1 + x₁

POL(SNDSPLIT(x₁, x₂))	= x₁
POL(cons(x₁, x₂))	= 0
POL(s(x₁))	= 1 + x₁

POL(cons(x₁, x₂))	= 1 + x₂
POL(LENGTH(x₁))	= x₁

POL(cons(x₁, x₂))	= 1 + x₂
POL(APP(x₁, x₂))	= x₁

POL(MAP_F(x₁, x₂))	= x₂
POL(cons(x₁, x₂))	= 1 + x₂