MAYBE Time: 0.033009 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, if_1(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring(st_1, in_2, st_2, in_3, st_3, m) -> if_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_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)} 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), if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, st_1), if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, st_1), if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> fstsplit#(m, st_1), ring#(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) -> empty# map_f(two(), head in_2), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(three(), head in_3), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_2), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_3), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_2, ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_3, ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(two(), head in_2), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(three(), head in_3), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_2, ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_3, ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_1#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_1)), 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_2#(st_1, in_2, st_2, in_3, st_3, m, true()) -> fstsplit#(m, st_2), if_2#(st_1, in_2, st_2, in_3, st_3, m, true()) -> empty# fstsplit(m, st_2), if_2#(st_1, in_2, st_2, in_3, st_3, m, true()) -> if_3#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_2)), if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, app(map_f(two(), head in_2), st_2)), if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> empty# fstsplit(m, app(map_f(two(), head in_2), st_2)), if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> app#(map_f(two(), head in_2), st_2), if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(two(), head in_2), if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> head# in_2, if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> 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()) -> fstsplit#(m, st_2), if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, st_2), if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m), if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, app(map_f(two(), head in_2), st_2)), if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, app(map_f(two(), head in_2), st_2)), if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> app#(map_f(two(), head in_2), st_2), if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(two(), head in_2), if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> head# in_2, if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> tail# in_2, if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> tail# in_2, if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), if_6#(st_1, in_2, st_2, in_3, st_3, m, true()) -> fstsplit#(m, st_3), if_6#(st_1, in_2, st_2, in_3, st_3, m, true()) -> empty# fstsplit(m, st_3), if_6#(st_1, in_2, st_2, in_3, st_3, m, true()) -> if_7#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_3)), if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, app(map_f(three(), head in_3), st_3)), if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> empty# fstsplit(m, app(map_f(three(), head in_3), st_3)), if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> app#(map_f(three(), head in_3), st_3), if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(three(), head in_3), if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> head# in_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()) -> sndsplit#(m, st_3), if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m), if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, app(map_f(three(), head in_3), st_3)), if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> app#(map_f(three(), head in_3), st_3), if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(three(), head in_3), if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> head# in_3, if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> tail# in_3, if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), if_9#(st_1, in_2, st_2, in_3, st_3, m, true()) -> tail# in_3, if_9#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, in_2, st_2, tail in_3, st_3, m)} 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, if_1(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring(st_1, in_2, st_2, in_3, st_3, m) -> if_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_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)} 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)), head cons(h, t) -> h, tail cons(h, t) -> t, a(y, z) -> y, a(y, z) -> z} EDG: { (ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_3, length# cons(h, t) -> length# t) (if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, st_2), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, 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)), if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_1#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_1)), if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, st_1)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_1#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_1)), if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, st_1)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_5#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(two(), head in_2)), if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_5#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(two(), head in_2)), if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> tail# in_2) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_9#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(three(), head in_3)), if_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)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_9#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(three(), head in_3)), if_9#(st_1, in_2, st_2, in_3, st_3, m, true()) -> tail# in_3) (if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> if_4#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, app(map_f(two(), head in_2), st_2))), if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m)) (if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> if_4#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, app(map_f(two(), head in_2), st_2))), if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> tail# in_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_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> head# in_2) (if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> if_4#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, app(map_f(two(), head in_2), st_2))), if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(two(), head in_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_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> app#(map_f(two(), head in_2), 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_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, app(map_f(two(), head in_2), 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_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, app(map_f(two(), head in_2), st_2))) (if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> if_8#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, app(map_f(three(), head in_3), st_3))), if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m)) (if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> if_8#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, app(map_f(three(), head in_3), st_3))), if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> tail# in_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_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> head# in_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_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(three(), head in_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_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> app#(map_f(three(), head in_3), 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_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, app(map_f(three(), head in_3), st_3))) (if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_9#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(three(), head in_3))) (if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3))) (if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_5#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(two(), head in_2))) (if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length 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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_1#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_1))) (if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_3) (if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(three(), head in_3)) (if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(two(), head in_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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_3) (if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# 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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_3)) (if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length 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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(three(), head in_3)) (if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(two(), head in_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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# fstsplit(m, st_1)) (if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> fstsplit#(m, st_1)) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_9#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(three(), head in_3))) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3))) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_5#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(two(), head in_2))) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2))) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_1#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_1))) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_3) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_2) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(three(), head in_3)) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(two(), head in_2)) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_3) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_2) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_3)) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_2)) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(three(), head in_3)) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(two(), head in_2)) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# fstsplit(m, st_1)) (if_5#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, tail in_2, st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> fstsplit#(m, st_1)) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_9#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(three(), head in_3))) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3))) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_5#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(two(), head in_2))) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2))) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_1#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_1))) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_3) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_2) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(three(), head in_3)) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(two(), head in_2)) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_3) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_2) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_3)) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_2)) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(three(), head in_3)) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(two(), head in_2)) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# fstsplit(m, st_1)) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, tail in_3, sndsplit(m, app(map_f(three(), head in_3), st_3)), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> fstsplit#(m, st_1)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_2, length# cons(h, t) -> length# t) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, st_1), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> fstsplit#(m, st_1), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_3), leq#(s n, s m) -> leq#(n, m)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(three(), head in_3), map_f#(pid, cons(h, t)) -> map_f#(pid, t)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(three(), head in_3), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t))) (if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(two(), head in_2), map_f#(pid, cons(h, t)) -> map_f#(pid, t)) (if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(two(), head in_2), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t))) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, app(map_f(two(), head in_2), st_2)), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t)) (if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, app(map_f(three(), head in_3), st_3)), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t)) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, app(map_f(three(), head in_3), st_3)), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, 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))) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> app#(map_f(three(), head in_3), st_3), app#(cons(h, t), x) -> app#(t, x)) (if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, st_3), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t)) (if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> app#(map_f(two(), head in_2), st_2), app#(cons(h, t), x) -> app#(t, x)) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> app#(map_f(two(), head in_2), st_2), app#(cons(h, t), x) -> app#(t, x)) (leq#(s n, s m) -> leq#(n, m), leq#(s n, s m) -> leq#(n, m)) (length# cons(h, t) -> length# t, length# cons(h, t) -> length# t) (if_6#(st_1, in_2, st_2, in_3, st_3, m, true()) -> fstsplit#(m, st_3), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t)) (app#(cons(h, t), x) -> app#(t, x), app#(cons(h, t), x) -> app#(t, x)) (if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> app#(map_f(three(), head in_3), st_3), app#(cons(h, t), x) -> app#(t, x)) (sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t)) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(three(), head in_3), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t))) (if_8#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(three(), head in_3), map_f#(pid, cons(h, t)) -> map_f#(pid, t)) (if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(three(), head in_3), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t))) (if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(three(), head in_3), map_f#(pid, cons(h, t)) -> map_f#(pid, t)) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(two(), head in_2), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t))) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(two(), head in_2), map_f#(pid, cons(h, t)) -> map_f#(pid, t)) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, app(map_f(two(), head in_2), st_2)), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t)) (if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, app(map_f(two(), head in_2), st_2)), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(two(), head in_2), map_f#(pid, cons(h, t)) -> app#(f(pid, h), map_f(pid, t))) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(two(), head in_2), map_f#(pid, cons(h, t)) -> map_f#(pid, t)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_2), leq#(s n, s m) -> leq#(n, m)) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, st_1), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t)) (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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> fstsplit#(m, st_1)) (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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# fstsplit(m, st_1)) (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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(two(), head in_2)) (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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(three(), head in_3)) (if_9#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, in_2, st_2, tail in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_2)) (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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_3)) (if_9#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, in_2, st_2, tail in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_2) (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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_3) (if_9#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, in_2, st_2, tail in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(two(), head in_2)) (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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(three(), head in_3)) (if_9#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, in_2, st_2, tail in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_2) (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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_3) (if_9#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, in_2, st_2, tail in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_1#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_1))) (if_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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2))) (if_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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_5#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(two(), head in_2))) (if_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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3))) (if_9#(st_1, in_2, st_2, in_3, st_3, m, true()) -> ring#(st_1, in_2, st_2, tail in_3, st_3, m), 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_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> fstsplit#(m, st_1)) (if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# fstsplit(m, st_1)) (if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(two(), head in_2)) (if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(three(), head in_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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_2)) (if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length 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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_2) (if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# 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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(two(), head in_2)) (if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(three(), head in_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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_2) (if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_1#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_1))) (if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2))) (if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_5#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(two(), head in_2))) (if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length 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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_9#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(three(), head in_3))) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> fstsplit#(m, st_1)) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# fstsplit(m, st_1)) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(two(), head in_2)) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(three(), head in_3)) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_2)) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_3)) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_2) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_3) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(two(), head in_2)) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(three(), head in_3)) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_2) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_3) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_1#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_1))) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2))) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_5#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(two(), head in_2))) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3))) (if_4#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, tail in_2, sndsplit(m, app(map_f(two(), head in_2), st_2)), cons(fstsplit(m, app(map_f(two(), head in_2), st_2)), in_3), st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> fstsplit#(m, st_1)) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# fstsplit(m, st_1)) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> empty# map_f(two(), head in_2)) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_2)) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> leq#(m, length st_3)) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_2) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> length# st_3) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> map_f#(two(), head in_2)) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> 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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> head# in_2) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> 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), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_1#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_1))) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2))) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_5#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(two(), head in_2))) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3))) (if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_9#(st_1, in_2, st_2, in_3, st_3, m, empty map_f(three(), head in_3))) (if_6#(st_1, in_2, st_2, in_3, st_3, m, true()) -> if_7#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_3)), if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, st_3)) (if_6#(st_1, in_2, st_2, in_3, st_3, m, true()) -> if_7#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_3)), if_7#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)) (if_2#(st_1, in_2, st_2, in_3, st_3, m, true()) -> if_3#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_2)), if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, st_2)) (if_2#(st_1, in_2, st_2, in_3, st_3, m, true()) -> if_3#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_2)), if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> sndsplit#(m, st_2)) (if_2#(st_1, in_2, st_2, in_3, st_3, m, true()) -> if_3#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_2)), if_3#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3)), if_6#(st_1, in_2, st_2, in_3, st_3, m, true()) -> fstsplit#(m, st_3)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3)), if_6#(st_1, in_2, st_2, in_3, st_3, m, true()) -> empty# fstsplit(m, st_3)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3)), if_6#(st_1, in_2, st_2, in_3, st_3, m, true()) -> if_7#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_3))) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3)), if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, app(map_f(three(), head in_3), st_3))) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3)), if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> empty# fstsplit(m, app(map_f(three(), head in_3), st_3))) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3)), if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> app#(map_f(three(), head in_3), st_3)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3)), if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(three(), head in_3)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3)), if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> head# in_3) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_6#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_3)), if_6#(st_1, in_2, st_2, in_3, st_3, m, false()) -> if_8#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, app(map_f(three(), head in_3), st_3)))) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2)), if_2#(st_1, in_2, st_2, in_3, st_3, m, true()) -> fstsplit#(m, st_2)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2)), if_2#(st_1, in_2, st_2, in_3, st_3, m, true()) -> empty# fstsplit(m, st_2)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2)), if_2#(st_1, in_2, st_2, in_3, st_3, m, true()) -> if_3#(st_1, in_2, st_2, in_3, st_3, m, empty fstsplit(m, st_2))) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2)), if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> fstsplit#(m, app(map_f(two(), head in_2), st_2))) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2)), if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> empty# fstsplit(m, app(map_f(two(), head in_2), st_2))) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2)), if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> app#(map_f(two(), head in_2), st_2)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2)), if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> map_f#(two(), head in_2)) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2)), if_2#(st_1, in_2, st_2, in_3, st_3, m, false()) -> head# in_2) (ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_2#(st_1, in_2, st_2, in_3, st_3, m, leq(m, length st_2)), if_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()) -> sndsplit#(m, st_2), sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t)) (if_2#(st_1, in_2, st_2, in_3, st_3, m, true()) -> fstsplit#(m, st_2), fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t)) } STATUS: arrows: 0.955001 SCCS (7): Scc: {if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_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_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)} Scc: {app#(cons(h, t), x) -> app#(t, x)} Scc: {map_f#(pid, cons(h, t)) -> map_f#(pid, t)} Scc: {leq#(s n, s m) -> leq#(n, m)} Scc: {sndsplit#(s n, cons(h, t)) -> sndsplit#(n, t)} Scc: {fstsplit#(s n, cons(h, t)) -> fstsplit#(n, t)} Scc: {length# cons(h, t) -> length# t} SCC (16): Strict: {if_1#(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring#(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring#(st_1, in_2, st_2, in_3, st_3, m) -> if_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_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: { 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, if_1(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring(st_1, in_2, st_2, in_3, st_3, m) -> if_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_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)} 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)), head cons(h, t) -> h, tail cons(h, t) -> t, if_1(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring(st_1, in_2, st_2, in_3, st_3, m) -> if_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_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)} Open 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)), head cons(h, t) -> h, tail cons(h, t) -> t, if_1(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring(st_1, in_2, st_2, in_3, st_3, m) -> if_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_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)} 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)), head cons(h, t) -> h, tail cons(h, t) -> t, if_1(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring(st_1, in_2, st_2, in_3, st_3, m) -> if_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_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)} 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)), head cons(h, t) -> h, tail cons(h, t) -> t, if_1(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring(st_1, in_2, st_2, in_3, st_3, m) -> if_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_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)} 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)), head cons(h, t) -> h, tail cons(h, t) -> t, if_1(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring(st_1, in_2, st_2, in_3, st_3, m) -> if_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_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)} 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)), head cons(h, t) -> h, tail cons(h, t) -> t, if_1(st_1, in_2, st_2, in_3, st_3, m, false()) -> ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m), ring(st_1, in_2, st_2, in_3, st_3, m) -> if_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_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)} Open