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() , 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)) , sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) , if(false(), false(), y, xs, ys, x) -> sumList(ys, x) , if(false(), true(), y, xs, ys, x) -> sumList(xs, y) , if(true(), b, y, xs, ys, x) -> y , sum(xs) -> sumList(xs, 0()) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: 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() , tail^#(cons(x, xs)) -> c_6() , tail^#(nil()) -> c_7() , p^#(0()) -> c_8() , p^#(s(0())) -> c_9() , p^#(s(s(x))) -> c_10(p^#(s(x))) , inc^#(0()) -> c_11() , inc^#(s(x)) -> c_12(inc^#(x)) , sumList^#(xs, y) -> c_13(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), isEmpty^#(xs), isZero^#(head(xs)), head^#(xs), tail^#(xs), p^#(head(xs)), head^#(xs), tail^#(xs), inc^#(y)) , if^#(false(), false(), y, xs, ys, x) -> c_14(sumList^#(ys, x)) , if^#(false(), true(), y, xs, ys, x) -> c_15(sumList^#(xs, y)) , if^#(true(), b, y, xs, ys, x) -> c_16() , sum^#(xs) -> c_17(sumList^#(xs, 0())) } 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() , tail^#(cons(x, xs)) -> c_6() , tail^#(nil()) -> c_7() , p^#(0()) -> c_8() , p^#(s(0())) -> c_9() , p^#(s(s(x))) -> c_10(p^#(s(x))) , inc^#(0()) -> c_11() , inc^#(s(x)) -> c_12(inc^#(x)) , sumList^#(xs, y) -> c_13(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), isEmpty^#(xs), isZero^#(head(xs)), head^#(xs), tail^#(xs), p^#(head(xs)), head^#(xs), tail^#(xs), inc^#(y)) , if^#(false(), false(), y, xs, ys, x) -> c_14(sumList^#(ys, x)) , if^#(false(), true(), y, xs, ys, x) -> c_15(sumList^#(xs, y)) , if^#(true(), b, y, xs, ys, x) -> c_16() , sum^#(xs) -> c_17(sumList^#(xs, 0())) } Weak 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() , 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)) , sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) , if(false(), false(), y, xs, ys, x) -> sumList(ys, x) , if(false(), true(), y, xs, ys, x) -> sumList(xs, y) , if(true(), b, y, xs, ys, x) -> y , sum(xs) -> sumList(xs, 0()) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,4,5,6,7,8,9,11,16} by applications of Pre({1,2,3,4,5,6,7,8,9,11,16}) = {10,12,13}. 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() , 6: tail^#(cons(x, xs)) -> c_6() , 7: tail^#(nil()) -> c_7() , 8: p^#(0()) -> c_8() , 9: p^#(s(0())) -> c_9() , 10: p^#(s(s(x))) -> c_10(p^#(s(x))) , 11: inc^#(0()) -> c_11() , 12: inc^#(s(x)) -> c_12(inc^#(x)) , 13: sumList^#(xs, y) -> c_13(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), isEmpty^#(xs), isZero^#(head(xs)), head^#(xs), tail^#(xs), p^#(head(xs)), head^#(xs), tail^#(xs), inc^#(y)) , 14: if^#(false(), false(), y, xs, ys, x) -> c_14(sumList^#(ys, x)) , 15: if^#(false(), true(), y, xs, ys, x) -> c_15(sumList^#(xs, y)) , 16: if^#(true(), b, y, xs, ys, x) -> c_16() , 17: sum^#(xs) -> c_17(sumList^#(xs, 0())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { p^#(s(s(x))) -> c_10(p^#(s(x))) , inc^#(s(x)) -> c_12(inc^#(x)) , sumList^#(xs, y) -> c_13(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), isEmpty^#(xs), isZero^#(head(xs)), head^#(xs), tail^#(xs), p^#(head(xs)), head^#(xs), tail^#(xs), inc^#(y)) , if^#(false(), false(), y, xs, ys, x) -> c_14(sumList^#(ys, x)) , if^#(false(), true(), y, xs, ys, x) -> c_15(sumList^#(xs, y)) , sum^#(xs) -> c_17(sumList^#(xs, 0())) } Weak 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() , tail^#(cons(x, xs)) -> c_6() , tail^#(nil()) -> c_7() , p^#(0()) -> c_8() , p^#(s(0())) -> c_9() , inc^#(0()) -> c_11() , if^#(true(), b, y, xs, ys, x) -> c_16() } Weak 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() , 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)) , sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) , if(false(), false(), y, xs, ys, x) -> sumList(ys, x) , if(false(), true(), y, xs, ys, x) -> sumList(xs, y) , if(true(), b, y, xs, ys, x) -> y , sum(xs) -> sumList(xs, 0()) } 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. { 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() , tail^#(cons(x, xs)) -> c_6() , tail^#(nil()) -> c_7() , p^#(0()) -> c_8() , p^#(s(0())) -> c_9() , inc^#(0()) -> c_11() , if^#(true(), b, y, xs, ys, x) -> c_16() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { p^#(s(s(x))) -> c_10(p^#(s(x))) , inc^#(s(x)) -> c_12(inc^#(x)) , sumList^#(xs, y) -> c_13(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), isEmpty^#(xs), isZero^#(head(xs)), head^#(xs), tail^#(xs), p^#(head(xs)), head^#(xs), tail^#(xs), inc^#(y)) , if^#(false(), false(), y, xs, ys, x) -> c_14(sumList^#(ys, x)) , if^#(false(), true(), y, xs, ys, x) -> c_15(sumList^#(xs, y)) , sum^#(xs) -> c_17(sumList^#(xs, 0())) } Weak 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() , 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)) , sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) , if(false(), false(), y, xs, ys, x) -> sumList(ys, x) , if(false(), true(), y, xs, ys, x) -> sumList(xs, y) , if(true(), b, y, xs, ys, x) -> y , sum(xs) -> sumList(xs, 0()) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { sumList^#(xs, y) -> c_13(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), isEmpty^#(xs), isZero^#(head(xs)), head^#(xs), tail^#(xs), p^#(head(xs)), head^#(xs), tail^#(xs), inc^#(y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { p^#(s(s(x))) -> c_1(p^#(s(x))) , inc^#(s(x)) -> c_2(inc^#(x)) , sumList^#(xs, y) -> c_3(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), p^#(head(xs)), inc^#(y)) , if^#(false(), false(), y, xs, ys, x) -> c_4(sumList^#(ys, x)) , if^#(false(), true(), y, xs, ys, x) -> c_5(sumList^#(xs, y)) , sum^#(xs) -> c_6(sumList^#(xs, 0())) } Weak 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() , 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)) , sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) , if(false(), false(), y, xs, ys, x) -> sumList(ys, x) , if(false(), true(), y, xs, ys, x) -> sumList(xs, y) , if(true(), b, y, xs, ys, x) -> y , sum(xs) -> sumList(xs, 0()) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { 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() , 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)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { p^#(s(s(x))) -> c_1(p^#(s(x))) , inc^#(s(x)) -> c_2(inc^#(x)) , sumList^#(xs, y) -> c_3(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), p^#(head(xs)), inc^#(y)) , if^#(false(), false(), y, xs, ys, x) -> c_4(sumList^#(ys, x)) , if^#(false(), true(), y, xs, ys, x) -> c_5(sumList^#(xs, y)) , sum^#(xs) -> c_6(sumList^#(xs, 0())) } Weak 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() , 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)) } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: p^#(s(s(x))) -> c_1(p^#(s(x))) -->_1 p^#(s(s(x))) -> c_1(p^#(s(x))) :1 2: inc^#(s(x)) -> c_2(inc^#(x)) -->_1 inc^#(s(x)) -> c_2(inc^#(x)) :2 3: sumList^#(xs, y) -> c_3(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), p^#(head(xs)), inc^#(y)) -->_1 if^#(false(), true(), y, xs, ys, x) -> c_5(sumList^#(xs, y)) :5 -->_1 if^#(false(), false(), y, xs, ys, x) -> c_4(sumList^#(ys, x)) :4 -->_3 inc^#(s(x)) -> c_2(inc^#(x)) :2 -->_2 p^#(s(s(x))) -> c_1(p^#(s(x))) :1 4: if^#(false(), false(), y, xs, ys, x) -> c_4(sumList^#(ys, x)) -->_1 sumList^#(xs, y) -> c_3(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), p^#(head(xs)), inc^#(y)) :3 5: if^#(false(), true(), y, xs, ys, x) -> c_5(sumList^#(xs, y)) -->_1 sumList^#(xs, y) -> c_3(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), p^#(head(xs)), inc^#(y)) :3 6: sum^#(xs) -> c_6(sumList^#(xs, 0())) -->_1 sumList^#(xs, y) -> c_3(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), p^#(head(xs)), inc^#(y)) :3 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { sum^#(xs) -> c_6(sumList^#(xs, 0())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { p^#(s(s(x))) -> c_1(p^#(s(x))) , inc^#(s(x)) -> c_2(inc^#(x)) , sumList^#(xs, y) -> c_3(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)), p^#(head(xs)), inc^#(y)) , if^#(false(), false(), y, xs, ys, x) -> c_4(sumList^#(ys, x)) , if^#(false(), true(), y, xs, ys, x) -> c_5(sumList^#(xs, y)) } Weak 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() , 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)) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..