MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { isEmpty(cons(x, xs)) -> false() , isEmpty(nil()) -> true() , isZero(0()) -> true() , isZero(s(x)) -> false() , head(cons(x, xs)) -> x , tail(cons(x, xs)) -> xs , tail(nil()) -> nil() , append(cons(y, ys), x) -> cons(y, append(ys, x)) , append(nil(), x) -> cons(x, nil()) , p(0()) -> 0() , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , addLists(xs, ys, zs) -> if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys))) , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) -> addLists(xs2, ys2, zs) , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) -> addLists(xs, ys, zs2) , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError() , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError() , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs , addList(xs, ys) -> addLists(xs, ys, nil()) } 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: Computation stopped due to timeout after 30.0 seconds. 2) '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) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) '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 2) '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 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { isEmpty^#(cons(x, xs)) -> c_1() , isEmpty^#(nil()) -> c_2() , isZero^#(0()) -> c_3() , isZero^#(s(x)) -> c_4() , head^#(cons(x, xs)) -> c_5(x) , tail^#(cons(x, xs)) -> c_6(xs) , tail^#(nil()) -> c_7() , append^#(cons(y, ys), x) -> c_8(y, append^#(ys, x)) , append^#(nil(), x) -> c_9(x) , p^#(0()) -> c_10() , p^#(s(0())) -> c_11() , p^#(s(s(x))) -> c_12(p^#(s(x))) , inc^#(0()) -> c_13() , inc^#(s(x)) -> c_14(inc^#(x)) , addLists^#(xs, ys, zs) -> c_15(if^#(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))) , if^#(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) -> c_16(addLists^#(xs2, ys2, zs)) , if^#(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) -> c_17(addLists^#(xs, ys, zs2)) , if^#(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_18() , if^#(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) -> c_19() , if^#(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_20(zs) , addList^#(xs, ys) -> c_21(addLists^#(xs, ys, nil())) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { isEmpty^#(cons(x, xs)) -> c_1() , isEmpty^#(nil()) -> c_2() , isZero^#(0()) -> c_3() , isZero^#(s(x)) -> c_4() , head^#(cons(x, xs)) -> c_5(x) , tail^#(cons(x, xs)) -> c_6(xs) , tail^#(nil()) -> c_7() , append^#(cons(y, ys), x) -> c_8(y, append^#(ys, x)) , append^#(nil(), x) -> c_9(x) , p^#(0()) -> c_10() , p^#(s(0())) -> c_11() , p^#(s(s(x))) -> c_12(p^#(s(x))) , inc^#(0()) -> c_13() , inc^#(s(x)) -> c_14(inc^#(x)) , addLists^#(xs, ys, zs) -> c_15(if^#(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))) , if^#(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) -> c_16(addLists^#(xs2, ys2, zs)) , if^#(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) -> c_17(addLists^#(xs, ys, zs2)) , if^#(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_18() , if^#(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) -> c_19() , if^#(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_20(zs) , addList^#(xs, ys) -> c_21(addLists^#(xs, ys, nil())) } Strict Trs: { isEmpty(cons(x, xs)) -> false() , isEmpty(nil()) -> true() , isZero(0()) -> true() , isZero(s(x)) -> false() , head(cons(x, xs)) -> x , tail(cons(x, xs)) -> xs , tail(nil()) -> nil() , append(cons(y, ys), x) -> cons(y, append(ys, x)) , append(nil(), x) -> cons(x, nil()) , p(0()) -> 0() , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , addLists(xs, ys, zs) -> if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys))) , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) -> addLists(xs2, ys2, zs) , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) -> addLists(xs, ys, zs2) , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError() , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError() , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs , addList(xs, ys) -> addLists(xs, ys, nil()) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,4,7,10,11,13,18,19} by applications of Pre({1,2,3,4,7,10,11,13,18,19}) = {5,6,8,9,12,14,15,20}. Here rules are labeled as follows: DPs: { 1: isEmpty^#(cons(x, xs)) -> c_1() , 2: isEmpty^#(nil()) -> c_2() , 3: isZero^#(0()) -> c_3() , 4: isZero^#(s(x)) -> c_4() , 5: head^#(cons(x, xs)) -> c_5(x) , 6: tail^#(cons(x, xs)) -> c_6(xs) , 7: tail^#(nil()) -> c_7() , 8: append^#(cons(y, ys), x) -> c_8(y, append^#(ys, x)) , 9: append^#(nil(), x) -> c_9(x) , 10: p^#(0()) -> c_10() , 11: p^#(s(0())) -> c_11() , 12: p^#(s(s(x))) -> c_12(p^#(s(x))) , 13: inc^#(0()) -> c_13() , 14: inc^#(s(x)) -> c_14(inc^#(x)) , 15: addLists^#(xs, ys, zs) -> c_15(if^#(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))) , 16: if^#(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) -> c_16(addLists^#(xs2, ys2, zs)) , 17: if^#(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) -> c_17(addLists^#(xs, ys, zs2)) , 18: if^#(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_18() , 19: if^#(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) -> c_19() , 20: if^#(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_20(zs) , 21: addList^#(xs, ys) -> c_21(addLists^#(xs, ys, nil())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { head^#(cons(x, xs)) -> c_5(x) , tail^#(cons(x, xs)) -> c_6(xs) , append^#(cons(y, ys), x) -> c_8(y, append^#(ys, x)) , append^#(nil(), x) -> c_9(x) , p^#(s(s(x))) -> c_12(p^#(s(x))) , inc^#(s(x)) -> c_14(inc^#(x)) , addLists^#(xs, ys, zs) -> c_15(if^#(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))) , if^#(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) -> c_16(addLists^#(xs2, ys2, zs)) , if^#(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) -> c_17(addLists^#(xs, ys, zs2)) , if^#(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_20(zs) , addList^#(xs, ys) -> c_21(addLists^#(xs, ys, nil())) } Strict Trs: { isEmpty(cons(x, xs)) -> false() , isEmpty(nil()) -> true() , isZero(0()) -> true() , isZero(s(x)) -> false() , head(cons(x, xs)) -> x , tail(cons(x, xs)) -> xs , tail(nil()) -> nil() , append(cons(y, ys), x) -> cons(y, append(ys, x)) , append(nil(), x) -> cons(x, nil()) , p(0()) -> 0() , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , addLists(xs, ys, zs) -> if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys))) , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) -> addLists(xs2, ys2, zs) , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) -> addLists(xs, ys, zs2) , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError() , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError() , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs , addList(xs, ys) -> addLists(xs, ys, nil()) } Weak DPs: { isEmpty^#(cons(x, xs)) -> c_1() , isEmpty^#(nil()) -> c_2() , isZero^#(0()) -> c_3() , isZero^#(s(x)) -> c_4() , tail^#(nil()) -> c_7() , p^#(0()) -> c_10() , p^#(s(0())) -> c_11() , inc^#(0()) -> c_13() , if^#(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_18() , if^#(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) -> c_19() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..