MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { plus(x, y) -> plusIter(x, y, 0()) , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) , ifPlus(true(), x, y, z) -> y , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , sum(xs) -> sumIter(xs, 0()) , sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))) , ifSum(true(), xs, x, y) -> x , ifSum(false(), xs, x, y) -> sumIter(tail(xs), y) , isempty(nil()) -> true() , isempty(cons(x, xs)) -> false() , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , a() -> b() , a() -> c() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) , plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , ifPlus^#(true(), x, y, z) -> c_3() , ifPlus^#(false(), x, y, z) -> c_4(plusIter^#(x, s(y), s(z))) , le^#(0(), y) -> c_5() , le^#(s(x), 0()) -> c_6() , le^#(s(x), s(y)) -> c_7(le^#(x, y)) , sum^#(xs) -> c_8(sumIter^#(xs, 0())) , sumIter^#(xs, x) -> c_9(ifSum^#(isempty(xs), xs, x, plus(x, head(xs))), isempty^#(xs), plus^#(x, head(xs)), head^#(xs)) , ifSum^#(true(), xs, x, y) -> c_10() , ifSum^#(false(), xs, x, y) -> c_11(sumIter^#(tail(xs), y), tail^#(xs)) , isempty^#(nil()) -> c_12() , isempty^#(cons(x, xs)) -> c_13() , head^#(nil()) -> c_14() , head^#(cons(x, xs)) -> c_15() , tail^#(nil()) -> c_16() , tail^#(cons(x, xs)) -> c_17() , a^#() -> c_18() , a^#() -> c_19() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) , plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , ifPlus^#(true(), x, y, z) -> c_3() , ifPlus^#(false(), x, y, z) -> c_4(plusIter^#(x, s(y), s(z))) , le^#(0(), y) -> c_5() , le^#(s(x), 0()) -> c_6() , le^#(s(x), s(y)) -> c_7(le^#(x, y)) , sum^#(xs) -> c_8(sumIter^#(xs, 0())) , sumIter^#(xs, x) -> c_9(ifSum^#(isempty(xs), xs, x, plus(x, head(xs))), isempty^#(xs), plus^#(x, head(xs)), head^#(xs)) , ifSum^#(true(), xs, x, y) -> c_10() , ifSum^#(false(), xs, x, y) -> c_11(sumIter^#(tail(xs), y), tail^#(xs)) , isempty^#(nil()) -> c_12() , isempty^#(cons(x, xs)) -> c_13() , head^#(nil()) -> c_14() , head^#(cons(x, xs)) -> c_15() , tail^#(nil()) -> c_16() , tail^#(cons(x, xs)) -> c_17() , a^#() -> c_18() , a^#() -> c_19() } Weak Trs: { plus(x, y) -> plusIter(x, y, 0()) , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) , ifPlus(true(), x, y, z) -> y , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , sum(xs) -> sumIter(xs, 0()) , sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))) , ifSum(true(), xs, x, y) -> x , ifSum(false(), xs, x, y) -> sumIter(tail(xs), y) , isempty(nil()) -> true() , isempty(cons(x, xs)) -> false() , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , a() -> b() , a() -> c() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3,5,6,10,12,13,14,15,16,17,18,19} by applications of Pre({3,5,6,10,12,13,14,15,16,17,18,19}) = {2,7,9,11}. Here rules are labeled as follows: DPs: { 1: plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) , 2: plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , 3: ifPlus^#(true(), x, y, z) -> c_3() , 4: ifPlus^#(false(), x, y, z) -> c_4(plusIter^#(x, s(y), s(z))) , 5: le^#(0(), y) -> c_5() , 6: le^#(s(x), 0()) -> c_6() , 7: le^#(s(x), s(y)) -> c_7(le^#(x, y)) , 8: sum^#(xs) -> c_8(sumIter^#(xs, 0())) , 9: sumIter^#(xs, x) -> c_9(ifSum^#(isempty(xs), xs, x, plus(x, head(xs))), isempty^#(xs), plus^#(x, head(xs)), head^#(xs)) , 10: ifSum^#(true(), xs, x, y) -> c_10() , 11: ifSum^#(false(), xs, x, y) -> c_11(sumIter^#(tail(xs), y), tail^#(xs)) , 12: isempty^#(nil()) -> c_12() , 13: isempty^#(cons(x, xs)) -> c_13() , 14: head^#(nil()) -> c_14() , 15: head^#(cons(x, xs)) -> c_15() , 16: tail^#(nil()) -> c_16() , 17: tail^#(cons(x, xs)) -> c_17() , 18: a^#() -> c_18() , 19: a^#() -> c_19() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) , plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , ifPlus^#(false(), x, y, z) -> c_4(plusIter^#(x, s(y), s(z))) , le^#(s(x), s(y)) -> c_7(le^#(x, y)) , sum^#(xs) -> c_8(sumIter^#(xs, 0())) , sumIter^#(xs, x) -> c_9(ifSum^#(isempty(xs), xs, x, plus(x, head(xs))), isempty^#(xs), plus^#(x, head(xs)), head^#(xs)) , ifSum^#(false(), xs, x, y) -> c_11(sumIter^#(tail(xs), y), tail^#(xs)) } Weak DPs: { ifPlus^#(true(), x, y, z) -> c_3() , le^#(0(), y) -> c_5() , le^#(s(x), 0()) -> c_6() , ifSum^#(true(), xs, x, y) -> c_10() , isempty^#(nil()) -> c_12() , isempty^#(cons(x, xs)) -> c_13() , head^#(nil()) -> c_14() , head^#(cons(x, xs)) -> c_15() , tail^#(nil()) -> c_16() , tail^#(cons(x, xs)) -> c_17() , a^#() -> c_18() , a^#() -> c_19() } Weak Trs: { plus(x, y) -> plusIter(x, y, 0()) , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) , ifPlus(true(), x, y, z) -> y , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , sum(xs) -> sumIter(xs, 0()) , sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))) , ifSum(true(), xs, x, y) -> x , ifSum(false(), xs, x, y) -> sumIter(tail(xs), y) , isempty(nil()) -> true() , isempty(cons(x, xs)) -> false() , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , a() -> b() , a() -> c() } 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. { ifPlus^#(true(), x, y, z) -> c_3() , le^#(0(), y) -> c_5() , le^#(s(x), 0()) -> c_6() , ifSum^#(true(), xs, x, y) -> c_10() , isempty^#(nil()) -> c_12() , isempty^#(cons(x, xs)) -> c_13() , head^#(nil()) -> c_14() , head^#(cons(x, xs)) -> c_15() , tail^#(nil()) -> c_16() , tail^#(cons(x, xs)) -> c_17() , a^#() -> c_18() , a^#() -> c_19() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) , plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , ifPlus^#(false(), x, y, z) -> c_4(plusIter^#(x, s(y), s(z))) , le^#(s(x), s(y)) -> c_7(le^#(x, y)) , sum^#(xs) -> c_8(sumIter^#(xs, 0())) , sumIter^#(xs, x) -> c_9(ifSum^#(isempty(xs), xs, x, plus(x, head(xs))), isempty^#(xs), plus^#(x, head(xs)), head^#(xs)) , ifSum^#(false(), xs, x, y) -> c_11(sumIter^#(tail(xs), y), tail^#(xs)) } Weak Trs: { plus(x, y) -> plusIter(x, y, 0()) , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) , ifPlus(true(), x, y, z) -> y , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , sum(xs) -> sumIter(xs, 0()) , sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))) , ifSum(true(), xs, x, y) -> x , ifSum(false(), xs, x, y) -> sumIter(tail(xs), y) , isempty(nil()) -> true() , isempty(cons(x, xs)) -> false() , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , a() -> b() , a() -> c() } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { sumIter^#(xs, x) -> c_9(ifSum^#(isempty(xs), xs, x, plus(x, head(xs))), isempty^#(xs), plus^#(x, head(xs)), head^#(xs)) , ifSum^#(false(), xs, x, y) -> c_11(sumIter^#(tail(xs), y), tail^#(xs)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) , plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , ifPlus^#(false(), x, y, z) -> c_3(plusIter^#(x, s(y), s(z))) , le^#(s(x), s(y)) -> c_4(le^#(x, y)) , sum^#(xs) -> c_5(sumIter^#(xs, 0())) , sumIter^#(xs, x) -> c_6(ifSum^#(isempty(xs), xs, x, plus(x, head(xs))), plus^#(x, head(xs))) , ifSum^#(false(), xs, x, y) -> c_7(sumIter^#(tail(xs), y)) } Weak Trs: { plus(x, y) -> plusIter(x, y, 0()) , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) , ifPlus(true(), x, y, z) -> y , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , sum(xs) -> sumIter(xs, 0()) , sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))) , ifSum(true(), xs, x, y) -> x , ifSum(false(), xs, x, y) -> sumIter(tail(xs), y) , isempty(nil()) -> true() , isempty(cons(x, xs)) -> false() , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , a() -> b() , a() -> c() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { plus(x, y) -> plusIter(x, y, 0()) , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) , ifPlus(true(), x, y, z) -> y , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , isempty(nil()) -> true() , isempty(cons(x, xs)) -> false() , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) , plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , ifPlus^#(false(), x, y, z) -> c_3(plusIter^#(x, s(y), s(z))) , le^#(s(x), s(y)) -> c_4(le^#(x, y)) , sum^#(xs) -> c_5(sumIter^#(xs, 0())) , sumIter^#(xs, x) -> c_6(ifSum^#(isempty(xs), xs, x, plus(x, head(xs))), plus^#(x, head(xs))) , ifSum^#(false(), xs, x, y) -> c_7(sumIter^#(tail(xs), y)) } Weak Trs: { plus(x, y) -> plusIter(x, y, 0()) , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) , ifPlus(true(), x, y, z) -> y , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , isempty(nil()) -> true() , isempty(cons(x, xs)) -> false() , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) -->_1 plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) :2 2: plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) -->_2 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4 -->_1 ifPlus^#(false(), x, y, z) -> c_3(plusIter^#(x, s(y), s(z))) :3 3: ifPlus^#(false(), x, y, z) -> c_3(plusIter^#(x, s(y), s(z))) -->_1 plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) :2 4: le^#(s(x), s(y)) -> c_4(le^#(x, y)) -->_1 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4 5: sum^#(xs) -> c_5(sumIter^#(xs, 0())) -->_1 sumIter^#(xs, x) -> c_6(ifSum^#(isempty(xs), xs, x, plus(x, head(xs))), plus^#(x, head(xs))) :6 6: sumIter^#(xs, x) -> c_6(ifSum^#(isempty(xs), xs, x, plus(x, head(xs))), plus^#(x, head(xs))) -->_1 ifSum^#(false(), xs, x, y) -> c_7(sumIter^#(tail(xs), y)) :7 -->_2 plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) :1 7: ifSum^#(false(), xs, x, y) -> c_7(sumIter^#(tail(xs), y)) -->_1 sumIter^#(xs, x) -> c_6(ifSum^#(isempty(xs), xs, x, plus(x, head(xs))), plus^#(x, head(xs))) :6 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_5(sumIter^#(xs, 0())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) , plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , ifPlus^#(false(), x, y, z) -> c_3(plusIter^#(x, s(y), s(z))) , le^#(s(x), s(y)) -> c_4(le^#(x, y)) , sumIter^#(xs, x) -> c_6(ifSum^#(isempty(xs), xs, x, plus(x, head(xs))), plus^#(x, head(xs))) , ifSum^#(false(), xs, x, y) -> c_7(sumIter^#(tail(xs), y)) } Weak Trs: { plus(x, y) -> plusIter(x, y, 0()) , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) , ifPlus(true(), x, y, z) -> y , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , isempty(nil()) -> true() , isempty(cons(x, xs)) -> false() , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..