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