MAYBE
Time: 0.029150
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)),
      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))),
          process(store, m) -> if1(store, m, leq(m, length 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)}
 DP:
  DP:
   {fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t),
    sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t),
                leq#(s n, s m) -> leq#(n, m),
            length# cons(h, t) -> length# t,
           app#(cons(h, t), x) -> app#(t, x),
       map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t)),
       map_f#(pid, cons(h, t)) -> map_f#(pid, t),
        if1#(store, m, true()) -> fstsplit#(m, store),
        if1#(store, m, true()) -> empty# fstsplit(m, store),
        if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)),
       if1#(store, m, false()) -> fstsplit#(m, app(map_f(self(), nil()), store)),
       if1#(store, m, false()) -> empty# fstsplit(m, app(map_f(self(), nil()), store)),
       if1#(store, m, false()) -> app#(map_f(self(), nil()), store),
       if1#(store, m, false()) -> map_f#(self(), nil()),
       if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))),
            process#(store, m) -> leq#(m, length store),
            process#(store, m) -> length# store,
            process#(store, m) -> if1#(store, m, leq(m, length store)),
       if2#(store, m, false()) -> sndsplit#(m, store),
       if2#(store, m, false()) -> app#(map_f(self(), nil()), sndsplit(m, store)),
       if2#(store, m, false()) -> map_f#(self(), nil()),
       if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m),
       if3#(store, m, false()) -> sndsplit#(m, app(map_f(self(), nil()), store)),
       if3#(store, m, false()) -> app#(map_f(self(), nil()), store),
       if3#(store, m, false()) -> map_f#(self(), nil()),
       if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m)}
  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)),
       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))),
           process(store, m) -> if1(store, m, leq(m, length 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)}
  UR:
   {         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)),
                      a(y, z) -> y,
                      a(y, z) -> z}
   EDG:
    {(if1#(store, m, false()) -> map_f#(self(), nil()), map_f#(pid, cons(h, t)) -> map_f#(pid, t))
     (if1#(store, m, false()) -> map_f#(self(), nil()), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t)))
     (if3#(store, m, false()) -> map_f#(self(), nil()), map_f#(pid, cons(h, t)) -> map_f#(pid, t))
     (if3#(store, m, false()) -> map_f#(self(), nil()), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t)))
     (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m))
     (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> map_f#(self(), nil()))
     (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> app#(map_f(self(), nil()), store))
     (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> sndsplit#(m, app(map_f(self(), nil()), store)))
     (if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m), process#(store, m) -> if1#(store, m, leq(m, length store)))
     (if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m), process#(store, m) -> length# store)
     (if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m), process#(store, m) -> leq#(m, length store))
     (if3#(store, m, false()) -> app#(map_f(self(), nil()), store), app#(cons(h, t), x) -> app#(t, x))
     (process#(store, m) -> length# store, length# cons(h, t) -> length# t)
     (fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t))
     (map_f#(pid, cons(h, t)) -> map_f#(pid, t), map_f#(pid, cons(h, t)) -> map_f#(pid, t))
     (map_f#(pid, cons(h, t)) -> map_f#(pid, t), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t)))
     (if2#(store, m, false()) -> sndsplit#(m, store), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t))
     (length# cons(h, t) -> length# t, length# cons(h, t) -> length# t)
     (if1#(store, m, false()) -> fstsplit#(m, app(map_f(self(), nil()), store)), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t))
     (if3#(store, m, false()) -> sndsplit#(m, app(map_f(self(), nil()), store)), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t))
     (if2#(store, m, false()) -> app#(map_f(self(), nil()), sndsplit(m, store)), app#(cons(h, t), x) -> app#(t, x))
     (map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t)), app#(cons(h, t), x) -> app#(t, x))
     (process#(store, m) -> leq#(m, length store), leq#(s n, s m) -> leq#(n, m))
     (if1#(store, m, true()) -> fstsplit#(m, store), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t))
     (leq#(s n, s m) -> leq#(n, m), leq#(s n, s m) -> leq#(n, m))
     (sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t))
     (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, true()) -> fstsplit#(m, store))
     (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, true()) -> empty# fstsplit(m, store))
     (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)))
     (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> fstsplit#(m, app(map_f(self(), nil()), store)))
     (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> empty# fstsplit(m, app(map_f(self(), nil()), store)))
     (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> app#(map_f(self(), nil()), store))
     (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> map_f#(self(), nil()))
     (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))))
     (app#(cons(h, t), x) -> app#(t, x), app#(cons(h, t), x) -> app#(t, x))
     (if1#(store, m, false()) -> app#(map_f(self(), nil()), store), app#(cons(h, t), x) -> app#(t, x))
     (if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m), process#(store, m) -> leq#(m, length store))
     (if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m), process#(store, m) -> length# store)
     (if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m), process#(store, m) -> if1#(store, m, leq(m, length store)))
     (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> sndsplit#(m, store))
     (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> app#(map_f(self(), nil()), sndsplit(m, store)))
     (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> map_f#(self(), nil()))
     (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m))
     (if2#(store, m, false()) -> map_f#(self(), nil()), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t)))
     (if2#(store, m, false()) -> map_f#(self(), nil()), map_f#(pid, cons(h, t)) -> map_f#(pid, t))}
    EDG:
     {(if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m))
      (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> map_f#(self(), nil()))
      (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> app#(map_f(self(), nil()), store))
      (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> sndsplit#(m, app(map_f(self(), nil()), store)))
      (if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m), process#(store, m) -> if1#(store, m, leq(m, length store)))
      (if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m), process#(store, m) -> length# store)
      (if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m), process#(store, m) -> leq#(m, length store))
      (if3#(store, m, false()) -> app#(map_f(self(), nil()), store), app#(cons(h, t), x) -> app#(t, x))
      (process#(store, m) -> length# store, length# cons(h, t) -> length# t)
      (fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t))
      (map_f#(pid, cons(h, t)) -> map_f#(pid, t), map_f#(pid, cons(h, t)) -> map_f#(pid, t))
      (map_f#(pid, cons(h, t)) -> map_f#(pid, t), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t)))
      (if2#(store, m, false()) -> sndsplit#(m, store), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t))
      (length# cons(h, t) -> length# t, length# cons(h, t) -> length# t)
      (if1#(store, m, false()) -> fstsplit#(m, app(map_f(self(), nil()), store)), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t))
      (if3#(store, m, false()) -> sndsplit#(m, app(map_f(self(), nil()), store)), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t))
      (if2#(store, m, false()) -> app#(map_f(self(), nil()), sndsplit(m, store)), app#(cons(h, t), x) -> app#(t, x))
      (process#(store, m) -> leq#(m, length store), leq#(s n, s m) -> leq#(n, m))
      (if1#(store, m, true()) -> fstsplit#(m, store), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t))
      (leq#(s n, s m) -> leq#(n, m), leq#(s n, s m) -> leq#(n, m))
      (sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t))
      (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, true()) -> fstsplit#(m, store))
      (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, true()) -> empty# fstsplit(m, store))
      (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)))
      (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> fstsplit#(m, app(map_f(self(), nil()), store)))
      (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> empty# fstsplit(m, app(map_f(self(), nil()), store)))
      (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> app#(map_f(self(), nil()), store))
      (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> map_f#(self(), nil()))
      (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))))
      (app#(cons(h, t), x) -> app#(t, x), app#(cons(h, t), x) -> app#(t, x))
      (if1#(store, m, false()) -> app#(map_f(self(), nil()), store), app#(cons(h, t), x) -> app#(t, x))
      (if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m), process#(store, m) -> leq#(m, length store))
      (if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m), process#(store, m) -> length# store)
      (if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m), process#(store, m) -> if1#(store, m, leq(m, length store)))
      (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> sndsplit#(m, store))
      (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> app#(map_f(self(), nil()), sndsplit(m, store)))
      (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> map_f#(self(), nil()))
      (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m))}
     EDG:
      {(if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m))
       (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> map_f#(self(), nil()))
       (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> app#(map_f(self(), nil()), store))
       (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> sndsplit#(m, app(map_f(self(), nil()), store)))
       (if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m), process#(store, m) -> if1#(store, m, leq(m, length store)))
       (if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m), process#(store, m) -> length# store)
       (if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m), process#(store, m) -> leq#(m, length store))
       (process#(store, m) -> length# store, length# cons(h, t) -> length# t)
       (fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t))
       (map_f#(pid, cons(h, t)) -> map_f#(pid, t), map_f#(pid, cons(h, t)) -> map_f#(pid, t))
       (map_f#(pid, cons(h, t)) -> map_f#(pid, t), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t)))
       (if2#(store, m, false()) -> sndsplit#(m, store), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t))
       (length# cons(h, t) -> length# t, length# cons(h, t) -> length# t)
       (if1#(store, m, false()) -> fstsplit#(m, app(map_f(self(), nil()), store)), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t))
       (if3#(store, m, false()) -> sndsplit#(m, app(map_f(self(), nil()), store)), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t))
       (process#(store, m) -> leq#(m, length store), leq#(s n, s m) -> leq#(n, m))
       (if1#(store, m, true()) -> fstsplit#(m, store), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t))
       (leq#(s n, s m) -> leq#(n, m), leq#(s n, s m) -> leq#(n, m))
       (sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t))
       (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, true()) -> fstsplit#(m, store))
       (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, true()) -> empty# fstsplit(m, store))
       (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)))
       (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> fstsplit#(m, app(map_f(self(), nil()), store)))
       (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> empty# fstsplit(m, app(map_f(self(), nil()), store)))
       (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> app#(map_f(self(), nil()), store))
       (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> map_f#(self(), nil()))
       (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))))
       (app#(cons(h, t), x) -> app#(t, x), app#(cons(h, t), x) -> app#(t, x))
       (if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m), process#(store, m) -> leq#(m, length store))
       (if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m), process#(store, m) -> length# store)
       (if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m), process#(store, m) -> if1#(store, m, leq(m, length store)))
       (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> sndsplit#(m, store))
       (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> app#(map_f(self(), nil()), sndsplit(m, store)))
       (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> map_f#(self(), nil()))
       (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m))}
      EDG:
       {(if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m))
        (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> map_f#(self(), nil()))
        (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> app#(map_f(self(), nil()), store))
        (if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))), if3#(store, m, false()) -> sndsplit#(m, app(map_f(self(), nil()), store)))
        (if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m), process#(store, m) -> if1#(store, m, leq(m, length store)))
        (if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m), process#(store, m) -> length# store)
        (if3#(store, m, false()) -> process#(sndsplit(m, app(map_f(self(), nil()), store)), m), process#(store, m) -> leq#(m, length store))
        (process#(store, m) -> length# store, length# cons(h, t) -> length# t)
        (fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t))
        (map_f#(pid, cons(h, t)) -> map_f#(pid, t), map_f#(pid, cons(h, t)) -> map_f#(pid, t))
        (map_f#(pid, cons(h, t)) -> map_f#(pid, t), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t)))
        (if2#(store, m, false()) -> sndsplit#(m, store), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t))
        (length# cons(h, t) -> length# t, length# cons(h, t) -> length# t)
        (if1#(store, m, false()) -> fstsplit#(m, app(map_f(self(), nil()), store)), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t))
        (if3#(store, m, false()) -> sndsplit#(m, app(map_f(self(), nil()), store)), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t))
        (process#(store, m) -> leq#(m, length store), leq#(s n, s m) -> leq#(n, m))
        (if1#(store, m, true()) -> fstsplit#(m, store), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t))
        (leq#(s n, s m) -> leq#(n, m), leq#(s n, s m) -> leq#(n, m))
        (sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t))
        (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, true()) -> fstsplit#(m, store))
        (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, true()) -> empty# fstsplit(m, store))
        (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)))
        (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> fstsplit#(m, app(map_f(self(), nil()), store)))
        (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> empty# fstsplit(m, app(map_f(self(), nil()), store)))
        (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> app#(map_f(self(), nil()), store))
        (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> map_f#(self(), nil()))
        (process#(store, m) -> if1#(store, m, leq(m, length store)), if1#(store, m, false()) -> if3#(store, m, empty fstsplit(m, app(map_f(self(), nil()), store))))
        (app#(cons(h, t), x) -> app#(t, x), app#(cons(h, t), x) -> app#(t, x))
        (if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m), process#(store, m) -> leq#(m, length store))
        (if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m), process#(store, m) -> length# store)
        (if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m), process#(store, m) -> if1#(store, m, leq(m, length store)))
        (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> sndsplit#(m, store))
        (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> app#(map_f(self(), nil()), sndsplit(m, store)))
        (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> map_f#(self(), nil()))
        (if1#(store, m, true()) -> if2#(store, m, empty fstsplit(m, store)), if2#(store, m, false()) -> process#(app(map_f(self(), nil()), sndsplit(m, store)), m))}
       STATUS:
        arrows: 0.948225
        SCCS (7):
         Scc:
          {map_f#(pid, cons(h, t)) -> map_f#(pid, t)}
         Scc:
          {app#(cons(h, t), x) -> app#(t, x)}
         Scc:
          { 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))),
                process#(store, m) -> if1#(store, m, leq(m, length 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)}
         Scc:
          {fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t)}
         Scc:
          {length# cons(h, t) -> length# t}
         Scc:
          {leq#(s n, s m) -> leq#(n, m)}
         Scc:
          {sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t)}
         
         SCC (1):
          Strict:
           {map_f#(pid, cons(h, t)) -> map_f#(pid, t)}
          Weak:
          {         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)),
               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))),
                   process(store, m) -> if1(store, m, leq(m, length 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)}
          Open
         
         SCC (1):
          Strict:
           {app#(cons(h, t), x) -> app#(t, x)}
          Weak:
          {         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)),
               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))),
                   process(store, m) -> if1(store, m, leq(m, length 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)}
          Open
         SCC (5):
          Strict:
           { 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))),
                 process#(store, m) -> if1#(store, m, leq(m, length 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)}
          Weak:
          {         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)),
               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))),
                   process(store, m) -> if1(store, m, leq(m, length 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)}
          Open
         
         
         
         
         
         
         SCC (1):
          Strict:
           {fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t)}
          Weak:
          {         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)),
               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))),
                   process(store, m) -> if1(store, m, leq(m, length 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)}
          Open
         
         SCC (1):
          Strict:
           {length# cons(h, t) -> length# t}
          Weak:
          {         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)),
               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))),
                   process(store, m) -> if1(store, m, leq(m, length 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)}
          Open
         
         SCC (1):
          Strict:
           {leq#(s n, s m) -> leq#(n, m)}
          Weak:
          {         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)),
               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))),
                   process(store, m) -> if1(store, m, leq(m, length 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)}
          Open
         
         
         SCC (1):
          Strict:
           {sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t)}
          Weak:
          {         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)),
               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))),
                   process(store, m) -> if1(store, m, leq(m, length 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)}
          Open