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))
  , process(store, m) -> if1(store, m, leq(m, length(store)))
  , if1(store, m, true()) -> if2(store, m, empty(fstsplit(m, store)))
  , if1(store, m, false()) ->
    if3(store, m, empty(fstsplit(m, app(map_f(self(), nil()), store))))
  , if2(store, m, false()) ->
    process(app(map_f(self(), nil()), sndsplit(m, store)), m)
  , if3(store, m, false()) ->
    process(sndsplit(m, app(map_f(self(), nil()), store)), m) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { fstsplit^#(0(), x) -> c_1()
  , fstsplit^#(s(n), nil()) -> c_2()
  , fstsplit^#(s(n), cons(h, t)) -> c_3(fstsplit^#(n, t))
  , sndsplit^#(0(), x) -> c_4()
  , 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()
  , app^#(cons(h, t), x) -> c_15(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)), map_f^#(pid, t))
  , process^#(store, m) ->
    c_18(if1^#(store, m, leq(m, length(store))),
         leq^#(m, length(store)),
         length^#(store))
  , if1^#(store, m, true()) ->
    c_19(if2^#(store, m, empty(fstsplit(m, store))),
         empty^#(fstsplit(m, store)),
         fstsplit^#(m, store))
  , if1^#(store, m, false()) ->
    c_20(if3^#(store,
               m,
               empty(fstsplit(m, app(map_f(self(), nil()), store)))),
         empty^#(fstsplit(m, app(map_f(self(), nil()), store))),
         fstsplit^#(m, app(map_f(self(), nil()), store)),
         app^#(map_f(self(), nil()), store),
         map_f^#(self(), nil()))
  , if2^#(store, m, false()) ->
    c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m),
         app^#(map_f(self(), nil()), sndsplit(m, store)),
         map_f^#(self(), nil()),
         sndsplit^#(m, store))
  , if3^#(store, m, false()) ->
    c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m),
         sndsplit^#(m, app(map_f(self(), nil()), store)),
         app^#(map_f(self(), nil()), store),
         map_f^#(self(), nil())) }

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(fstsplit^#(n, t))
  , sndsplit^#(0(), x) -> c_4()
  , 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()
  , app^#(cons(h, t), x) -> c_15(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)), map_f^#(pid, t))
  , process^#(store, m) ->
    c_18(if1^#(store, m, leq(m, length(store))),
         leq^#(m, length(store)),
         length^#(store))
  , if1^#(store, m, true()) ->
    c_19(if2^#(store, m, empty(fstsplit(m, store))),
         empty^#(fstsplit(m, store)),
         fstsplit^#(m, store))
  , if1^#(store, m, false()) ->
    c_20(if3^#(store,
               m,
               empty(fstsplit(m, app(map_f(self(), nil()), store)))),
         empty^#(fstsplit(m, app(map_f(self(), nil()), store))),
         fstsplit^#(m, app(map_f(self(), nil()), store)),
         app^#(map_f(self(), nil()), store),
         map_f^#(self(), nil()))
  , if2^#(store, m, false()) ->
    c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m),
         app^#(map_f(self(), nil()), sndsplit(m, store)),
         map_f^#(self(), nil()),
         sndsplit^#(m, store))
  , if3^#(store, m, false()) ->
    c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m),
         sndsplit^#(m, app(map_f(self(), nil()), store)),
         app^#(map_f(self(), nil()), store),
         map_f^#(self(), nil())) }
Weak 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))
  , process(store, m) -> if1(store, m, leq(m, length(store)))
  , if1(store, m, true()) -> if2(store, m, empty(fstsplit(m, store)))
  , if1(store, m, false()) ->
    if3(store, m, empty(fstsplit(m, app(map_f(self(), nil()), store))))
  , if2(store, m, false()) ->
    process(app(map_f(self(), nil()), sndsplit(m, store)), m)
  , if3(store, m, false()) ->
    process(sndsplit(m, app(map_f(self(), nil()), store)), m) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of
{1,2,4,5,7,8,9,10,12,14,16} by applications of
Pre({1,2,4,5,7,8,9,10,12,14,16}) =
{3,6,11,13,15,17,18,19,20,21,22}. 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(fstsplit^#(n, t))
    , 4: sndsplit^#(0(), x) -> c_4()
    , 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()
    , 15: app^#(cons(h, t), x) -> c_15(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)), map_f^#(pid, t))
    , 18: process^#(store, m) ->
          c_18(if1^#(store, m, leq(m, length(store))),
               leq^#(m, length(store)),
               length^#(store))
    , 19: if1^#(store, m, true()) ->
          c_19(if2^#(store, m, empty(fstsplit(m, store))),
               empty^#(fstsplit(m, store)),
               fstsplit^#(m, store))
    , 20: if1^#(store, m, false()) ->
          c_20(if3^#(store,
                     m,
                     empty(fstsplit(m, app(map_f(self(), nil()), store)))),
               empty^#(fstsplit(m, app(map_f(self(), nil()), store))),
               fstsplit^#(m, app(map_f(self(), nil()), store)),
               app^#(map_f(self(), nil()), store),
               map_f^#(self(), nil()))
    , 21: if2^#(store, m, false()) ->
          c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m),
               app^#(map_f(self(), nil()), sndsplit(m, store)),
               map_f^#(self(), nil()),
               sndsplit^#(m, store))
    , 22: if3^#(store, m, false()) ->
          c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m),
               sndsplit^#(m, app(map_f(self(), nil()), store)),
               app^#(map_f(self(), nil()), store),
               map_f^#(self(), nil())) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { fstsplit^#(s(n), cons(h, t)) -> c_3(fstsplit^#(n, t))
  , 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^#(cons(h, t), x) -> c_15(app^#(t, x))
  , map_f^#(pid, cons(h, t)) ->
    c_17(app^#(f(pid, h), map_f(pid, t)), map_f^#(pid, t))
  , process^#(store, m) ->
    c_18(if1^#(store, m, leq(m, length(store))),
         leq^#(m, length(store)),
         length^#(store))
  , if1^#(store, m, true()) ->
    c_19(if2^#(store, m, empty(fstsplit(m, store))),
         empty^#(fstsplit(m, store)),
         fstsplit^#(m, store))
  , if1^#(store, m, false()) ->
    c_20(if3^#(store,
               m,
               empty(fstsplit(m, app(map_f(self(), nil()), store)))),
         empty^#(fstsplit(m, app(map_f(self(), nil()), store))),
         fstsplit^#(m, app(map_f(self(), nil()), store)),
         app^#(map_f(self(), nil()), store),
         map_f^#(self(), nil()))
  , if2^#(store, m, false()) ->
    c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m),
         app^#(map_f(self(), nil()), sndsplit(m, store)),
         map_f^#(self(), nil()),
         sndsplit^#(m, store))
  , if3^#(store, m, false()) ->
    c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m),
         sndsplit^#(m, app(map_f(self(), nil()), store)),
         app^#(map_f(self(), nil()), store),
         map_f^#(self(), nil())) }
Weak DPs:
  { fstsplit^#(0(), x) -> c_1()
  , fstsplit^#(s(n), nil()) -> c_2()
  , sndsplit^#(0(), x) -> c_4()
  , 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()
  , app^#(nil(), x) -> c_14()
  , map_f^#(pid, nil()) -> c_16() }
Weak 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))
  , process(store, m) -> if1(store, m, leq(m, length(store)))
  , if1(store, m, true()) -> if2(store, m, empty(fstsplit(m, store)))
  , if1(store, m, false()) ->
    if3(store, m, empty(fstsplit(m, app(map_f(self(), nil()), store))))
  , if2(store, m, false()) ->
    process(app(map_f(self(), nil()), sndsplit(m, store)), m)
  , if3(store, m, false()) ->
    process(sndsplit(m, app(map_f(self(), nil()), store)), m) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ fstsplit^#(0(), x) -> c_1()
, fstsplit^#(s(n), nil()) -> c_2()
, sndsplit^#(0(), x) -> c_4()
, 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()
, app^#(nil(), x) -> c_14()
, map_f^#(pid, nil()) -> c_16() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { fstsplit^#(s(n), cons(h, t)) -> c_3(fstsplit^#(n, t))
  , 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^#(cons(h, t), x) -> c_15(app^#(t, x))
  , map_f^#(pid, cons(h, t)) ->
    c_17(app^#(f(pid, h), map_f(pid, t)), map_f^#(pid, t))
  , process^#(store, m) ->
    c_18(if1^#(store, m, leq(m, length(store))),
         leq^#(m, length(store)),
         length^#(store))
  , if1^#(store, m, true()) ->
    c_19(if2^#(store, m, empty(fstsplit(m, store))),
         empty^#(fstsplit(m, store)),
         fstsplit^#(m, store))
  , if1^#(store, m, false()) ->
    c_20(if3^#(store,
               m,
               empty(fstsplit(m, app(map_f(self(), nil()), store)))),
         empty^#(fstsplit(m, app(map_f(self(), nil()), store))),
         fstsplit^#(m, app(map_f(self(), nil()), store)),
         app^#(map_f(self(), nil()), store),
         map_f^#(self(), nil()))
  , if2^#(store, m, false()) ->
    c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m),
         app^#(map_f(self(), nil()), sndsplit(m, store)),
         map_f^#(self(), nil()),
         sndsplit^#(m, store))
  , if3^#(store, m, false()) ->
    c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m),
         sndsplit^#(m, app(map_f(self(), nil()), store)),
         app^#(map_f(self(), nil()), store),
         map_f^#(self(), nil())) }
Weak 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))
  , process(store, m) -> if1(store, m, leq(m, length(store)))
  , if1(store, m, true()) -> if2(store, m, empty(fstsplit(m, store)))
  , if1(store, m, false()) ->
    if3(store, m, empty(fstsplit(m, app(map_f(self(), nil()), store))))
  , if2(store, m, false()) ->
    process(app(map_f(self(), nil()), sndsplit(m, store)), m)
  , if3(store, m, false()) ->
    process(sndsplit(m, app(map_f(self(), nil()), store)), m) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { map_f^#(pid, cons(h, t)) ->
    c_17(app^#(f(pid, h), map_f(pid, t)), map_f^#(pid, t))
  , if1^#(store, m, true()) ->
    c_19(if2^#(store, m, empty(fstsplit(m, store))),
         empty^#(fstsplit(m, store)),
         fstsplit^#(m, store))
  , if1^#(store, m, false()) ->
    c_20(if3^#(store,
               m,
               empty(fstsplit(m, app(map_f(self(), nil()), store)))),
         empty^#(fstsplit(m, app(map_f(self(), nil()), store))),
         fstsplit^#(m, app(map_f(self(), nil()), store)),
         app^#(map_f(self(), nil()), store),
         map_f^#(self(), nil()))
  , if2^#(store, m, false()) ->
    c_21(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m),
         app^#(map_f(self(), nil()), sndsplit(m, store)),
         map_f^#(self(), nil()),
         sndsplit^#(m, store))
  , if3^#(store, m, false()) ->
    c_22(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m),
         sndsplit^#(m, app(map_f(self(), nil()), store)),
         app^#(map_f(self(), nil()), store),
         map_f^#(self(), nil())) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { fstsplit^#(s(n), cons(h, t)) -> c_1(fstsplit^#(n, t))
  , sndsplit^#(s(n), cons(h, t)) -> c_2(sndsplit^#(n, t))
  , leq^#(s(n), s(m)) -> c_3(leq^#(n, m))
  , length^#(cons(h, t)) -> c_4(length^#(t))
  , app^#(cons(h, t), x) -> c_5(app^#(t, x))
  , map_f^#(pid, cons(h, t)) -> c_6(map_f^#(pid, t))
  , process^#(store, m) ->
    c_7(if1^#(store, m, leq(m, length(store))),
        leq^#(m, length(store)),
        length^#(store))
  , if1^#(store, m, true()) ->
    c_8(if2^#(store, m, empty(fstsplit(m, store))),
        fstsplit^#(m, store))
  , if1^#(store, m, false()) ->
    c_9(if3^#(store,
              m,
              empty(fstsplit(m, app(map_f(self(), nil()), store)))),
        fstsplit^#(m, app(map_f(self(), nil()), store)),
        app^#(map_f(self(), nil()), store))
  , if2^#(store, m, false()) ->
    c_10(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m),
         app^#(map_f(self(), nil()), sndsplit(m, store)),
         sndsplit^#(m, store))
  , if3^#(store, m, false()) ->
    c_11(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m),
         sndsplit^#(m, app(map_f(self(), nil()), store)),
         app^#(map_f(self(), nil()), store)) }
Weak 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))
  , process(store, m) -> if1(store, m, leq(m, length(store)))
  , if1(store, m, true()) -> if2(store, m, empty(fstsplit(m, store)))
  , if1(store, m, false()) ->
    if3(store, m, empty(fstsplit(m, app(map_f(self(), nil()), store))))
  , if2(store, m, false()) ->
    process(app(map_f(self(), nil()), sndsplit(m, store)), m)
  , if3(store, m, false()) ->
    process(sndsplit(m, app(map_f(self(), nil()), store)), m) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { fstsplit(0(), x) -> nil()
    , fstsplit(s(n), nil()) -> nil()
    , fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
    , sndsplit(0(), x) -> x
    , sndsplit(s(n), nil()) -> nil()
    , sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
    , empty(nil()) -> true()
    , empty(cons(h, t)) -> false()
    , leq(0(), m) -> true()
    , leq(s(n), 0()) -> false()
    , leq(s(n), s(m)) -> leq(n, m)
    , length(nil()) -> 0()
    , length(cons(h, t)) -> s(length(t))
    , app(nil(), x) -> x
    , app(cons(h, t), x) -> cons(h, app(t, x))
    , map_f(pid, nil()) -> nil()
    , map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { fstsplit^#(s(n), cons(h, t)) -> c_1(fstsplit^#(n, t))
  , sndsplit^#(s(n), cons(h, t)) -> c_2(sndsplit^#(n, t))
  , leq^#(s(n), s(m)) -> c_3(leq^#(n, m))
  , length^#(cons(h, t)) -> c_4(length^#(t))
  , app^#(cons(h, t), x) -> c_5(app^#(t, x))
  , map_f^#(pid, cons(h, t)) -> c_6(map_f^#(pid, t))
  , process^#(store, m) ->
    c_7(if1^#(store, m, leq(m, length(store))),
        leq^#(m, length(store)),
        length^#(store))
  , if1^#(store, m, true()) ->
    c_8(if2^#(store, m, empty(fstsplit(m, store))),
        fstsplit^#(m, store))
  , if1^#(store, m, false()) ->
    c_9(if3^#(store,
              m,
              empty(fstsplit(m, app(map_f(self(), nil()), store)))),
        fstsplit^#(m, app(map_f(self(), nil()), store)),
        app^#(map_f(self(), nil()), store))
  , if2^#(store, m, false()) ->
    c_10(process^#(app(map_f(self(), nil()), sndsplit(m, store)), m),
         app^#(map_f(self(), nil()), sndsplit(m, store)),
         sndsplit^#(m, store))
  , if3^#(store, m, false()) ->
    c_11(process^#(sndsplit(m, app(map_f(self(), nil()), store)), m),
         sndsplit^#(m, app(map_f(self(), nil()), store)),
         app^#(map_f(self(), nil()), store)) }
Weak 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)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..