TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60001 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (4291ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (61ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4 (33ms).
 | – Problem 4 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (70ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (66ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (66ms), PolynomialLinearRange4 (1443ms), DependencyGraph (98ms), PolynomialLinearRange4 (2453ms), DependencyGraph (107ms), PolynomialLinearRange4 (2472ms), DependencyGraph (68ms), ReductionPairSAT (timeout)].
 | – Problem 5 was processed with processor PolynomialLinearRange4 (13ms).
 | – Problem 6 was processed with processor PolynomialLinearRange4 (116ms).
 | – Problem 7 was processed with processor PolynomialLinearRange4 (98ms).
 | – Problem 8 was processed with processor PolynomialLinearRange4 (89ms).

The following open problems remain:

Open Dependency Pair Problem 4

Dependency Pairs

U221#(true, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, tail(in_2), st_2, in_3, st_3, m)U231#(true, st_3, st_2, in_2, in_3, st_1, m) → U232#(empty(fstsplit(m, st_3)), st_3, st_2, in_2, in_3, st_1, m)
ring#(st_1, in_2, st_2, in_3, st_3, m) → U241#(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)U242#(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U201#(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)ring#(st_1, in_2, st_2, in_3, st_3, m) → U191#(empty(fstsplit(m, st_1)), st_3, st_2, in_2, in_3, st_1, m)
U191#(false, st_3, st_2, in_2, in_3, st_1, m) → ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)U212#(false, st_3, st_2, in_2, in_3, st_1, m) → 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)
U232#(false, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)ring#(st_1, in_2, st_2, in_3, st_3, m) → U231#(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)
ring#(st_1, in_2, st_2, in_3, st_3, m) → U221#(empty(map_f(two, head(in_2))), st_3, st_2, in_2, in_3, st_1, m)U241#(false, st_3, st_2, in_2, in_3, st_1, m) → U242#(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_3, st_2, in_2, in_3, st_1, m)
U202#(false, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)ring#(st_1, in_2, st_2, in_3, st_3, m) → U211#(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)
U251#(true, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, in_2, st_2, tail(in_3), st_3, m)ring#(st_1, in_2, st_2, in_3, st_3, m) → U251#(empty(map_f(three, head(in_3))), st_3, st_2, in_2, in_3, st_1, m)
U211#(false, st_3, st_2, in_2, in_3, st_1, m) → U212#(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_3, st_2, in_2, in_3, st_1, m)U201#(true, st_3, st_2, in_2, in_3, st_1, m) → U202#(empty(fstsplit(m, st_2)), st_3, st_2, in_2, in_3, st_1, m)

Rewrite Rules

fstsplit(0, x) → nilfstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))sndsplit(0, x) → x
sndsplit(s(n), nil) → nilsndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → trueempty(cons(h, t)) → false
leq(0, m) → trueleq(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)) → tring(st_1, in_2, st_2, in_3, st_3, m) → U191(empty(fstsplit(m, st_1)), st_3, st_2, in_2, in_3, st_1, m)
U191(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U201(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)
U201(true, st_3, st_2, in_2, in_3, st_1, m) → U202(empty(fstsplit(m, st_2)), st_3, st_2, in_2, in_3, st_1, m)U202(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U211(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)U211(false, st_3, st_2, in_2, in_3, st_1, m) → U212(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_3, st_2, in_2, in_3, st_1, m)
U212(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U221(empty(map_f(two, head(in_2))), st_3, st_2, in_2, in_3, st_1, m)
U221(true, st_3, st_2, in_2, in_3, st_1, m) → 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) → U231(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)
U231(true, st_3, st_2, in_2, in_3, st_1, m) → U232(empty(fstsplit(m, st_3)), st_3, st_2, in_2, in_3, st_1, m)U232(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U241(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)U241(false, st_3, st_2, in_2, in_3, st_1, m) → U242(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_3, st_2, in_2, in_3, st_1, m)
U242(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U251(empty(map_f(three, head(in_3))), st_3, st_2, in_2, in_3, st_1, m)
U251(true, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Original Signature

Termination of terms over the following signature is verified: f, ring, app, map_f, leq, true, tail, fstsplit, two, 0, s, sndsplit, three, empty, length, false, head, nil, cons

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

U212#(false, st_3, st_2, in_2, in_3, st_1, m) → T(m)U221#(true, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, tail(in_2), st_2, in_3, st_3, m)
U231#(true, st_3, st_2, in_2, in_3, st_1, m) → empty#(fstsplit(m, st_3))ring#(st_1, in_2, st_2, in_3, st_3, m) → map_f#(two, head(in_2))
ring#(st_1, in_2, st_2, in_3, st_3, m) → empty#(fstsplit(m, st_1))leq#(s(n), s(m)) → leq#(n, m)
U241#(false, st_3, st_2, in_2, in_3, st_1, m) → head#(in_3)U191#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_1)
U212#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_3)U211#(false, st_3, st_2, in_2, in_3, st_1, m) → app#(map_f(two, head(in_2)), st_2)
U242#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_2)ring#(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) → map_f#(three, head(in_3))U241#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_3)
U212#(false, st_3, st_2, in_2, in_3, st_1, m) → head#(in_2)U241#(false, st_3, st_2, in_2, in_3, st_1, m) → empty#(fstsplit(m, app(map_f(three, head(in_3)), st_3)))
U201#(true, st_3, st_2, in_2, in_3, st_1, m) → T(m)U251#(true, st_3, st_2, in_2, in_3, st_1, m) → T(in_2)
map_f#(pid, cons(h, t)) → app#(f(pid, h), map_f(pid, t))ring#(st_1, in_2, st_2, in_3, st_3, m) → U191#(empty(fstsplit(m, st_1)), st_3, st_2, in_2, in_3, st_1, m)
U232#(false, st_3, st_2, in_2, in_3, st_1, m) → T(in_3)U232#(false, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
ring#(st_1, in_2, st_2, in_3, st_3, m) → U221#(empty(map_f(two, head(in_2))), st_3, st_2, in_2, in_3, st_1, m)U221#(true, st_3, st_2, in_2, in_3, st_1, m) → T(st_3)
U241#(false, st_3, st_2, in_2, in_3, st_1, m) → T(in_3)U201#(true, st_3, st_2, in_2, in_3, st_1, m) → U202#(empty(fstsplit(m, st_2)), st_3, st_2, in_2, in_3, st_1, m)
U212#(false, st_3, st_2, in_2, in_3, st_1, m) → map_f#(two, head(in_2))map_f#(pid, cons(h, t)) → map_f#(pid, t)
U232#(false, st_3, st_2, in_2, in_3, st_1, m) → T(in_2)U242#(false, st_3, st_2, in_2, in_3, st_1, m) → T(m)
U232#(false, st_3, st_2, in_2, in_3, st_1, m) → T(m)U211#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_2)
U211#(false, st_3, st_2, in_2, in_3, st_1, m) → T(m)U202#(false, st_3, st_2, in_2, in_3, st_1, m) → T(in_2)
U202#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_2)U242#(false, st_3, st_2, in_2, in_3, st_1, m) → app#(map_f(three, head(in_3)), st_3)
U242#(false, st_3, st_2, in_2, in_3, st_1, m) → sndsplit#(m, app(map_f(three, head(in_3)), st_3))ring#(st_1, in_2, st_2, in_3, st_3, m) → leq#(m, length(st_3))
U212#(false, st_3, st_2, in_2, in_3, st_1, m) → fstsplit#(m, app(map_f(two, head(in_2)), st_2))ring#(st_1, in_2, st_2, in_3, st_3, m) → length#(st_2)
U242#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_3)U251#(true, st_3, st_2, in_2, in_3, st_1, m) → T(in_3)
fstsplit#(s(n), cons(h, t)) → fstsplit#(n, t)ring#(st_1, in_2, st_2, in_3, st_3, m) → U201#(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)
U231#(true, st_3, st_2, in_2, in_3, st_1, m) → fstsplit#(m, st_3)ring#(st_1, in_2, st_2, in_3, st_3, m) → length#(st_3)
U221#(true, st_3, st_2, in_2, in_3, st_1, m) → T(in_3)ring#(st_1, in_2, st_2, in_3, st_3, m) → empty#(map_f(two, head(in_2)))
U251#(true, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, in_2, st_2, tail(in_3), st_3, m)U212#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_2)
U242#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_1)U241#(false, st_3, st_2, in_2, in_3, st_1, m) → app#(map_f(three, head(in_3)), st_3)
U242#(false, st_3, st_2, in_2, in_3, st_1, m) → tail#(in_3)U251#(true, st_3, st_2, in_2, in_3, st_1, m) → T(st_1)
U231#(true, st_3, st_2, in_2, in_3, st_1, m) → U232#(empty(fstsplit(m, st_3)), st_3, st_2, in_2, in_3, st_1, m)U242#(false, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
U221#(true, st_3, st_2, in_2, in_3, st_1, m) → T(m)U221#(true, st_3, st_2, in_2, in_3, st_1, m) → tail#(in_2)
U212#(false, st_3, st_2, in_2, in_3, st_1, m) → tail#(in_2)U241#(false, st_3, st_2, in_2, in_3, st_1, m) → U242#(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_3, st_2, in_2, in_3, st_1, m)
U202#(false, st_3, st_2, in_2, in_3, st_1, m) → fstsplit#(m, st_2)U202#(false, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
U251#(true, st_3, st_2, in_2, in_3, st_1, m) → T(st_3)ring#(st_1, in_2, st_2, in_3, st_3, m) → head#(in_3)
ring#(st_1, in_2, st_2, in_3, st_3, m) → empty#(map_f(three, head(in_3)))U202#(false, st_3, st_2, in_2, in_3, st_1, m) → sndsplit#(m, st_2)
U221#(true, st_3, st_2, in_2, in_3, st_1, m) → T(st_1)ring#(st_1, in_2, st_2, in_3, st_3, m) → head#(in_2)
U191#(false, st_3, st_2, in_2, in_3, st_1, m) → T(in_2)U191#(false, st_3, st_2, in_2, in_3, st_1, m) → T(m)
U231#(true, st_3, st_2, in_2, in_3, st_1, m) → T(m)U201#(true, st_3, st_2, in_2, in_3, st_1, m) → T(st_2)
U211#(false, st_3, st_2, in_2, in_3, st_1, m) → map_f#(two, head(in_2))U251#(true, st_3, st_2, in_2, in_3, st_1, m) → T(st_2)
U241#(false, st_3, st_2, in_2, in_3, st_1, m) → T(m)U212#(false, st_3, st_2, in_2, in_3, st_1, m) → 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)
U191#(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U211#(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)
U201#(true, st_3, st_2, in_2, in_3, st_1, m) → empty#(fstsplit(m, st_2))U232#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_2)
U191#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_2)U211#(false, st_3, st_2, in_2, in_3, st_1, m) → U212#(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_3, st_2, in_2, in_3, st_1, m)
sndsplit#(s(n), cons(h, t)) → sndsplit#(n, t)U232#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_3)
U241#(false, st_3, st_2, in_2, in_3, st_1, m) → map_f#(three, head(in_3))U212#(false, st_3, st_2, in_2, in_3, st_1, m) → app#(map_f(two, head(in_2)), st_2)
U242#(false, st_3, st_2, in_2, in_3, st_1, m) → map_f#(three, head(in_3))U232#(false, st_3, st_2, in_2, in_3, st_1, m) → sndsplit#(m, st_3)
U242#(false, st_3, st_2, in_2, in_3, st_1, m) → T(in_2)U221#(true, st_3, st_2, in_2, in_3, st_1, m) → T(st_2)
ring#(st_1, in_2, st_2, in_3, st_3, m) → fstsplit#(m, st_1)U191#(false, st_3, st_2, in_2, in_3, st_1, m) → T(in_3)
ring#(st_1, in_2, st_2, in_3, st_3, m) → U241#(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)U211#(false, st_3, st_2, in_2, in_3, st_1, m) → fstsplit#(m, app(map_f(two, head(in_2)), st_2))
U201#(true, st_3, st_2, in_2, in_3, st_1, m) → fstsplit#(m, st_2)ring#(st_1, in_2, st_2, in_3, st_3, m) → U231#(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)
length#(cons(h, t)) → length#(t)U211#(false, st_3, st_2, in_2, in_3, st_1, m) → T(in_2)
U212#(false, st_3, st_2, in_2, in_3, st_1, m) → sndsplit#(m, app(map_f(two, head(in_2)), st_2))U202#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_3)
U242#(false, st_3, st_2, in_2, in_3, st_1, m) → T(in_3)U191#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_3)
U241#(false, st_3, st_2, in_2, in_3, st_1, m) → fstsplit#(m, app(map_f(three, head(in_3)), st_3))U212#(false, st_3, st_2, in_2, in_3, st_1, m) → T(in_2)
U212#(false, st_3, st_2, in_2, in_3, st_1, m) → T(in_3)U191#(false, st_3, st_2, in_2, in_3, st_1, m) → sndsplit#(m, st_1)
U211#(false, st_3, st_2, in_2, in_3, st_1, m) → head#(in_2)U231#(true, st_3, st_2, in_2, in_3, st_1, m) → T(st_3)
U202#(false, st_3, st_2, in_2, in_3, st_1, m) → T(m)U221#(true, st_3, st_2, in_2, in_3, st_1, m) → T(in_2)
U212#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_1)U251#(true, st_3, st_2, in_2, in_3, st_1, m) → tail#(in_3)
U232#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_1)U251#(true, st_3, st_2, in_2, in_3, st_1, m) → T(m)
U202#(false, st_3, st_2, in_2, in_3, st_1, m) → T(st_1)U202#(false, st_3, st_2, in_2, in_3, st_1, m) → T(in_3)
U242#(false, st_3, st_2, in_2, in_3, st_1, m) → head#(in_3)app#(cons(h, t), x) → app#(t, x)
ring#(st_1, in_2, st_2, in_3, st_3, m) → U251#(empty(map_f(three, head(in_3))), st_3, st_2, in_2, in_3, st_1, m)U191#(false, st_3, st_2, in_2, in_3, st_1, m) → fstsplit#(m, st_1)
U211#(false, st_3, st_2, in_2, in_3, st_1, m) → empty#(fstsplit(m, app(map_f(two, head(in_2)), st_2)))

Rewrite Rules

fstsplit(0, x) → nilfstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))sndsplit(0, x) → x
sndsplit(s(n), nil) → nilsndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → trueempty(cons(h, t)) → false
leq(0, m) → trueleq(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)) → tring(st_1, in_2, st_2, in_3, st_3, m) → U191(empty(fstsplit(m, st_1)), st_3, st_2, in_2, in_3, st_1, m)
U191(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U201(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)
U201(true, st_3, st_2, in_2, in_3, st_1, m) → U202(empty(fstsplit(m, st_2)), st_3, st_2, in_2, in_3, st_1, m)U202(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U211(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)U211(false, st_3, st_2, in_2, in_3, st_1, m) → U212(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_3, st_2, in_2, in_3, st_1, m)
U212(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U221(empty(map_f(two, head(in_2))), st_3, st_2, in_2, in_3, st_1, m)
U221(true, st_3, st_2, in_2, in_3, st_1, m) → 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) → U231(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)
U231(true, st_3, st_2, in_2, in_3, st_1, m) → U232(empty(fstsplit(m, st_3)), st_3, st_2, in_2, in_3, st_1, m)U232(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U241(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)U241(false, st_3, st_2, in_2, in_3, st_1, m) → U242(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_3, st_2, in_2, in_3, st_1, m)
U242(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U251(empty(map_f(three, head(in_3))), st_3, st_2, in_2, in_3, st_1, m)
U251(true, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Original Signature

Termination of terms over the following signature is verified: f, ring, app, map_f, leq, true, tail, fstsplit, two, 0, s, sndsplit, length, empty, three, false, head, cons, nil

Strategy

Context-sensitive strategy:
μ(three) = μ(false) = μ(0) = μ(T) = μ(true) = μ(two) = μ(nil) = ∅
μ(tail#) = μ(U211) = μ(U212) = μ(empty) = μ(U251) = μ(head) = μ(U212#) = μ(U202#) = μ(tail) = μ(U191) = μ(U191#) = μ(U221) = μ(U242#) = μ(U232#) = μ(length#) = μ(empty#) = μ(U201#) = μ(U211#) = μ(U241#) = μ(U221#) = μ(U251#) = μ(length) = μ(U232) = μ(U231) = μ(U231#) = μ(U201) = μ(U202) = μ(s) = μ(head#) = μ(U242) = μ(U241) = {1}
μ(map_f) = μ(sndsplit#) = μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(leq) = {1, 2}
μ(ring) = μ(ring#) = {1, 2, 3, 4, 5, 6}

The following SCCs where found

fstsplit#(s(n), cons(h, t)) → fstsplit#(n, t)
length#(cons(h, t)) → length#(t)
U221#(true, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, tail(in_2), st_2, in_3, st_3, m)U231#(true, st_3, st_2, in_2, in_3, st_1, m) → U232#(empty(fstsplit(m, st_3)), st_3, st_2, in_2, in_3, st_1, m)
U242#(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U241#(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)
ring#(st_1, in_2, st_2, in_3, st_3, m) → U201#(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)U212#(false, st_3, st_2, in_2, in_3, st_1, m) → 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)
U191#(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U191#(empty(fstsplit(m, st_1)), st_3, st_2, in_2, in_3, st_1, m)
ring#(st_1, in_2, st_2, in_3, st_3, m) → U231#(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)U232#(false, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
ring#(st_1, in_2, st_2, in_3, st_3, m) → U221#(empty(map_f(two, head(in_2))), st_3, st_2, in_2, in_3, st_1, m)U241#(false, st_3, st_2, in_2, in_3, st_1, m) → U242#(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_3, st_2, in_2, in_3, st_1, m)
U202#(false, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)ring#(st_1, in_2, st_2, in_3, st_3, m) → U211#(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)
U251#(true, st_3, st_2, in_2, in_3, st_1, m) → ring#(st_1, in_2, st_2, tail(in_3), st_3, m)U211#(false, st_3, st_2, in_2, in_3, st_1, m) → U212#(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_3, st_2, in_2, in_3, st_1, m)
ring#(st_1, in_2, st_2, in_3, st_3, m) → U251#(empty(map_f(three, head(in_3))), st_3, st_2, in_2, in_3, st_1, m)U201#(true, st_3, st_2, in_2, in_3, st_1, m) → U202#(empty(fstsplit(m, st_2)), st_3, st_2, in_2, in_3, st_1, m)
app#(cons(h, t), x) → app#(t, x)
leq#(s(n), s(m)) → leq#(n, m)
sndsplit#(s(n), cons(h, t)) → sndsplit#(n, t)
map_f#(pid, cons(h, t)) → map_f#(pid, t)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

fstsplit#(s(n), cons(h, t)) → fstsplit#(n, t)

Rewrite Rules

fstsplit(0, x) → nilfstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))sndsplit(0, x) → x
sndsplit(s(n), nil) → nilsndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → trueempty(cons(h, t)) → false
leq(0, m) → trueleq(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)) → tring(st_1, in_2, st_2, in_3, st_3, m) → U191(empty(fstsplit(m, st_1)), st_3, st_2, in_2, in_3, st_1, m)
U191(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U201(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)
U201(true, st_3, st_2, in_2, in_3, st_1, m) → U202(empty(fstsplit(m, st_2)), st_3, st_2, in_2, in_3, st_1, m)U202(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U211(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)U211(false, st_3, st_2, in_2, in_3, st_1, m) → U212(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_3, st_2, in_2, in_3, st_1, m)
U212(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U221(empty(map_f(two, head(in_2))), st_3, st_2, in_2, in_3, st_1, m)
U221(true, st_3, st_2, in_2, in_3, st_1, m) → 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) → U231(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)
U231(true, st_3, st_2, in_2, in_3, st_1, m) → U232(empty(fstsplit(m, st_3)), st_3, st_2, in_2, in_3, st_1, m)U232(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U241(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)U241(false, st_3, st_2, in_2, in_3, st_1, m) → U242(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_3, st_2, in_2, in_3, st_1, m)
U242(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U251(empty(map_f(three, head(in_3))), st_3, st_2, in_2, in_3, st_1, m)
U251(true, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Original Signature

Termination of terms over the following signature is verified: f, ring, app, map_f, leq, true, tail, fstsplit, two, 0, s, sndsplit, length, empty, three, false, head, cons, nil

Strategy

Context-sensitive strategy:
μ(three) = μ(false) = μ(0) = μ(T) = μ(true) = μ(two) = μ(nil) = ∅
μ(tail#) = μ(U211) = μ(U212) = μ(empty) = μ(U251) = μ(head) = μ(U212#) = μ(U202#) = μ(tail) = μ(U191) = μ(U191#) = μ(U221) = μ(U242#) = μ(U232#) = μ(length#) = μ(empty#) = μ(U201#) = μ(U211#) = μ(U241#) = μ(U221#) = μ(U251#) = μ(length) = μ(U232) = μ(U231) = μ(U231#) = μ(U201) = μ(U202) = μ(s) = μ(head#) = μ(U242) = μ(U241) = {1}
μ(map_f) = μ(sndsplit#) = μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(leq) = {1, 2}
μ(ring) = μ(ring#) = {1, 2, 3, 4, 5, 6}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

fstsplit#(s(n), cons(h, t)) → fstsplit#(n, t)

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

leq#(s(n), s(m)) → leq#(n, m)

Rewrite Rules

fstsplit(0, x) → nilfstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))sndsplit(0, x) → x
sndsplit(s(n), nil) → nilsndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → trueempty(cons(h, t)) → false
leq(0, m) → trueleq(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)) → tring(st_1, in_2, st_2, in_3, st_3, m) → U191(empty(fstsplit(m, st_1)), st_3, st_2, in_2, in_3, st_1, m)
U191(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U201(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)
U201(true, st_3, st_2, in_2, in_3, st_1, m) → U202(empty(fstsplit(m, st_2)), st_3, st_2, in_2, in_3, st_1, m)U202(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U211(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)U211(false, st_3, st_2, in_2, in_3, st_1, m) → U212(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_3, st_2, in_2, in_3, st_1, m)
U212(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U221(empty(map_f(two, head(in_2))), st_3, st_2, in_2, in_3, st_1, m)
U221(true, st_3, st_2, in_2, in_3, st_1, m) → 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) → U231(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)
U231(true, st_3, st_2, in_2, in_3, st_1, m) → U232(empty(fstsplit(m, st_3)), st_3, st_2, in_2, in_3, st_1, m)U232(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U241(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)U241(false, st_3, st_2, in_2, in_3, st_1, m) → U242(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_3, st_2, in_2, in_3, st_1, m)
U242(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U251(empty(map_f(three, head(in_3))), st_3, st_2, in_2, in_3, st_1, m)
U251(true, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Original Signature

Termination of terms over the following signature is verified: f, ring, app, map_f, leq, true, tail, fstsplit, two, 0, s, sndsplit, length, empty, three, false, head, cons, nil

Strategy

Context-sensitive strategy:
μ(three) = μ(false) = μ(0) = μ(T) = μ(true) = μ(two) = μ(nil) = ∅
μ(tail#) = μ(U211) = μ(U212) = μ(empty) = μ(U251) = μ(head) = μ(U212#) = μ(U202#) = μ(tail) = μ(U191) = μ(U191#) = μ(U221) = μ(U242#) = μ(U232#) = μ(length#) = μ(empty#) = μ(U201#) = μ(U211#) = μ(U241#) = μ(U221#) = μ(U251#) = μ(length) = μ(U232) = μ(U231) = μ(U231#) = μ(U201) = μ(U202) = μ(s) = μ(head#) = μ(U242) = μ(U241) = {1}
μ(map_f) = μ(sndsplit#) = μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(leq) = {1, 2}
μ(ring) = μ(ring#) = {1, 2, 3, 4, 5, 6}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

leq#(s(n), s(m)) → leq#(n, m)

Problem 5: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

sndsplit#(s(n), cons(h, t)) → sndsplit#(n, t)

Rewrite Rules

fstsplit(0, x) → nilfstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))sndsplit(0, x) → x
sndsplit(s(n), nil) → nilsndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → trueempty(cons(h, t)) → false
leq(0, m) → trueleq(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)) → tring(st_1, in_2, st_2, in_3, st_3, m) → U191(empty(fstsplit(m, st_1)), st_3, st_2, in_2, in_3, st_1, m)
U191(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U201(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)
U201(true, st_3, st_2, in_2, in_3, st_1, m) → U202(empty(fstsplit(m, st_2)), st_3, st_2, in_2, in_3, st_1, m)U202(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U211(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)U211(false, st_3, st_2, in_2, in_3, st_1, m) → U212(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_3, st_2, in_2, in_3, st_1, m)
U212(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U221(empty(map_f(two, head(in_2))), st_3, st_2, in_2, in_3, st_1, m)
U221(true, st_3, st_2, in_2, in_3, st_1, m) → 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) → U231(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)
U231(true, st_3, st_2, in_2, in_3, st_1, m) → U232(empty(fstsplit(m, st_3)), st_3, st_2, in_2, in_3, st_1, m)U232(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U241(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)U241(false, st_3, st_2, in_2, in_3, st_1, m) → U242(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_3, st_2, in_2, in_3, st_1, m)
U242(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U251(empty(map_f(three, head(in_3))), st_3, st_2, in_2, in_3, st_1, m)
U251(true, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Original Signature

Termination of terms over the following signature is verified: f, ring, app, map_f, leq, true, tail, fstsplit, two, 0, s, sndsplit, length, empty, three, false, head, cons, nil

Strategy

Context-sensitive strategy:
μ(three) = μ(false) = μ(0) = μ(T) = μ(true) = μ(two) = μ(nil) = ∅
μ(tail#) = μ(U211) = μ(U212) = μ(empty) = μ(U251) = μ(head) = μ(U212#) = μ(U202#) = μ(tail) = μ(U191) = μ(U191#) = μ(U221) = μ(U242#) = μ(U232#) = μ(length#) = μ(empty#) = μ(U201#) = μ(U211#) = μ(U241#) = μ(U221#) = μ(U251#) = μ(length) = μ(U232) = μ(U231) = μ(U231#) = μ(U201) = μ(U202) = μ(s) = μ(head#) = μ(U242) = μ(U241) = {1}
μ(map_f) = μ(sndsplit#) = μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(leq) = {1, 2}
μ(ring) = μ(ring#) = {1, 2, 3, 4, 5, 6}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

sndsplit#(s(n), cons(h, t)) → sndsplit#(n, t)

Problem 6: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

app#(cons(h, t), x) → app#(t, x)

Rewrite Rules

fstsplit(0, x) → nilfstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))sndsplit(0, x) → x
sndsplit(s(n), nil) → nilsndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → trueempty(cons(h, t)) → false
leq(0, m) → trueleq(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)) → tring(st_1, in_2, st_2, in_3, st_3, m) → U191(empty(fstsplit(m, st_1)), st_3, st_2, in_2, in_3, st_1, m)
U191(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U201(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)
U201(true, st_3, st_2, in_2, in_3, st_1, m) → U202(empty(fstsplit(m, st_2)), st_3, st_2, in_2, in_3, st_1, m)U202(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U211(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)U211(false, st_3, st_2, in_2, in_3, st_1, m) → U212(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_3, st_2, in_2, in_3, st_1, m)
U212(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U221(empty(map_f(two, head(in_2))), st_3, st_2, in_2, in_3, st_1, m)
U221(true, st_3, st_2, in_2, in_3, st_1, m) → 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) → U231(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)
U231(true, st_3, st_2, in_2, in_3, st_1, m) → U232(empty(fstsplit(m, st_3)), st_3, st_2, in_2, in_3, st_1, m)U232(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U241(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)U241(false, st_3, st_2, in_2, in_3, st_1, m) → U242(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_3, st_2, in_2, in_3, st_1, m)
U242(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U251(empty(map_f(three, head(in_3))), st_3, st_2, in_2, in_3, st_1, m)
U251(true, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Original Signature

Termination of terms over the following signature is verified: f, ring, app, map_f, leq, true, tail, fstsplit, two, 0, s, sndsplit, length, empty, three, false, head, cons, nil

Strategy

Context-sensitive strategy:
μ(three) = μ(false) = μ(0) = μ(T) = μ(true) = μ(two) = μ(nil) = ∅
μ(tail#) = μ(U211) = μ(U212) = μ(empty) = μ(U251) = μ(head) = μ(U212#) = μ(U202#) = μ(tail) = μ(U191) = μ(U191#) = μ(U221) = μ(U242#) = μ(U232#) = μ(length#) = μ(empty#) = μ(U201#) = μ(U211#) = μ(U241#) = μ(U221#) = μ(U251#) = μ(length) = μ(U232) = μ(U231) = μ(U231#) = μ(U201) = μ(U202) = μ(s) = μ(head#) = μ(U242) = μ(U241) = {1}
μ(map_f) = μ(sndsplit#) = μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(leq) = {1, 2}
μ(ring) = μ(ring#) = {1, 2, 3, 4, 5, 6}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

app#(cons(h, t), x) → app#(t, x)

Problem 7: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

map_f#(pid, cons(h, t)) → map_f#(pid, t)

Rewrite Rules

fstsplit(0, x) → nilfstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))sndsplit(0, x) → x
sndsplit(s(n), nil) → nilsndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → trueempty(cons(h, t)) → false
leq(0, m) → trueleq(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)) → tring(st_1, in_2, st_2, in_3, st_3, m) → U191(empty(fstsplit(m, st_1)), st_3, st_2, in_2, in_3, st_1, m)
U191(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U201(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)
U201(true, st_3, st_2, in_2, in_3, st_1, m) → U202(empty(fstsplit(m, st_2)), st_3, st_2, in_2, in_3, st_1, m)U202(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U211(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)U211(false, st_3, st_2, in_2, in_3, st_1, m) → U212(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_3, st_2, in_2, in_3, st_1, m)
U212(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U221(empty(map_f(two, head(in_2))), st_3, st_2, in_2, in_3, st_1, m)
U221(true, st_3, st_2, in_2, in_3, st_1, m) → 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) → U231(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)
U231(true, st_3, st_2, in_2, in_3, st_1, m) → U232(empty(fstsplit(m, st_3)), st_3, st_2, in_2, in_3, st_1, m)U232(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U241(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)U241(false, st_3, st_2, in_2, in_3, st_1, m) → U242(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_3, st_2, in_2, in_3, st_1, m)
U242(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U251(empty(map_f(three, head(in_3))), st_3, st_2, in_2, in_3, st_1, m)
U251(true, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Original Signature

Termination of terms over the following signature is verified: f, ring, app, map_f, leq, true, tail, fstsplit, two, 0, s, sndsplit, length, empty, three, false, head, cons, nil

Strategy

Context-sensitive strategy:
μ(three) = μ(false) = μ(0) = μ(T) = μ(true) = μ(two) = μ(nil) = ∅
μ(tail#) = μ(U211) = μ(U212) = μ(empty) = μ(U251) = μ(head) = μ(U212#) = μ(U202#) = μ(tail) = μ(U191) = μ(U191#) = μ(U221) = μ(U242#) = μ(U232#) = μ(length#) = μ(empty#) = μ(U201#) = μ(U211#) = μ(U241#) = μ(U221#) = μ(U251#) = μ(length) = μ(U232) = μ(U231) = μ(U231#) = μ(U201) = μ(U202) = μ(s) = μ(head#) = μ(U242) = μ(U241) = {1}
μ(map_f) = μ(sndsplit#) = μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(leq) = {1, 2}
μ(ring) = μ(ring#) = {1, 2, 3, 4, 5, 6}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

map_f#(pid, cons(h, t)) → map_f#(pid, t)

Problem 8: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

length#(cons(h, t)) → length#(t)

Rewrite Rules

fstsplit(0, x) → nilfstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))sndsplit(0, x) → x
sndsplit(s(n), nil) → nilsndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → trueempty(cons(h, t)) → false
leq(0, m) → trueleq(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)) → tring(st_1, in_2, st_2, in_3, st_3, m) → U191(empty(fstsplit(m, st_1)), st_3, st_2, in_2, in_3, st_1, m)
U191(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U201(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)
U201(true, st_3, st_2, in_2, in_3, st_1, m) → U202(empty(fstsplit(m, st_2)), st_3, st_2, in_2, in_3, st_1, m)U202(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U211(leq(m, length(st_2)), st_3, st_2, in_2, in_3, st_1, m)U211(false, st_3, st_2, in_2, in_3, st_1, m) → U212(empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))), st_3, st_2, in_2, in_3, st_1, m)
U212(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U221(empty(map_f(two, head(in_2))), st_3, st_2, in_2, in_3, st_1, m)
U221(true, st_3, st_2, in_2, in_3, st_1, m) → 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) → U231(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)
U231(true, st_3, st_2, in_2, in_3, st_1, m) → U232(empty(fstsplit(m, st_3)), st_3, st_2, in_2, in_3, st_1, m)U232(false, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → U241(leq(m, length(st_3)), st_3, st_2, in_2, in_3, st_1, m)U241(false, st_3, st_2, in_2, in_3, st_1, m) → U242(empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))), st_3, st_2, in_2, in_3, st_1, m)
U242(false, st_3, st_2, in_2, in_3, st_1, m) → 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) → U251(empty(map_f(three, head(in_3))), st_3, st_2, in_2, in_3, st_1, m)
U251(true, st_3, st_2, in_2, in_3, st_1, m) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Original Signature

Termination of terms over the following signature is verified: f, ring, app, map_f, leq, true, tail, fstsplit, two, 0, s, sndsplit, length, empty, three, false, head, cons, nil

Strategy

Context-sensitive strategy:
μ(three) = μ(false) = μ(0) = μ(T) = μ(true) = μ(two) = μ(nil) = ∅
μ(tail#) = μ(U211) = μ(U212) = μ(empty) = μ(U251) = μ(head) = μ(U212#) = μ(U202#) = μ(tail) = μ(U191) = μ(U191#) = μ(U221) = μ(U242#) = μ(U232#) = μ(length#) = μ(empty#) = μ(U201#) = μ(U211#) = μ(U241#) = μ(U221#) = μ(U251#) = μ(length) = μ(U232) = μ(U231) = μ(U231#) = μ(U201) = μ(U202) = μ(s) = μ(head#) = μ(U242) = μ(U241) = {1}
μ(map_f) = μ(sndsplit#) = μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(leq) = {1, 2}
μ(ring) = μ(ring#) = {1, 2, 3, 4, 5, 6}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

length#(cons(h, t)) → length#(t)