MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ f(x, Cons(x', xs)) ->
f(f[Ite][False][Ite](lt0(x, Cons(Nil(), Nil())), x, Cons(x', xs)),
f[Ite][False][Ite](lt0(x, Cons(Nil(), Nil())), x, Cons(x', xs)))
, f(x, Nil()) ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil()))))))))))))))))))))))))))))))))))))))))))
, lt0(x, Nil()) -> False()
, lt0(Cons(x', xs'), Cons(x, xs)) -> lt0(xs', xs)
, number42() ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil()))))))))))))))))))))))))))))))))))))))))))
, goal(x, y) -> Cons(f(x, y), Cons(g(x, y), Nil()))
, g(x, Cons(x', xs)) ->
g[Ite][False][Ite](lt0(x, Cons(Nil(), Nil())), x, Cons(x', xs))
, g(x, Nil()) ->
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Cons(Nil(),
Nil())))))))))))))))))))))))))))))))))))))))))) }
Weak Trs:
{ f[Ite][False][Ite](True(), x, y) -> x
, f[Ite][False][Ite](True(), x', Cons(x, xs)) -> xs
, f[Ite][False][Ite](False(), x, y) -> Cons(Cons(Nil(), Nil()), y)
, f[Ite][False][Ite](False(), Cons(x, xs), y) -> xs
, g[Ite][False][Ite](True(), x', Cons(x, xs)) -> g(x', xs)
, g[Ite][False][Ite](False(), Cons(x, xs), y) ->
g(xs, Cons(Cons(Nil(), Nil()), y)) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
following reason:
Computation stopped due to timeout after 60.0 seconds.
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
failed due to the following reason:
Computation stopped due to timeout after 30.0 seconds.
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
following reason:
The input cannot be shown compatible
2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
to the following reason:
The input cannot be shown compatible
3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Bounds with minimal-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
Arrrr..