interpretations
TIMEOUT
We are left with following problem, upon which TcT provides the
certificate TIMEOUT.
Strict Trs:
{ test(x_0, y) -> True()
, test(x_0, y) -> False()
, append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2)
, match_0(l1_2, l2_1, Nil()) -> l2_1
, match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1))
, part(a_4, l_3) -> match_1(a_4, l_3, l_3)
, match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil())
, match_1(a_4, l_3, Cons(x, l')) ->
match_2(x, l', a_4, l_3, part(a_4, l'))
, match_2(x, l', a_4, l_3, Pair(l1, l2)) ->
match_3(l1, l2, x, l', a_4, l_3, test(a_4, x))
, match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2))
, match_3(l1, l2, x, l', a_4, l_3, False()) ->
Pair(Cons(x, l1), l2)
, quick(l_5) -> match_4(l_5, l_5)
, match_4(l_5, Nil()) -> Nil()
, match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l'))
, match_5(a, l', l_5, Pair(l1, l2)) ->
append(quick(l1), Cons(a, quick(l2))) }
Obligation:
innermost runtime complexity
Answer:
TIMEOUT
Computation stopped due to timeout after 20.0 seconds.
Arrrr..
lmpo
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ test(x_0, y) -> True()
, test(x_0, y) -> False()
, append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2)
, match_0(l1_2, l2_1, Nil()) -> l2_1
, match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1))
, part(a_4, l_3) -> match_1(a_4, l_3, l_3)
, match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil())
, match_1(a_4, l_3, Cons(x, l')) ->
match_2(x, l', a_4, l_3, part(a_4, l'))
, match_2(x, l', a_4, l_3, Pair(l1, l2)) ->
match_3(l1, l2, x, l', a_4, l_3, test(a_4, x))
, match_3(l1, l2, x, l', a_4, l_3, False()) ->
Pair(Cons(x, l1), l2)
, match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2))
, quick(l_5) -> match_4(l_5, l_5)
, match_4(l_5, Nil()) -> Nil()
, match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l'))
, match_5(a, l', l_5, Pair(l1, l2)) ->
append(quick(l1), Cons(a, quick(l2))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
mpo
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ test(x_0, y) -> True()
, test(x_0, y) -> False()
, append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2)
, match_0(l1_2, l2_1, Nil()) -> l2_1
, match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1))
, part(a_4, l_3) -> match_1(a_4, l_3, l_3)
, match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil())
, match_1(a_4, l_3, Cons(x, l')) ->
match_2(x, l', a_4, l_3, part(a_4, l'))
, match_2(x, l', a_4, l_3, Pair(l1, l2)) ->
match_3(l1, l2, x, l', a_4, l_3, test(a_4, x))
, match_3(l1, l2, x, l', a_4, l_3, False()) ->
Pair(Cons(x, l1), l2)
, match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2))
, quick(l_5) -> match_4(l_5, l_5)
, match_4(l_5, Nil()) -> Nil()
, match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l'))
, match_5(a, l', l_5, Pair(l1, l2)) ->
append(quick(l1), Cons(a, quick(l2))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ test(x_0, y) -> True()
, test(x_0, y) -> False()
, append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2)
, match_0(l1_2, l2_1, Nil()) -> l2_1
, match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1))
, part(a_4, l_3) -> match_1(a_4, l_3, l_3)
, match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil())
, match_1(a_4, l_3, Cons(x, l')) ->
match_2(x, l', a_4, l_3, part(a_4, l'))
, match_2(x, l', a_4, l_3, Pair(l1, l2)) ->
match_3(l1, l2, x, l', a_4, l_3, test(a_4, x))
, match_3(l1, l2, x, l', a_4, l_3, False()) ->
Pair(Cons(x, l1), l2)
, match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2))
, quick(l_5) -> match_4(l_5, l_5)
, match_4(l_5, Nil()) -> Nil()
, match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l'))
, match_5(a, l', l_5, Pair(l1, l2)) ->
append(quick(l1), Cons(a, quick(l2))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar-ps
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ test(x_0, y) -> True()
, test(x_0, y) -> False()
, append(l1_2, l2_1) -> match_0(l1_2, l2_1, l1_2)
, match_0(l1_2, l2_1, Nil()) -> l2_1
, match_0(l1_2, l2_1, Cons(x, l)) -> Cons(x, append(l, l2_1))
, part(a_4, l_3) -> match_1(a_4, l_3, l_3)
, match_1(a_4, l_3, Nil()) -> Pair(Nil(), Nil())
, match_1(a_4, l_3, Cons(x, l')) ->
match_2(x, l', a_4, l_3, part(a_4, l'))
, match_2(x, l', a_4, l_3, Pair(l1, l2)) ->
match_3(l1, l2, x, l', a_4, l_3, test(a_4, x))
, match_3(l1, l2, x, l', a_4, l_3, False()) ->
Pair(Cons(x, l1), l2)
, match_3(l1, l2, x, l', a_4, l_3, True()) -> Pair(l1, Cons(x, l2))
, quick(l_5) -> match_4(l_5, l_5)
, match_4(l_5, Nil()) -> Nil()
, match_4(l_5, Cons(a, l')) -> match_5(a, l', l_5, part(a, l'))
, match_5(a, l', l_5, Pair(l1, l2)) ->
append(quick(l1), Cons(a, quick(l2))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..