MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ is_empty(nil()) -> true()
, is_empty(cons(x, l)) -> false()
, hd(cons(x, l)) -> x
, tl(cons(x, l)) -> cons(x, l)
, append(l1, l2) -> ifappend(l1, l2, is_empty(l1))
, ifappend(l1, l2, true()) -> l2
, ifappend(l1, l2, false()) -> cons(hd(l1), append(tl(l1), l2)) }
Obligation:
runtime complexity
Answer:
MAYBE
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:
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) 'WithProblem' failed due to the following reason:
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) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem' failed due to the following reason:
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) 'WithProblem' failed due to the following reason:
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) 'WithProblem' failed due to the following reason:
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) 'WithProblem' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'WithProblem' failed due to the following reason:
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) 'WithProblem' 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) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
following reason:
The processor is inapplicable, reason:
Processor only applicable for innermost runtime complexity analysis
2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
to the following reason:
The processor is inapplicable, reason:
Processor only applicable for innermost runtime complexity analysis
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 perSymbol-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with minimal-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
due to the following reason:
We add the following weak dependency pairs:
Strict DPs:
{ is_empty^#(nil()) -> c_1()
, is_empty^#(cons(x, l)) -> c_2()
, hd^#(cons(x, l)) -> c_3(x)
, tl^#(cons(x, l)) -> c_4(x, l)
, append^#(l1, l2) -> c_5(ifappend^#(l1, l2, is_empty(l1)))
, ifappend^#(l1, l2, true()) -> c_6(l2)
, ifappend^#(l1, l2, false()) ->
c_7(hd^#(l1), append^#(tl(l1), l2)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ is_empty^#(nil()) -> c_1()
, is_empty^#(cons(x, l)) -> c_2()
, hd^#(cons(x, l)) -> c_3(x)
, tl^#(cons(x, l)) -> c_4(x, l)
, append^#(l1, l2) -> c_5(ifappend^#(l1, l2, is_empty(l1)))
, ifappend^#(l1, l2, true()) -> c_6(l2)
, ifappend^#(l1, l2, false()) ->
c_7(hd^#(l1), append^#(tl(l1), l2)) }
Strict Trs:
{ is_empty(nil()) -> true()
, is_empty(cons(x, l)) -> false()
, hd(cons(x, l)) -> x
, tl(cons(x, l)) -> cons(x, l)
, append(l1, l2) -> ifappend(l1, l2, is_empty(l1))
, ifappend(l1, l2, true()) -> l2
, ifappend(l1, l2, false()) -> cons(hd(l1), append(tl(l1), l2)) }
Obligation:
runtime complexity
Answer:
MAYBE
We estimate the number of application of {1,2} by applications of
Pre({1,2}) = {3,4,6}. Here rules are labeled as follows:
DPs:
{ 1: is_empty^#(nil()) -> c_1()
, 2: is_empty^#(cons(x, l)) -> c_2()
, 3: hd^#(cons(x, l)) -> c_3(x)
, 4: tl^#(cons(x, l)) -> c_4(x, l)
, 5: append^#(l1, l2) -> c_5(ifappend^#(l1, l2, is_empty(l1)))
, 6: ifappend^#(l1, l2, true()) -> c_6(l2)
, 7: ifappend^#(l1, l2, false()) ->
c_7(hd^#(l1), append^#(tl(l1), l2)) }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ hd^#(cons(x, l)) -> c_3(x)
, tl^#(cons(x, l)) -> c_4(x, l)
, append^#(l1, l2) -> c_5(ifappend^#(l1, l2, is_empty(l1)))
, ifappend^#(l1, l2, true()) -> c_6(l2)
, ifappend^#(l1, l2, false()) ->
c_7(hd^#(l1), append^#(tl(l1), l2)) }
Strict Trs:
{ is_empty(nil()) -> true()
, is_empty(cons(x, l)) -> false()
, hd(cons(x, l)) -> x
, tl(cons(x, l)) -> cons(x, l)
, append(l1, l2) -> ifappend(l1, l2, is_empty(l1))
, ifappend(l1, l2, true()) -> l2
, ifappend(l1, l2, false()) -> cons(hd(l1), append(tl(l1), l2)) }
Weak DPs:
{ is_empty^#(nil()) -> c_1()
, is_empty^#(cons(x, l)) -> c_2() }
Obligation:
runtime complexity
Answer:
MAYBE
Empty strict component of the problem is NOT empty.
Arrrr..