Termination w.r.t. Q proof of /tmp/tmp

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, in_2, st_2, tail(in_3), st_3, m)
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_2)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(two, head(in_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_2))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_1)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_2)
IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_3)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
LENGTH(cons(h, t)) → LENGTH(t)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, tail(in_2), st_2, in_3, st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_3)
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → IF_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
MAP_F(pid, cons(h, t)) → APP(f(pid, h), map_f(pid, t))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(two, head(in_2)), st_2)))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → IF_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(three, head(in_3)), st_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(three, head(in_3)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → IF_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(three, head(in_3)), st_3))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_2)
APP(cons(h, t), x) → APP(t, x)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_2)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_1)
LEQ(s(n), s(m)) → LEQ(n, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_3))
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(three, head(in_3)), st_3)))
RING(st_1, in_2, st_2, in_3, st_3, m) → FSTSPLIT(m, st_1)
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(two, head(in_2))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_2)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_2)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(fstsplit(m, st_1))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → IF_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(three, head(in_3))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(two, head(in_2)), st_2))
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_2))
MAP_F(pid, cons(h, t)) → MAP_F(pid, t)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_3)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → RING(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_3)

The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, in_2, st_2, tail(in_3), st_3, m)
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_2)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(two, head(in_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_2))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_1)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_2)
IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → TAIL(in_3)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
LENGTH(cons(h, t)) → LENGTH(t)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(three, head(in_3))
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, tail(in_2), st_2, in_3, st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_3)
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → IF_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
MAP_F(pid, cons(h, t)) → APP(f(pid, h), map_f(pid, t))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(two, head(in_2)), st_2)))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → IF_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(three, head(in_3)), st_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(three, head(in_3)), st_3)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(map_f(three, head(in_3)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → IF_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(three, head(in_3)), st_3))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, st_2)
APP(cons(h, t), x) → APP(t, x)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_2)
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → FSTSPLIT(m, st_2)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → APP(map_f(two, head(in_2)), st_2)
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_1)
LEQ(s(n), s(m)) → LEQ(n, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → LEQ(m, length(st_3))
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_2)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → EMPTY(fstsplit(m, app(map_f(three, head(in_3)), st_3)))
RING(st_1, in_2, st_2, in_3, st_3, m) → FSTSPLIT(m, st_1)
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(two, head(in_2))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_3))
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_2)
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → TAIL(in_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → FSTSPLIT(m, app(map_f(two, head(in_2)), st_2))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
RING(st_1, in_2, st_2, in_3, st_3, m) → LENGTH(st_2)
RING(st_1, in_2, st_2, in_3, st_3, m) → EMPTY(fstsplit(m, st_1))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → IF_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
RING(st_1, in_2, st_2, in_3, st_3, m) → MAP_F(three, head(in_3))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, app(map_f(two, head(in_2)), st_2))
IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → EMPTY(fstsplit(m, st_2))
MAP_F(pid, cons(h, t)) → MAP_F(pid, t)
RING(st_1, in_2, st_2, in_3, st_3, m) → HEAD(in_3)
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → HEAD(in_3)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → MAP_F(two, head(in_2))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → RING(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → SNDSPLIT(m, st_3)

The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 7 SCCs with 45 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP(cons(h, t), x) → APP(t, x)

The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

APP(cons(h, t), x) → APP(t, x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

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

The value of delta used in the strict ordering is 4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MAP_F(pid, cons(h, t)) → MAP_F(pid, t)

The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MAP_F(pid, cons(h, t)) → MAP_F(pid, t)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

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

The value of delta used in the strict ordering is 4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LENGTH(cons(h, t)) → LENGTH(t)

The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

LENGTH(cons(h, t)) → LENGTH(t)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

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

The value of delta used in the strict ordering is 4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LEQ(s(n), s(m)) → LEQ(n, m)

The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

LEQ(s(n), s(m)) → LEQ(n, m)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(LEQ(x₁, x₂)) = (3)x_2
POL(s(x₁)) = 4 + (2)x_1

The value of delta used in the strict ordering is 12.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)

The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

SNDSPLIT(s(n), cons(h, t)) → SNDSPLIT(n, t)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(cons(x₁, x₂)) = (4)x_2
POL(SNDSPLIT(x₁, x₂)) = (4)x_1 + (3)x_2
POL(s(x₁)) = 1 + (4)x_1

The value of delta used in the strict ordering is 4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)

The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

FSTSPLIT(s(n), cons(h, t)) → FSTSPLIT(n, t)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(cons(x₁, x₂)) = (4)x_2
POL(s(x₁)) = 1 + (4)x_1
POL(FSTSPLIT(x₁, x₂)) = (4)x_1 + (3)x_2

The value of delta used in the strict ordering is 4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF_2(st_1, in_2, st_2, in_3, st_3, m, true) → IF_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
IF_9(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, in_2, st_2, tail(in_3), st_3, m)
IF_5(st_1, in_2, st_2, in_3, st_3, m, true) → RING(st_1, tail(in_2), st_2, in_3, st_3, m)
IF_4(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, true) → IF_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
IF_6(st_1, in_2, st_2, in_3, st_3, m, false) → IF_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
IF_3(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
IF_7(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
IF_2(st_1, in_2, st_2, in_3, st_3, m, false) → IF_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
IF_8(st_1, in_2, st_2, in_3, st_3, m, false) → RING(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
RING(st_1, in_2, st_2, in_3, st_3, m) → IF_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
IF_1(st_1, in_2, st_2, in_3, st_3, m, false) → RING(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)

The TRS R consists of the following 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_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.