MAYBE 424.05/297.10 MAYBE 424.05/297.10 424.05/297.10 We are left with following problem, upon which TcT provides the 424.05/297.10 certificate MAYBE. 424.05/297.10 424.05/297.10 Strict Trs: 424.05/297.10 { mergesort(Nil()) -> Nil() 424.05/297.10 , mergesort(Cons(x, Nil())) -> Cons(x, Nil()) 424.05/297.10 , mergesort(Cons(x', Cons(x, xs))) -> 424.05/297.10 splitmerge(Cons(x', Cons(x, xs)), Nil(), Nil()) 424.05/297.10 , merge(Nil(), xs2) -> xs2 424.05/297.10 , merge(Cons(x, xs), Nil()) -> Cons(x, xs) 424.05/297.10 , merge(Cons(x', xs'), Cons(x, xs)) -> 424.05/297.10 merge[Ite][True][Ite][True][Ite](<=(x', x), 424.05/297.10 Cons(x', xs'), 424.05/297.10 Cons(x, xs)) 424.05/297.10 , splitmerge(Nil(), xs1, xs2) -> 424.05/297.10 merge(mergesort(xs1), mergesort(xs2)) 424.05/297.10 , splitmerge(Cons(x, xs), xs1, xs2) -> 424.05/297.10 splitmerge(xs, Cons(x, xs2), xs1) 424.05/297.10 , notEmpty(Nil()) -> False() 424.05/297.10 , notEmpty(Cons(x, xs)) -> True() 424.05/297.10 , goal(xs) -> mergesort(xs) } 424.05/297.10 Weak Trs: 424.05/297.10 { <=(S(x), S(y)) -> <=(x, y) 424.05/297.10 , <=(S(x), 0()) -> False() 424.05/297.10 , <=(0(), y) -> True() } 424.05/297.10 Obligation: 424.05/297.10 innermost runtime complexity 424.05/297.10 Answer: 424.05/297.10 MAYBE 424.05/297.10 424.05/297.10 None of the processors succeeded. 424.05/297.10 424.05/297.10 Details of failed attempt(s): 424.05/297.11 ----------------------------- 424.05/297.11 1) 'empty' failed due to the following reason: 424.05/297.11 424.05/297.11 Empty strict component of the problem is NOT empty. 424.05/297.11 424.05/297.11 2) 'Best' failed due to the following reason: 424.05/297.11 424.05/297.11 None of the processors succeeded. 424.05/297.11 424.05/297.11 Details of failed attempt(s): 424.05/297.11 ----------------------------- 424.05/297.11 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 424.05/297.11 following reason: 424.05/297.11 424.05/297.11 Computation stopped due to timeout after 297.0 seconds. 424.05/297.11 424.05/297.11 2) 'Best' failed due to the following reason: 424.05/297.11 424.05/297.11 None of the processors succeeded. 424.05/297.11 424.05/297.11 Details of failed attempt(s): 424.05/297.11 ----------------------------- 424.05/297.11 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 424.05/297.11 seconds)' failed due to the following reason: 424.05/297.11 424.05/297.11 The weightgap principle applies (using the following nonconstant 424.05/297.11 growth matrix-interpretation) 424.05/297.11 424.05/297.11 The following argument positions are usable: 424.05/297.11 Uargs(merge[Ite][True][Ite][True][Ite]) = {1}, 424.05/297.11 Uargs(merge) = {1, 2} 424.05/297.11 424.05/297.11 TcT has computed the following matrix interpretation satisfying 424.05/297.11 not(EDA) and not(IDA(1)). 424.05/297.11 424.05/297.11 [True] = [0] 424.05/297.11 424.05/297.11 [mergesort](x1) = [0] 424.05/297.11 424.05/297.11 [merge[Ite][True][Ite][True][Ite]](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] 424.05/297.11 424.05/297.11 [Nil] = [0] 424.05/297.11 424.05/297.11 [merge](x1, x2) = [1] x1 + [1] x2 + [0] 424.05/297.11 424.05/297.11 [<=](x1, x2) = [5] 424.05/297.11 424.05/297.11 [splitmerge](x1, x2, x3) = [0] 424.05/297.11 424.05/297.11 [S](x1) = [1] x1 + [7] 424.05/297.11 424.05/297.11 [Cons](x1, x2) = [0] 424.05/297.11 424.05/297.11 [0] = [7] 424.05/297.11 424.05/297.11 [notEmpty](x1) = [1] 424.05/297.11 424.05/297.11 [goal](x1) = [1] x1 + [7] 424.05/297.11 424.05/297.11 [False] = [0] 424.05/297.11 424.05/297.11 The order satisfies the following ordering constraints: 424.05/297.11 424.05/297.11 [mergesort(Nil())] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [Nil()] 424.05/297.11 424.05/297.11 [mergesort(Cons(x, Nil()))] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [Cons(x, Nil())] 424.05/297.11 424.05/297.11 [mergesort(Cons(x', Cons(x, xs)))] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [splitmerge(Cons(x', Cons(x, xs)), Nil(), Nil())] 424.05/297.11 424.05/297.11 [merge(Nil(), xs2)] = [1] xs2 + [0] 424.05/297.11 >= [1] xs2 + [0] 424.05/297.11 = [xs2] 424.05/297.11 424.05/297.11 [merge(Cons(x, xs), Nil())] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [Cons(x, xs)] 424.05/297.11 424.05/297.11 [merge(Cons(x', xs'), Cons(x, xs))] = [0] 424.05/297.11 ? [7] 424.05/297.11 = [merge[Ite][True][Ite][True][Ite](<=(x', x), 424.05/297.11 Cons(x', xs'), 424.05/297.11 Cons(x, xs))] 424.05/297.11 424.05/297.11 [<=(S(x), S(y))] = [5] 424.05/297.11 >= [5] 424.05/297.11 = [<=(x, y)] 424.05/297.11 424.05/297.11 [<=(S(x), 0())] = [5] 424.05/297.11 > [0] 424.05/297.11 = [False()] 424.05/297.11 424.05/297.11 [<=(0(), y)] = [5] 424.05/297.11 > [0] 424.05/297.11 = [True()] 424.05/297.11 424.05/297.11 [splitmerge(Nil(), xs1, xs2)] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [merge(mergesort(xs1), mergesort(xs2))] 424.05/297.11 424.05/297.11 [splitmerge(Cons(x, xs), xs1, xs2)] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [splitmerge(xs, Cons(x, xs2), xs1)] 424.05/297.11 424.05/297.11 [notEmpty(Nil())] = [1] 424.05/297.11 > [0] 424.05/297.11 = [False()] 424.05/297.11 424.05/297.11 [notEmpty(Cons(x, xs))] = [1] 424.05/297.11 > [0] 424.05/297.11 = [True()] 424.05/297.11 424.05/297.11 [goal(xs)] = [1] xs + [7] 424.05/297.11 > [0] 424.05/297.11 = [mergesort(xs)] 424.05/297.11 424.05/297.11 424.05/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 424.05/297.11 424.05/297.11 We are left with following problem, upon which TcT provides the 424.05/297.11 certificate MAYBE. 424.05/297.11 424.05/297.11 Strict Trs: 424.05/297.11 { mergesort(Nil()) -> Nil() 424.05/297.11 , mergesort(Cons(x, Nil())) -> Cons(x, Nil()) 424.05/297.11 , mergesort(Cons(x', Cons(x, xs))) -> 424.05/297.11 splitmerge(Cons(x', Cons(x, xs)), Nil(), Nil()) 424.05/297.11 , merge(Nil(), xs2) -> xs2 424.05/297.11 , merge(Cons(x, xs), Nil()) -> Cons(x, xs) 424.05/297.11 , merge(Cons(x', xs'), Cons(x, xs)) -> 424.05/297.11 merge[Ite][True][Ite][True][Ite](<=(x', x), 424.05/297.11 Cons(x', xs'), 424.05/297.11 Cons(x, xs)) 424.05/297.11 , splitmerge(Nil(), xs1, xs2) -> 424.05/297.11 merge(mergesort(xs1), mergesort(xs2)) 424.05/297.11 , splitmerge(Cons(x, xs), xs1, xs2) -> 424.05/297.11 splitmerge(xs, Cons(x, xs2), xs1) } 424.05/297.11 Weak Trs: 424.05/297.11 { <=(S(x), S(y)) -> <=(x, y) 424.05/297.11 , <=(S(x), 0()) -> False() 424.05/297.11 , <=(0(), y) -> True() 424.05/297.11 , notEmpty(Nil()) -> False() 424.05/297.11 , notEmpty(Cons(x, xs)) -> True() 424.05/297.11 , goal(xs) -> mergesort(xs) } 424.05/297.11 Obligation: 424.05/297.11 innermost runtime complexity 424.05/297.11 Answer: 424.05/297.11 MAYBE 424.05/297.11 424.05/297.11 The weightgap principle applies (using the following nonconstant 424.05/297.11 growth matrix-interpretation) 424.05/297.11 424.05/297.11 The following argument positions are usable: 424.05/297.11 Uargs(merge[Ite][True][Ite][True][Ite]) = {1}, 424.05/297.11 Uargs(merge) = {1, 2} 424.05/297.11 424.05/297.11 TcT has computed the following matrix interpretation satisfying 424.05/297.11 not(EDA) and not(IDA(1)). 424.05/297.11 424.05/297.11 [True] = [0] 424.05/297.11 424.05/297.11 [mergesort](x1) = [0] 424.05/297.11 424.05/297.11 [merge[Ite][True][Ite][True][Ite]](x1, x2, x3) = [1] x1 + [3] 424.05/297.11 424.05/297.11 [Nil] = [1] 424.05/297.11 424.05/297.11 [merge](x1, x2) = [1] x1 + [1] x2 + [0] 424.05/297.11 424.05/297.11 [<=](x1, x2) = [0] 424.05/297.11 424.05/297.11 [splitmerge](x1, x2, x3) = [0] 424.05/297.11 424.05/297.11 [S](x1) = [1] x1 + [7] 424.05/297.11 424.05/297.11 [Cons](x1, x2) = [0] 424.05/297.11 424.05/297.11 [0] = [7] 424.05/297.11 424.05/297.11 [notEmpty](x1) = [1] x1 + [3] 424.05/297.11 424.05/297.11 [goal](x1) = [1] x1 + [7] 424.05/297.11 424.05/297.11 [False] = [0] 424.05/297.11 424.05/297.11 The order satisfies the following ordering constraints: 424.05/297.11 424.05/297.11 [mergesort(Nil())] = [0] 424.05/297.11 ? [1] 424.05/297.11 = [Nil()] 424.05/297.11 424.05/297.11 [mergesort(Cons(x, Nil()))] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [Cons(x, Nil())] 424.05/297.11 424.05/297.11 [mergesort(Cons(x', Cons(x, xs)))] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [splitmerge(Cons(x', Cons(x, xs)), Nil(), Nil())] 424.05/297.11 424.05/297.11 [merge(Nil(), xs2)] = [1] xs2 + [1] 424.05/297.11 > [1] xs2 + [0] 424.05/297.11 = [xs2] 424.05/297.11 424.05/297.11 [merge(Cons(x, xs), Nil())] = [1] 424.05/297.11 > [0] 424.05/297.11 = [Cons(x, xs)] 424.05/297.11 424.05/297.11 [merge(Cons(x', xs'), Cons(x, xs))] = [0] 424.05/297.11 ? [3] 424.05/297.11 = [merge[Ite][True][Ite][True][Ite](<=(x', x), 424.05/297.11 Cons(x', xs'), 424.05/297.11 Cons(x, xs))] 424.05/297.11 424.05/297.11 [<=(S(x), S(y))] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [<=(x, y)] 424.05/297.11 424.05/297.11 [<=(S(x), 0())] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [False()] 424.05/297.11 424.05/297.11 [<=(0(), y)] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [True()] 424.05/297.11 424.05/297.11 [splitmerge(Nil(), xs1, xs2)] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [merge(mergesort(xs1), mergesort(xs2))] 424.05/297.11 424.05/297.11 [splitmerge(Cons(x, xs), xs1, xs2)] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [splitmerge(xs, Cons(x, xs2), xs1)] 424.05/297.11 424.05/297.11 [notEmpty(Nil())] = [4] 424.05/297.11 > [0] 424.05/297.11 = [False()] 424.05/297.11 424.05/297.11 [notEmpty(Cons(x, xs))] = [3] 424.05/297.11 > [0] 424.05/297.11 = [True()] 424.05/297.11 424.05/297.11 [goal(xs)] = [1] xs + [7] 424.05/297.11 > [0] 424.05/297.11 = [mergesort(xs)] 424.05/297.11 424.05/297.11 424.05/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 424.05/297.11 424.05/297.11 We are left with following problem, upon which TcT provides the 424.05/297.11 certificate MAYBE. 424.05/297.11 424.05/297.11 Strict Trs: 424.05/297.11 { mergesort(Nil()) -> Nil() 424.05/297.11 , mergesort(Cons(x, Nil())) -> Cons(x, Nil()) 424.05/297.11 , mergesort(Cons(x', Cons(x, xs))) -> 424.05/297.11 splitmerge(Cons(x', Cons(x, xs)), Nil(), Nil()) 424.05/297.11 , merge(Cons(x', xs'), Cons(x, xs)) -> 424.05/297.11 merge[Ite][True][Ite][True][Ite](<=(x', x), 424.05/297.11 Cons(x', xs'), 424.05/297.11 Cons(x, xs)) 424.05/297.11 , splitmerge(Nil(), xs1, xs2) -> 424.05/297.11 merge(mergesort(xs1), mergesort(xs2)) 424.05/297.11 , splitmerge(Cons(x, xs), xs1, xs2) -> 424.05/297.11 splitmerge(xs, Cons(x, xs2), xs1) } 424.05/297.11 Weak Trs: 424.05/297.11 { merge(Nil(), xs2) -> xs2 424.05/297.11 , merge(Cons(x, xs), Nil()) -> Cons(x, xs) 424.05/297.11 , <=(S(x), S(y)) -> <=(x, y) 424.05/297.11 , <=(S(x), 0()) -> False() 424.05/297.11 , <=(0(), y) -> True() 424.05/297.11 , notEmpty(Nil()) -> False() 424.05/297.11 , notEmpty(Cons(x, xs)) -> True() 424.05/297.11 , goal(xs) -> mergesort(xs) } 424.05/297.11 Obligation: 424.05/297.11 innermost runtime complexity 424.05/297.11 Answer: 424.05/297.11 MAYBE 424.05/297.11 424.05/297.11 The weightgap principle applies (using the following nonconstant 424.05/297.11 growth matrix-interpretation) 424.05/297.11 424.05/297.11 The following argument positions are usable: 424.05/297.11 Uargs(merge[Ite][True][Ite][True][Ite]) = {1}, 424.05/297.11 Uargs(merge) = {1, 2} 424.05/297.11 424.05/297.11 TcT has computed the following matrix interpretation satisfying 424.05/297.11 not(EDA) and not(IDA(1)). 424.05/297.11 424.05/297.11 [True] = [1] 424.05/297.11 424.05/297.11 [mergesort](x1) = [0] 424.05/297.11 424.05/297.11 [merge[Ite][True][Ite][True][Ite]](x1, x2, x3) = [1] x1 + [2] 424.05/297.11 424.05/297.11 [Nil] = [4] 424.05/297.11 424.05/297.11 [merge](x1, x2) = [1] x1 + [1] x2 + [0] 424.05/297.11 424.05/297.11 [<=](x1, x2) = [5] 424.05/297.11 424.05/297.11 [splitmerge](x1, x2, x3) = [0] 424.05/297.11 424.05/297.11 [S](x1) = [1] x1 + [7] 424.05/297.11 424.05/297.11 [Cons](x1, x2) = [4] 424.05/297.11 424.05/297.11 [0] = [7] 424.05/297.11 424.05/297.11 [notEmpty](x1) = [1] x1 + [7] 424.05/297.11 424.05/297.11 [goal](x1) = [1] x1 + [7] 424.05/297.11 424.05/297.11 [False] = [1] 424.05/297.11 424.05/297.11 The order satisfies the following ordering constraints: 424.05/297.11 424.05/297.11 [mergesort(Nil())] = [0] 424.05/297.11 ? [4] 424.05/297.11 = [Nil()] 424.05/297.11 424.05/297.11 [mergesort(Cons(x, Nil()))] = [0] 424.05/297.11 ? [4] 424.05/297.11 = [Cons(x, Nil())] 424.05/297.11 424.05/297.11 [mergesort(Cons(x', Cons(x, xs)))] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [splitmerge(Cons(x', Cons(x, xs)), Nil(), Nil())] 424.05/297.11 424.05/297.11 [merge(Nil(), xs2)] = [1] xs2 + [4] 424.05/297.11 > [1] xs2 + [0] 424.05/297.11 = [xs2] 424.05/297.11 424.05/297.11 [merge(Cons(x, xs), Nil())] = [8] 424.05/297.11 > [4] 424.05/297.11 = [Cons(x, xs)] 424.05/297.11 424.05/297.11 [merge(Cons(x', xs'), Cons(x, xs))] = [8] 424.05/297.11 > [7] 424.05/297.11 = [merge[Ite][True][Ite][True][Ite](<=(x', x), 424.05/297.11 Cons(x', xs'), 424.05/297.11 Cons(x, xs))] 424.05/297.11 424.05/297.11 [<=(S(x), S(y))] = [5] 424.05/297.11 >= [5] 424.05/297.11 = [<=(x, y)] 424.05/297.11 424.05/297.11 [<=(S(x), 0())] = [5] 424.05/297.11 > [1] 424.05/297.11 = [False()] 424.05/297.11 424.05/297.11 [<=(0(), y)] = [5] 424.05/297.11 > [1] 424.05/297.11 = [True()] 424.05/297.11 424.05/297.11 [splitmerge(Nil(), xs1, xs2)] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [merge(mergesort(xs1), mergesort(xs2))] 424.05/297.11 424.05/297.11 [splitmerge(Cons(x, xs), xs1, xs2)] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [splitmerge(xs, Cons(x, xs2), xs1)] 424.05/297.11 424.05/297.11 [notEmpty(Nil())] = [11] 424.05/297.11 > [1] 424.05/297.11 = [False()] 424.05/297.11 424.05/297.11 [notEmpty(Cons(x, xs))] = [11] 424.05/297.11 > [1] 424.05/297.11 = [True()] 424.05/297.11 424.05/297.11 [goal(xs)] = [1] xs + [7] 424.05/297.11 > [0] 424.05/297.11 = [mergesort(xs)] 424.05/297.11 424.05/297.11 424.05/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 424.05/297.11 424.05/297.11 We are left with following problem, upon which TcT provides the 424.05/297.11 certificate MAYBE. 424.05/297.11 424.05/297.11 Strict Trs: 424.05/297.11 { mergesort(Nil()) -> Nil() 424.05/297.11 , mergesort(Cons(x, Nil())) -> Cons(x, Nil()) 424.05/297.11 , mergesort(Cons(x', Cons(x, xs))) -> 424.05/297.11 splitmerge(Cons(x', Cons(x, xs)), Nil(), Nil()) 424.05/297.11 , splitmerge(Nil(), xs1, xs2) -> 424.05/297.11 merge(mergesort(xs1), mergesort(xs2)) 424.05/297.11 , splitmerge(Cons(x, xs), xs1, xs2) -> 424.05/297.11 splitmerge(xs, Cons(x, xs2), xs1) } 424.05/297.11 Weak Trs: 424.05/297.11 { merge(Nil(), xs2) -> xs2 424.05/297.11 , merge(Cons(x, xs), Nil()) -> Cons(x, xs) 424.05/297.11 , merge(Cons(x', xs'), Cons(x, xs)) -> 424.05/297.11 merge[Ite][True][Ite][True][Ite](<=(x', x), 424.05/297.11 Cons(x', xs'), 424.05/297.11 Cons(x, xs)) 424.05/297.11 , <=(S(x), S(y)) -> <=(x, y) 424.05/297.11 , <=(S(x), 0()) -> False() 424.05/297.11 , <=(0(), y) -> True() 424.05/297.11 , notEmpty(Nil()) -> False() 424.05/297.11 , notEmpty(Cons(x, xs)) -> True() 424.05/297.11 , goal(xs) -> mergesort(xs) } 424.05/297.11 Obligation: 424.05/297.11 innermost runtime complexity 424.05/297.11 Answer: 424.05/297.11 MAYBE 424.05/297.11 424.05/297.11 The weightgap principle applies (using the following nonconstant 424.05/297.11 growth matrix-interpretation) 424.05/297.11 424.05/297.11 The following argument positions are usable: 424.05/297.11 Uargs(merge[Ite][True][Ite][True][Ite]) = {1}, 424.05/297.11 Uargs(merge) = {1, 2} 424.05/297.11 424.05/297.11 TcT has computed the following matrix interpretation satisfying 424.05/297.11 not(EDA) and not(IDA(1)). 424.05/297.11 424.05/297.11 [True] = [0] 424.05/297.11 424.05/297.11 [mergesort](x1) = [1] 424.05/297.11 424.05/297.11 [merge[Ite][True][Ite][True][Ite]](x1, x2, x3) = [1] x1 + [3] 424.05/297.11 424.05/297.11 [Nil] = [0] 424.05/297.11 424.05/297.11 [merge](x1, x2) = [1] x1 + [1] x2 + [6] 424.05/297.11 424.05/297.11 [<=](x1, x2) = [0] 424.05/297.11 424.05/297.11 [splitmerge](x1, x2, x3) = [0] 424.05/297.11 424.05/297.11 [S](x1) = [1] x1 + [7] 424.05/297.11 424.05/297.11 [Cons](x1, x2) = [0] 424.05/297.11 424.05/297.11 [0] = [7] 424.05/297.11 424.05/297.11 [notEmpty](x1) = [1] x1 + [7] 424.05/297.11 424.05/297.11 [goal](x1) = [1] x1 + [7] 424.05/297.11 424.05/297.11 [False] = [0] 424.05/297.11 424.05/297.11 The order satisfies the following ordering constraints: 424.05/297.11 424.05/297.11 [mergesort(Nil())] = [1] 424.05/297.11 > [0] 424.05/297.11 = [Nil()] 424.05/297.11 424.05/297.11 [mergesort(Cons(x, Nil()))] = [1] 424.05/297.11 > [0] 424.05/297.11 = [Cons(x, Nil())] 424.05/297.11 424.05/297.11 [mergesort(Cons(x', Cons(x, xs)))] = [1] 424.05/297.11 > [0] 424.05/297.11 = [splitmerge(Cons(x', Cons(x, xs)), Nil(), Nil())] 424.05/297.11 424.05/297.11 [merge(Nil(), xs2)] = [1] xs2 + [6] 424.05/297.11 > [1] xs2 + [0] 424.05/297.11 = [xs2] 424.05/297.11 424.05/297.11 [merge(Cons(x, xs), Nil())] = [6] 424.05/297.11 > [0] 424.05/297.11 = [Cons(x, xs)] 424.05/297.11 424.05/297.11 [merge(Cons(x', xs'), Cons(x, xs))] = [6] 424.05/297.11 > [3] 424.05/297.11 = [merge[Ite][True][Ite][True][Ite](<=(x', x), 424.05/297.11 Cons(x', xs'), 424.05/297.11 Cons(x, xs))] 424.05/297.11 424.05/297.11 [<=(S(x), S(y))] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [<=(x, y)] 424.05/297.11 424.05/297.11 [<=(S(x), 0())] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [False()] 424.05/297.11 424.05/297.11 [<=(0(), y)] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [True()] 424.05/297.11 424.05/297.11 [splitmerge(Nil(), xs1, xs2)] = [0] 424.05/297.11 ? [8] 424.05/297.11 = [merge(mergesort(xs1), mergesort(xs2))] 424.05/297.11 424.05/297.11 [splitmerge(Cons(x, xs), xs1, xs2)] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [splitmerge(xs, Cons(x, xs2), xs1)] 424.05/297.11 424.05/297.11 [notEmpty(Nil())] = [7] 424.05/297.11 > [0] 424.05/297.11 = [False()] 424.05/297.11 424.05/297.11 [notEmpty(Cons(x, xs))] = [7] 424.05/297.11 > [0] 424.05/297.11 = [True()] 424.05/297.11 424.05/297.11 [goal(xs)] = [1] xs + [7] 424.05/297.11 > [1] 424.05/297.11 = [mergesort(xs)] 424.05/297.11 424.05/297.11 424.05/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 424.05/297.11 424.05/297.11 We are left with following problem, upon which TcT provides the 424.05/297.11 certificate MAYBE. 424.05/297.11 424.05/297.11 Strict Trs: 424.05/297.11 { splitmerge(Nil(), xs1, xs2) -> 424.05/297.11 merge(mergesort(xs1), mergesort(xs2)) 424.05/297.11 , splitmerge(Cons(x, xs), xs1, xs2) -> 424.05/297.11 splitmerge(xs, Cons(x, xs2), xs1) } 424.05/297.11 Weak Trs: 424.05/297.11 { mergesort(Nil()) -> Nil() 424.05/297.11 , mergesort(Cons(x, Nil())) -> Cons(x, Nil()) 424.05/297.11 , mergesort(Cons(x', Cons(x, xs))) -> 424.05/297.11 splitmerge(Cons(x', Cons(x, xs)), Nil(), Nil()) 424.05/297.11 , merge(Nil(), xs2) -> xs2 424.05/297.11 , merge(Cons(x, xs), Nil()) -> Cons(x, xs) 424.05/297.11 , merge(Cons(x', xs'), Cons(x, xs)) -> 424.05/297.11 merge[Ite][True][Ite][True][Ite](<=(x', x), 424.05/297.11 Cons(x', xs'), 424.05/297.11 Cons(x, xs)) 424.05/297.11 , <=(S(x), S(y)) -> <=(x, y) 424.05/297.11 , <=(S(x), 0()) -> False() 424.05/297.11 , <=(0(), y) -> True() 424.05/297.11 , notEmpty(Nil()) -> False() 424.05/297.11 , notEmpty(Cons(x, xs)) -> True() 424.05/297.11 , goal(xs) -> mergesort(xs) } 424.05/297.11 Obligation: 424.05/297.11 innermost runtime complexity 424.05/297.11 Answer: 424.05/297.11 MAYBE 424.05/297.11 424.05/297.11 The weightgap principle applies (using the following nonconstant 424.05/297.11 growth matrix-interpretation) 424.05/297.11 424.05/297.11 The following argument positions are usable: 424.05/297.11 Uargs(merge[Ite][True][Ite][True][Ite]) = {1}, 424.05/297.11 Uargs(merge) = {1, 2} 424.05/297.11 424.05/297.11 TcT has computed the following matrix interpretation satisfying 424.05/297.11 not(EDA) and not(IDA(1)). 424.05/297.11 424.05/297.11 [True] = [0] 424.05/297.11 424.05/297.11 [mergesort](x1) = [1] x1 + [0] 424.05/297.11 424.05/297.11 [merge[Ite][True][Ite][True][Ite]](x1, x2, x3) = [1] x1 + [3] 424.05/297.11 424.05/297.11 [Nil] = [1] 424.05/297.11 424.05/297.11 [merge](x1, x2) = [1] x1 + [1] x2 + [0] 424.05/297.11 424.05/297.11 [<=](x1, x2) = [0] 424.05/297.11 424.05/297.11 [splitmerge](x1, x2, x3) = [1] x2 + [1] x3 + [1] 424.05/297.11 424.05/297.11 [S](x1) = [1] x1 + [7] 424.05/297.11 424.05/297.11 [Cons](x1, x2) = [1] x2 + [7] 424.05/297.11 424.05/297.11 [0] = [7] 424.05/297.11 424.05/297.11 [notEmpty](x1) = [1] x1 + [3] 424.05/297.11 424.05/297.11 [goal](x1) = [1] x1 + [7] 424.05/297.11 424.05/297.11 [False] = [0] 424.05/297.11 424.05/297.11 The order satisfies the following ordering constraints: 424.05/297.11 424.05/297.11 [mergesort(Nil())] = [1] 424.05/297.11 >= [1] 424.05/297.11 = [Nil()] 424.05/297.11 424.05/297.11 [mergesort(Cons(x, Nil()))] = [8] 424.05/297.11 >= [8] 424.05/297.11 = [Cons(x, Nil())] 424.05/297.11 424.05/297.11 [mergesort(Cons(x', Cons(x, xs)))] = [1] xs + [14] 424.05/297.11 > [3] 424.05/297.11 = [splitmerge(Cons(x', Cons(x, xs)), Nil(), Nil())] 424.05/297.11 424.05/297.11 [merge(Nil(), xs2)] = [1] xs2 + [1] 424.05/297.11 > [1] xs2 + [0] 424.05/297.11 = [xs2] 424.05/297.11 424.05/297.11 [merge(Cons(x, xs), Nil())] = [1] xs + [8] 424.05/297.11 > [1] xs + [7] 424.05/297.11 = [Cons(x, xs)] 424.05/297.11 424.05/297.11 [merge(Cons(x', xs'), Cons(x, xs))] = [1] xs + [1] xs' + [14] 424.05/297.11 > [3] 424.05/297.11 = [merge[Ite][True][Ite][True][Ite](<=(x', x), 424.05/297.11 Cons(x', xs'), 424.05/297.11 Cons(x, xs))] 424.05/297.11 424.05/297.11 [<=(S(x), S(y))] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [<=(x, y)] 424.05/297.11 424.05/297.11 [<=(S(x), 0())] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [False()] 424.05/297.11 424.05/297.11 [<=(0(), y)] = [0] 424.05/297.11 >= [0] 424.05/297.11 = [True()] 424.05/297.11 424.05/297.11 [splitmerge(Nil(), xs1, xs2)] = [1] xs1 + [1] xs2 + [1] 424.05/297.11 > [1] xs1 + [1] xs2 + [0] 424.05/297.11 = [merge(mergesort(xs1), mergesort(xs2))] 424.05/297.11 424.05/297.11 [splitmerge(Cons(x, xs), xs1, xs2)] = [1] xs1 + [1] xs2 + [1] 424.05/297.11 ? [1] xs1 + [1] xs2 + [8] 424.05/297.11 = [splitmerge(xs, Cons(x, xs2), xs1)] 424.05/297.11 424.05/297.11 [notEmpty(Nil())] = [4] 424.05/297.11 > [0] 424.05/297.11 = [False()] 424.05/297.11 424.05/297.11 [notEmpty(Cons(x, xs))] = [1] xs + [10] 424.05/297.11 > [0] 424.05/297.11 = [True()] 424.05/297.12 424.05/297.12 [goal(xs)] = [1] xs + [7] 424.05/297.12 > [1] xs + [0] 424.05/297.12 = [mergesort(xs)] 424.05/297.12 424.05/297.12 424.05/297.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 424.05/297.12 424.05/297.12 We are left with following problem, upon which TcT provides the 424.05/297.12 certificate MAYBE. 424.05/297.12 424.05/297.12 Strict Trs: 424.05/297.12 { splitmerge(Cons(x, xs), xs1, xs2) -> 424.05/297.12 splitmerge(xs, Cons(x, xs2), xs1) } 424.05/297.12 Weak Trs: 424.05/297.12 { mergesort(Nil()) -> Nil() 424.05/297.12 , mergesort(Cons(x, Nil())) -> Cons(x, Nil()) 424.05/297.12 , mergesort(Cons(x', Cons(x, xs))) -> 424.05/297.12 splitmerge(Cons(x', Cons(x, xs)), Nil(), Nil()) 424.05/297.12 , merge(Nil(), xs2) -> xs2 424.05/297.12 , merge(Cons(x, xs), Nil()) -> Cons(x, xs) 424.05/297.12 , merge(Cons(x', xs'), Cons(x, xs)) -> 424.05/297.12 merge[Ite][True][Ite][True][Ite](<=(x', x), 424.05/297.12 Cons(x', xs'), 424.05/297.12 Cons(x, xs)) 424.05/297.12 , <=(S(x), S(y)) -> <=(x, y) 424.05/297.12 , <=(S(x), 0()) -> False() 424.05/297.12 , <=(0(), y) -> True() 424.05/297.12 , splitmerge(Nil(), xs1, xs2) -> 424.05/297.12 merge(mergesort(xs1), mergesort(xs2)) 424.05/297.12 , notEmpty(Nil()) -> False() 424.05/297.12 , notEmpty(Cons(x, xs)) -> True() 424.05/297.12 , goal(xs) -> mergesort(xs) } 424.05/297.12 Obligation: 424.05/297.12 innermost runtime complexity 424.05/297.12 Answer: 424.05/297.12 MAYBE 424.05/297.12 424.05/297.12 None of the processors succeeded. 424.05/297.12 424.05/297.12 Details of failed attempt(s): 424.05/297.12 ----------------------------- 424.05/297.12 1) 'empty' failed due to the following reason: 424.05/297.12 424.05/297.12 Empty strict component of the problem is NOT empty. 424.05/297.12 424.05/297.12 2) 'With Problem ...' failed due to the following reason: 424.05/297.12 424.05/297.12 None of the processors succeeded. 424.05/297.12 424.05/297.12 Details of failed attempt(s): 424.05/297.12 ----------------------------- 424.05/297.12 1) 'empty' failed due to the following reason: 424.05/297.12 424.05/297.12 Empty strict component of the problem is NOT empty. 424.05/297.12 424.05/297.12 2) 'Fastest' failed due to the following reason: 424.05/297.12 424.05/297.12 None of the processors succeeded. 424.05/297.12 424.05/297.12 Details of failed attempt(s): 424.05/297.12 ----------------------------- 424.05/297.12 1) 'With Problem ...' failed due to the following reason: 424.05/297.12 424.05/297.12 None of the processors succeeded. 424.05/297.12 424.05/297.12 Details of failed attempt(s): 424.05/297.12 ----------------------------- 424.05/297.12 1) 'empty' failed due to the following reason: 424.05/297.12 424.05/297.12 Empty strict component of the problem is NOT empty. 424.05/297.12 424.05/297.12 2) 'With Problem ...' failed due to the following reason: 424.05/297.12 424.05/297.12 None of the processors succeeded. 424.05/297.12 424.05/297.12 Details of failed attempt(s): 424.05/297.12 ----------------------------- 424.05/297.12 1) 'empty' failed due to the following reason: 424.05/297.12 424.05/297.12 Empty strict component of the problem is NOT empty. 424.05/297.12 424.05/297.12 2) 'With Problem ...' failed due to the following reason: 424.05/297.12 424.05/297.12 None of the processors succeeded. 424.05/297.12 424.05/297.12 Details of failed attempt(s): 424.05/297.12 ----------------------------- 424.05/297.12 1) 'empty' failed due to the following reason: 424.05/297.12 424.05/297.12 Empty strict component of the problem is NOT empty. 424.05/297.12 424.05/297.12 2) 'With Problem ...' failed due to the following reason: 424.05/297.12 424.05/297.12 Empty strict component of the problem is NOT empty. 424.05/297.12 424.05/297.12 424.05/297.12 424.05/297.12 424.05/297.12 2) 'With Problem ...' failed due to the following reason: 424.05/297.12 424.05/297.12 None of the processors succeeded. 424.05/297.12 424.05/297.12 Details of failed attempt(s): 424.05/297.12 ----------------------------- 424.05/297.12 1) 'empty' failed due to the following reason: 424.05/297.12 424.05/297.12 Empty strict component of the problem is NOT empty. 424.05/297.12 424.05/297.12 2) 'With Problem ...' failed due to the following reason: 424.05/297.12 424.05/297.12 Empty strict component of the problem is NOT empty. 424.05/297.12 424.05/297.12 424.05/297.12 424.05/297.12 424.05/297.12 424.05/297.12 2) 'Best' failed due to the following reason: 424.05/297.12 424.05/297.12 None of the processors succeeded. 424.05/297.12 424.05/297.12 Details of failed attempt(s): 424.05/297.12 ----------------------------- 424.05/297.12 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 424.05/297.12 following reason: 424.05/297.12 424.05/297.12 The input cannot be shown compatible 424.05/297.12 424.05/297.12 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 424.05/297.12 to the following reason: 424.05/297.12 424.05/297.12 The input cannot be shown compatible 424.05/297.12 424.05/297.12 424.05/297.12 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 424.05/297.12 failed due to the following reason: 424.05/297.12 424.05/297.12 None of the processors succeeded. 424.05/297.12 424.05/297.12 Details of failed attempt(s): 424.05/297.12 ----------------------------- 424.05/297.12 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 424.05/297.12 failed due to the following reason: 424.05/297.12 424.05/297.12 match-boundness of the problem could not be verified. 424.05/297.12 424.05/297.12 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 424.05/297.12 failed due to the following reason: 424.05/297.12 424.05/297.12 match-boundness of the problem could not be verified. 424.05/297.12 424.05/297.12 424.05/297.12 424.05/297.12 424.05/297.12 424.05/297.12 Arrrr.. 424.05/297.16 EOF