MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { leq(0(), x) -> tt() , leq(s(x), 0()) -> ff() , leq(s(x), s(y)) -> leq(x, y) , split(nil()) -> app(nil(), nil()) , split(cons(x, nil())) -> app(cons(x, nil()), nil()) , split(cons(x, cons(y, xs))) -> split1(x, y, split(xs)) , split1(x, y, app(xs, ys)) -> app(cons(x, xs), cons(y, ys)) , merge(xs, []()) -> xs , merge(cons(x, xs), cons(y, ys)) -> ifmerge(leq(x, y), x, y, xs, ys) , merge([](), xs) -> xs , ifmerge(tt(), x, y, xs, ys) -> cons(x, merge(xs, cons(y, ys))) , ifmerge(ff(), x, y, xs, ys) -> cons(y, merge(cons(x, xs), ys)) , mergesort(xs) -> mergesort1(split(xs)) , mergesort1(app(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { leq^#(0(), x) -> c_1() , leq^#(s(x), 0()) -> c_2() , leq^#(s(x), s(y)) -> c_3(leq^#(x, y)) , split^#(nil()) -> c_4() , split^#(cons(x, nil())) -> c_5() , split^#(cons(x, cons(y, xs))) -> c_6(split1^#(x, y, split(xs)), split^#(xs)) , split1^#(x, y, app(xs, ys)) -> c_7() , merge^#(xs, []()) -> c_8() , merge^#(cons(x, xs), cons(y, ys)) -> c_9(ifmerge^#(leq(x, y), x, y, xs, ys), leq^#(x, y)) , merge^#([](), xs) -> c_10() , ifmerge^#(tt(), x, y, xs, ys) -> c_11(merge^#(xs, cons(y, ys))) , ifmerge^#(ff(), x, y, xs, ys) -> c_12(merge^#(cons(x, xs), ys)) , mergesort^#(xs) -> c_13(mergesort1^#(split(xs)), split^#(xs)) , mergesort1^#(app(xs, ys)) -> c_14(merge^#(mergesort(xs), mergesort(ys)), mergesort^#(xs), mergesort^#(ys)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { leq^#(0(), x) -> c_1() , leq^#(s(x), 0()) -> c_2() , leq^#(s(x), s(y)) -> c_3(leq^#(x, y)) , split^#(nil()) -> c_4() , split^#(cons(x, nil())) -> c_5() , split^#(cons(x, cons(y, xs))) -> c_6(split1^#(x, y, split(xs)), split^#(xs)) , split1^#(x, y, app(xs, ys)) -> c_7() , merge^#(xs, []()) -> c_8() , merge^#(cons(x, xs), cons(y, ys)) -> c_9(ifmerge^#(leq(x, y), x, y, xs, ys), leq^#(x, y)) , merge^#([](), xs) -> c_10() , ifmerge^#(tt(), x, y, xs, ys) -> c_11(merge^#(xs, cons(y, ys))) , ifmerge^#(ff(), x, y, xs, ys) -> c_12(merge^#(cons(x, xs), ys)) , mergesort^#(xs) -> c_13(mergesort1^#(split(xs)), split^#(xs)) , mergesort1^#(app(xs, ys)) -> c_14(merge^#(mergesort(xs), mergesort(ys)), mergesort^#(xs), mergesort^#(ys)) } Weak Trs: { leq(0(), x) -> tt() , leq(s(x), 0()) -> ff() , leq(s(x), s(y)) -> leq(x, y) , split(nil()) -> app(nil(), nil()) , split(cons(x, nil())) -> app(cons(x, nil()), nil()) , split(cons(x, cons(y, xs))) -> split1(x, y, split(xs)) , split1(x, y, app(xs, ys)) -> app(cons(x, xs), cons(y, ys)) , merge(xs, []()) -> xs , merge(cons(x, xs), cons(y, ys)) -> ifmerge(leq(x, y), x, y, xs, ys) , merge([](), xs) -> xs , ifmerge(tt(), x, y, xs, ys) -> cons(x, merge(xs, cons(y, ys))) , ifmerge(ff(), x, y, xs, ys) -> cons(y, merge(cons(x, xs), ys)) , mergesort(xs) -> mergesort1(split(xs)) , mergesort1(app(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,4,5,7,8,10} by applications of Pre({1,2,4,5,7,8,10}) = {3,6,9,11,12,13,14}. Here rules are labeled as follows: DPs: { 1: leq^#(0(), x) -> c_1() , 2: leq^#(s(x), 0()) -> c_2() , 3: leq^#(s(x), s(y)) -> c_3(leq^#(x, y)) , 4: split^#(nil()) -> c_4() , 5: split^#(cons(x, nil())) -> c_5() , 6: split^#(cons(x, cons(y, xs))) -> c_6(split1^#(x, y, split(xs)), split^#(xs)) , 7: split1^#(x, y, app(xs, ys)) -> c_7() , 8: merge^#(xs, []()) -> c_8() , 9: merge^#(cons(x, xs), cons(y, ys)) -> c_9(ifmerge^#(leq(x, y), x, y, xs, ys), leq^#(x, y)) , 10: merge^#([](), xs) -> c_10() , 11: ifmerge^#(tt(), x, y, xs, ys) -> c_11(merge^#(xs, cons(y, ys))) , 12: ifmerge^#(ff(), x, y, xs, ys) -> c_12(merge^#(cons(x, xs), ys)) , 13: mergesort^#(xs) -> c_13(mergesort1^#(split(xs)), split^#(xs)) , 14: mergesort1^#(app(xs, ys)) -> c_14(merge^#(mergesort(xs), mergesort(ys)), mergesort^#(xs), mergesort^#(ys)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { leq^#(s(x), s(y)) -> c_3(leq^#(x, y)) , split^#(cons(x, cons(y, xs))) -> c_6(split1^#(x, y, split(xs)), split^#(xs)) , merge^#(cons(x, xs), cons(y, ys)) -> c_9(ifmerge^#(leq(x, y), x, y, xs, ys), leq^#(x, y)) , ifmerge^#(tt(), x, y, xs, ys) -> c_11(merge^#(xs, cons(y, ys))) , ifmerge^#(ff(), x, y, xs, ys) -> c_12(merge^#(cons(x, xs), ys)) , mergesort^#(xs) -> c_13(mergesort1^#(split(xs)), split^#(xs)) , mergesort1^#(app(xs, ys)) -> c_14(merge^#(mergesort(xs), mergesort(ys)), mergesort^#(xs), mergesort^#(ys)) } Weak DPs: { leq^#(0(), x) -> c_1() , leq^#(s(x), 0()) -> c_2() , split^#(nil()) -> c_4() , split^#(cons(x, nil())) -> c_5() , split1^#(x, y, app(xs, ys)) -> c_7() , merge^#(xs, []()) -> c_8() , merge^#([](), xs) -> c_10() } Weak Trs: { leq(0(), x) -> tt() , leq(s(x), 0()) -> ff() , leq(s(x), s(y)) -> leq(x, y) , split(nil()) -> app(nil(), nil()) , split(cons(x, nil())) -> app(cons(x, nil()), nil()) , split(cons(x, cons(y, xs))) -> split1(x, y, split(xs)) , split1(x, y, app(xs, ys)) -> app(cons(x, xs), cons(y, ys)) , merge(xs, []()) -> xs , merge(cons(x, xs), cons(y, ys)) -> ifmerge(leq(x, y), x, y, xs, ys) , merge([](), xs) -> xs , ifmerge(tt(), x, y, xs, ys) -> cons(x, merge(xs, cons(y, ys))) , ifmerge(ff(), x, y, xs, ys) -> cons(y, merge(cons(x, xs), ys)) , mergesort(xs) -> mergesort1(split(xs)) , mergesort1(app(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { leq^#(0(), x) -> c_1() , leq^#(s(x), 0()) -> c_2() , split^#(nil()) -> c_4() , split^#(cons(x, nil())) -> c_5() , split1^#(x, y, app(xs, ys)) -> c_7() , merge^#(xs, []()) -> c_8() , merge^#([](), xs) -> c_10() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { leq^#(s(x), s(y)) -> c_3(leq^#(x, y)) , split^#(cons(x, cons(y, xs))) -> c_6(split1^#(x, y, split(xs)), split^#(xs)) , merge^#(cons(x, xs), cons(y, ys)) -> c_9(ifmerge^#(leq(x, y), x, y, xs, ys), leq^#(x, y)) , ifmerge^#(tt(), x, y, xs, ys) -> c_11(merge^#(xs, cons(y, ys))) , ifmerge^#(ff(), x, y, xs, ys) -> c_12(merge^#(cons(x, xs), ys)) , mergesort^#(xs) -> c_13(mergesort1^#(split(xs)), split^#(xs)) , mergesort1^#(app(xs, ys)) -> c_14(merge^#(mergesort(xs), mergesort(ys)), mergesort^#(xs), mergesort^#(ys)) } Weak Trs: { leq(0(), x) -> tt() , leq(s(x), 0()) -> ff() , leq(s(x), s(y)) -> leq(x, y) , split(nil()) -> app(nil(), nil()) , split(cons(x, nil())) -> app(cons(x, nil()), nil()) , split(cons(x, cons(y, xs))) -> split1(x, y, split(xs)) , split1(x, y, app(xs, ys)) -> app(cons(x, xs), cons(y, ys)) , merge(xs, []()) -> xs , merge(cons(x, xs), cons(y, ys)) -> ifmerge(leq(x, y), x, y, xs, ys) , merge([](), xs) -> xs , ifmerge(tt(), x, y, xs, ys) -> cons(x, merge(xs, cons(y, ys))) , ifmerge(ff(), x, y, xs, ys) -> cons(y, merge(cons(x, xs), ys)) , mergesort(xs) -> mergesort1(split(xs)) , mergesort1(app(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { split^#(cons(x, cons(y, xs))) -> c_6(split1^#(x, y, split(xs)), split^#(xs)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { leq^#(s(x), s(y)) -> c_1(leq^#(x, y)) , split^#(cons(x, cons(y, xs))) -> c_2(split^#(xs)) , merge^#(cons(x, xs), cons(y, ys)) -> c_3(ifmerge^#(leq(x, y), x, y, xs, ys), leq^#(x, y)) , ifmerge^#(tt(), x, y, xs, ys) -> c_4(merge^#(xs, cons(y, ys))) , ifmerge^#(ff(), x, y, xs, ys) -> c_5(merge^#(cons(x, xs), ys)) , mergesort^#(xs) -> c_6(mergesort1^#(split(xs)), split^#(xs)) , mergesort1^#(app(xs, ys)) -> c_7(merge^#(mergesort(xs), mergesort(ys)), mergesort^#(xs), mergesort^#(ys)) } Weak Trs: { leq(0(), x) -> tt() , leq(s(x), 0()) -> ff() , leq(s(x), s(y)) -> leq(x, y) , split(nil()) -> app(nil(), nil()) , split(cons(x, nil())) -> app(cons(x, nil()), nil()) , split(cons(x, cons(y, xs))) -> split1(x, y, split(xs)) , split1(x, y, app(xs, ys)) -> app(cons(x, xs), cons(y, ys)) , merge(xs, []()) -> xs , merge(cons(x, xs), cons(y, ys)) -> ifmerge(leq(x, y), x, y, xs, ys) , merge([](), xs) -> xs , ifmerge(tt(), x, y, xs, ys) -> cons(x, merge(xs, cons(y, ys))) , ifmerge(ff(), x, y, xs, ys) -> cons(y, merge(cons(x, xs), ys)) , mergesort(xs) -> mergesort1(split(xs)) , mergesort1(app(xs, ys)) -> merge(mergesort(xs), mergesort(ys)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrices' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrix interpretation of dimension 4' failed due to the following reason: Following exception was raised: stack overflow 2) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 3) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 4) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 5) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 6) 'matrix interpretation of dimension 1' failed due to the following reason: The input cannot be shown compatible 2) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. Arrrr..