MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { 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))) , 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) -> 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))) , 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_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_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_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_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()) -> 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_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_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_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_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()) -> ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three(), head(in_3)), st_3)), m) , 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) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { fstsplit^#(0(), x) -> c_1() , fstsplit^#(s(n), nil()) -> c_2() , fstsplit^#(s(n), cons(h, t)) -> c_3(h, fstsplit^#(n, t)) , sndsplit^#(0(), x) -> c_4(x) , sndsplit^#(s(n), nil()) -> c_5() , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t)) , empty^#(nil()) -> c_7() , empty^#(cons(h, t)) -> c_8() , leq^#(0(), m) -> c_9() , leq^#(s(n), 0()) -> c_10() , leq^#(s(n), s(m)) -> c_11(leq^#(n, m)) , length^#(nil()) -> c_12() , length^#(cons(h, t)) -> c_13(length^#(t)) , app^#(nil(), x) -> c_14(x) , app^#(cons(h, t), x) -> c_15(h, app^#(t, x)) , map_f^#(pid, nil()) -> c_16() , map_f^#(pid, cons(h, t)) -> c_17(app^#(f(pid, h), map_f(pid, t))) , head^#(cons(h, t)) -> c_18(h) , tail^#(cons(h, t)) -> c_19(t) , ring^#(st_1, in_2, st_2, in_3, st_3, m) -> c_20(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) -> c_21(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) -> c_22(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) -> c_23(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) -> c_24(if_9^#(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three(), head(in_3))))) , if_1^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_25(ring^#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)) , if_2^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_26(if_3^#(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))) , if_2^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_27(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_5^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_30(ring^#(st_1, tail(in_2), st_2, in_3, st_3, m)) , if_6^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_31(if_7^#(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))) , if_6^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_32(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_9^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_35(ring^#(st_1, in_2, st_2, tail(in_3), st_3, m)) , if_3^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_28(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()) -> c_29(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()) -> c_33(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()) -> c_34(ring^#(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three(), head(in_3)), st_3)), m)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fstsplit^#(0(), x) -> c_1() , fstsplit^#(s(n), nil()) -> c_2() , fstsplit^#(s(n), cons(h, t)) -> c_3(h, fstsplit^#(n, t)) , sndsplit^#(0(), x) -> c_4(x) , sndsplit^#(s(n), nil()) -> c_5() , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t)) , empty^#(nil()) -> c_7() , empty^#(cons(h, t)) -> c_8() , leq^#(0(), m) -> c_9() , leq^#(s(n), 0()) -> c_10() , leq^#(s(n), s(m)) -> c_11(leq^#(n, m)) , length^#(nil()) -> c_12() , length^#(cons(h, t)) -> c_13(length^#(t)) , app^#(nil(), x) -> c_14(x) , app^#(cons(h, t), x) -> c_15(h, app^#(t, x)) , map_f^#(pid, nil()) -> c_16() , map_f^#(pid, cons(h, t)) -> c_17(app^#(f(pid, h), map_f(pid, t))) , head^#(cons(h, t)) -> c_18(h) , tail^#(cons(h, t)) -> c_19(t) , ring^#(st_1, in_2, st_2, in_3, st_3, m) -> c_20(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) -> c_21(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) -> c_22(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) -> c_23(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) -> c_24(if_9^#(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three(), head(in_3))))) , if_1^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_25(ring^#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)) , if_2^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_26(if_3^#(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))) , if_2^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_27(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_5^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_30(ring^#(st_1, tail(in_2), st_2, in_3, st_3, m)) , if_6^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_31(if_7^#(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))) , if_6^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_32(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_9^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_35(ring^#(st_1, in_2, st_2, tail(in_3), st_3, m)) , if_3^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_28(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()) -> c_29(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()) -> c_33(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()) -> c_34(ring^#(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three(), head(in_3)), st_3)), m)) } Strict Trs: { 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))) , 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) -> 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))) , 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_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_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_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_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()) -> 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_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_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_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_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()) -> ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three(), head(in_3)), st_3)), m) , 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) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,5,7,8,9,10,12,16,17} by applications of Pre({1,2,5,7,8,9,10,12,16,17}) = {3,4,6,11,13,14,15,18,19}. Here rules are labeled as follows: DPs: { 1: fstsplit^#(0(), x) -> c_1() , 2: fstsplit^#(s(n), nil()) -> c_2() , 3: fstsplit^#(s(n), cons(h, t)) -> c_3(h, fstsplit^#(n, t)) , 4: sndsplit^#(0(), x) -> c_4(x) , 5: sndsplit^#(s(n), nil()) -> c_5() , 6: sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t)) , 7: empty^#(nil()) -> c_7() , 8: empty^#(cons(h, t)) -> c_8() , 9: leq^#(0(), m) -> c_9() , 10: leq^#(s(n), 0()) -> c_10() , 11: leq^#(s(n), s(m)) -> c_11(leq^#(n, m)) , 12: length^#(nil()) -> c_12() , 13: length^#(cons(h, t)) -> c_13(length^#(t)) , 14: app^#(nil(), x) -> c_14(x) , 15: app^#(cons(h, t), x) -> c_15(h, app^#(t, x)) , 16: map_f^#(pid, nil()) -> c_16() , 17: map_f^#(pid, cons(h, t)) -> c_17(app^#(f(pid, h), map_f(pid, t))) , 18: head^#(cons(h, t)) -> c_18(h) , 19: tail^#(cons(h, t)) -> c_19(t) , 20: ring^#(st_1, in_2, st_2, in_3, st_3, m) -> c_20(if_1^#(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))) , 21: ring^#(st_1, in_2, st_2, in_3, st_3, m) -> c_21(if_2^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))) , 22: ring^#(st_1, in_2, st_2, in_3, st_3, m) -> c_22(if_5^#(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two(), head(in_2))))) , 23: ring^#(st_1, in_2, st_2, in_3, st_3, m) -> c_23(if_6^#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))) , 24: ring^#(st_1, in_2, st_2, in_3, st_3, m) -> c_24(if_9^#(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three(), head(in_3))))) , 25: if_1^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_25(ring^#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)) , 26: if_2^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_26(if_3^#(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))) , 27: if_2^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_27(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))))) , 28: if_5^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_30(ring^#(st_1, tail(in_2), st_2, in_3, st_3, m)) , 29: if_6^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_31(if_7^#(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))) , 30: if_6^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_32(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))))) , 31: if_9^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_35(ring^#(st_1, in_2, st_2, tail(in_3), st_3, m)) , 32: if_3^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_28(ring^#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)) , 33: if_4^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_29(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)) , 34: if_7^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_33(ring^#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)) , 35: if_8^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_34(ring^#(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three(), head(in_3)), st_3)), m)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fstsplit^#(s(n), cons(h, t)) -> c_3(h, fstsplit^#(n, t)) , sndsplit^#(0(), x) -> c_4(x) , sndsplit^#(s(n), cons(h, t)) -> c_6(sndsplit^#(n, t)) , leq^#(s(n), s(m)) -> c_11(leq^#(n, m)) , length^#(cons(h, t)) -> c_13(length^#(t)) , app^#(nil(), x) -> c_14(x) , app^#(cons(h, t), x) -> c_15(h, app^#(t, x)) , head^#(cons(h, t)) -> c_18(h) , tail^#(cons(h, t)) -> c_19(t) , ring^#(st_1, in_2, st_2, in_3, st_3, m) -> c_20(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) -> c_21(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) -> c_22(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) -> c_23(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) -> c_24(if_9^#(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three(), head(in_3))))) , if_1^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_25(ring^#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)) , if_2^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_26(if_3^#(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))) , if_2^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_27(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_5^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_30(ring^#(st_1, tail(in_2), st_2, in_3, st_3, m)) , if_6^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_31(if_7^#(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))) , if_6^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_32(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_9^#(st_1, in_2, st_2, in_3, st_3, m, true()) -> c_35(ring^#(st_1, in_2, st_2, tail(in_3), st_3, m)) , if_3^#(st_1, in_2, st_2, in_3, st_3, m, false()) -> c_28(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()) -> c_29(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()) -> c_33(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()) -> c_34(ring^#(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three(), head(in_3)), st_3)), m)) } Strict Trs: { 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))) , 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) -> 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))) , 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_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_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_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_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()) -> 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_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_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_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_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()) -> ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three(), head(in_3)), st_3)), m) , 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) } Weak DPs: { fstsplit^#(0(), x) -> c_1() , fstsplit^#(s(n), nil()) -> c_2() , sndsplit^#(s(n), nil()) -> c_5() , empty^#(nil()) -> c_7() , empty^#(cons(h, t)) -> c_8() , leq^#(0(), m) -> c_9() , leq^#(s(n), 0()) -> c_10() , length^#(nil()) -> c_12() , map_f^#(pid, nil()) -> c_16() , map_f^#(pid, cons(h, t)) -> c_17(app^#(f(pid, h), map_f(pid, t))) } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..