TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (3985ms).
 | – Problem 2 was processed with processor SubtermCriterion (4ms).
 | – Problem 3 was processed with processor SubtermCriterion (2ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).
 | – Problem 5 was processed with processor SubtermCriterion (1ms).
 | – Problem 6 was processed with processor SubtermCriterion (4ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 8 remains open; application of the following processors failed [SubtermCriterion (3ms), DependencyGraph (166ms), PolynomialLinearRange4iUR (10000ms), DependencyGraph (timeout), PolynomialLinearRange8NegiUR (30001ms), DependencyGraph (timeout), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 8

Dependency Pairs

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_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) → if_9#(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))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))))
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_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)
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, 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_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)
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_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)
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))))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)

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) → 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)

Original Signature

Termination of terms over the following signature is verified: fstsplit, sndsplit, three, length, empty, false, head, cons, f, if_4, app, ring, if_5, if_2, map_f, if_3, if_8, if_9, leq, if_6, if_7, true, tail, two, 0, s, if_1, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

ring#(st_1, in_2, st_2, in_3, st_3, m) → map_f#(two, head(in_2))if_8#(st_1, in_2, st_2, in_3, st_3, m, false) → map_f#(three, head(in_3))
ring#(st_1, in_2, st_2, in_3, st_3, m) → empty#(fstsplit(m, st_1))if_8#(st_1, in_2, st_2, in_3, st_3, m, false) → tail#(in_3)
leq#(s(n), s(m)) → leq#(n, m)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_8#(st_1, in_2, st_2, in_3, st_3, m, false) → app#(map_f(three, head(in_3)), st_3)if_9#(st_1, in_2, st_2, in_3, st_3, m, true) → tail#(in_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_3#(st_1, in_2, st_2, in_3, st_3, m, false) → fstsplit#(m, 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))
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_4#(st_1, in_2, st_2, in_3, st_3, m, false) → map_f#(two, head(in_2))
ring#(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) → head#(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))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) → head#(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)))
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))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, true) → empty#(fstsplit(m, st_3))if_8#(st_1, in_2, st_2, in_3, st_3, m, false) → 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)))map_f#(pid, cons(h, t)) → app#(f(pid, h), map_f(pid, t))
if_6#(st_1, in_2, st_2, in_3, st_3, m, false) → 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_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_4#(st_1, in_2, st_2, in_3, st_3, m, false) → tail#(in_2)
if_2#(st_1, in_2, st_2, in_3, st_3, m, true) → fstsplit#(m, st_2)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) → map_f#(two, head(in_2))if_6#(st_1, in_2, st_2, in_3, st_3, m, false) → head#(in_3)
if_1#(st_1, in_2, st_2, in_3, st_3, m, false) → fstsplit#(m, st_1)if_2#(st_1, in_2, st_2, in_3, st_3, m, false) → app#(map_f(two, head(in_2)), st_2)
sndsplit#(s(n), cons(h, t)) → sndsplit#(n, t)map_f#(pid, cons(h, t)) → map_f#(pid, t)
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) → sndsplit#(m, 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)if_2#(st_1, in_2, st_2, in_3, st_3, m, true) → empty#(fstsplit(m, st_2))
ring#(st_1, in_2, st_2, in_3, st_3, m) → fstsplit#(m, st_1)if_6#(st_1, in_2, st_2, in_3, st_3, m, false) → map_f#(three, head(in_3))
if_2#(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, false) → fstsplit#(m, app(map_f(two, head(in_2)), st_2))
if_7#(st_1, in_2, st_2, in_3, st_3, m, false) → sndsplit#(m, st_3)if_6#(st_1, in_2, st_2, in_3, st_3, m, true) → fstsplit#(m, st_3)
if_1#(st_1, in_2, st_2, in_3, st_3, m, false) → sndsplit#(m, st_1)length#(cons(h, t)) → length#(t)
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) → head#(in_2)
if_5#(st_1, in_2, st_2, in_3, st_3, m, true) → tail#(in_2)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)))
ring#(st_1, in_2, st_2, in_3, st_3, m) → length#(st_2)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))))
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_4#(st_1, in_2, st_2, in_3, st_3, m, false) → app#(map_f(two, head(in_2)), st_2)
fstsplit#(s(n), cons(h, t)) → fstsplit#(n, t)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_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_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_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))ring#(st_1, in_2, st_2, in_3, st_3, m) → length#(st_3)
app#(cons(h, t), x) → app#(t, x)ring#(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)

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) → 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)

Original Signature

Termination of terms over the following signature is verified: fstsplit, sndsplit, empty, length, three, false, head, cons, if_4, f, if_5, ring, app, if_2, map_f, if_3, if_8, if_9, leq, if_6, if_7, true, tail, two, 0, s, if_1, nil

Strategy

The following SCCs where found

fstsplit#(s(n), cons(h, t)) → fstsplit#(n, t)
length#(cons(h, t)) → length#(t)
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)
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_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_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))))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_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(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)
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)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_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_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)
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_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_5#(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_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)
map_f#(pid, cons(h, t)) → map_f#(pid, t)

Problem 2: SubtermCriterion

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) → 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)

Original Signature

Termination of terms over the following signature is verified: fstsplit, sndsplit, empty, length, three, false, head, cons, if_4, f, if_5, ring, app, if_2, map_f, if_3, if_8, if_9, leq, if_6, if_7, true, tail, two, 0, s, if_1, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 3: SubtermCriterion

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) → 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)

Original Signature

Termination of terms over the following signature is verified: fstsplit, sndsplit, empty, length, three, false, head, cons, if_4, f, if_5, ring, app, if_2, map_f, if_3, if_8, if_9, leq, if_6, if_7, true, tail, two, 0, s, if_1, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion

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) → 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)

Original Signature

Termination of terms over the following signature is verified: fstsplit, sndsplit, empty, length, three, false, head, cons, if_4, f, if_5, ring, app, if_2, map_f, if_3, if_8, if_9, leq, if_6, if_7, true, tail, two, 0, s, if_1, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 5: SubtermCriterion

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) → 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)

Original Signature

Termination of terms over the following signature is verified: fstsplit, sndsplit, empty, length, three, false, head, cons, if_4, f, if_5, ring, app, if_2, map_f, if_3, if_8, if_9, leq, if_6, if_7, true, tail, two, 0, s, if_1, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 6: SubtermCriterion

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) → 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)

Original Signature

Termination of terms over the following signature is verified: fstsplit, sndsplit, empty, length, three, false, head, cons, if_4, f, if_5, ring, app, if_2, map_f, if_3, if_8, if_9, leq, if_6, if_7, true, tail, two, 0, s, if_1, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 7: SubtermCriterion

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) → 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)

Original Signature

Termination of terms over the following signature is verified: fstsplit, sndsplit, empty, length, three, false, head, cons, if_4, f, if_5, ring, app, if_2, map_f, if_3, if_8, if_9, leq, if_6, if_7, true, tail, two, 0, s, if_1, nil

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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