MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { average(x, y) -> if(ge(x, y), x, y) , if(true(), x, y) -> averIter(y, x, y) , if(false(), x, y) -> averIter(x, y, x) , ge(x, 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , ge(0(), s(y)) -> false() , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) , ifIter(true(), x, y, z) -> z , ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))) , plus(s(x), y) -> s(plus(x, y)) , plus(0(), y) -> y , append(nil(), y) -> y , append(cons(n, x), y) -> cons(n, app(x, y)) , low(n, nil()) -> nil() , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) , if_low(true(), n, cons(m, x)) -> low(n, x) , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) , high(n, nil()) -> nil() , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) , if_high(false(), n, cons(m, x)) -> high(n, x) , quicksort(x) -> ifquick(isempty(x), x) , ifquick(true(), x) -> nil() , ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) , isempty(nil()) -> true() , isempty(cons(n, x)) -> false() , head(nil()) -> error() , head(cons(n, x)) -> n , tail(nil()) -> nil() , tail(cons(n, x)) -> x , a() -> b() , a() -> c() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { average^#(x, y) -> c_1(if^#(ge(x, y), x, y), ge^#(x, y)) , if^#(true(), x, y) -> c_2(averIter^#(y, x, y)) , if^#(false(), x, y) -> c_3(averIter^#(x, y, x)) , ge^#(x, 0()) -> c_4() , ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , ge^#(0(), s(y)) -> c_6() , averIter^#(x, y, z) -> c_7(ifIter^#(ge(x, y), x, y, z), ge^#(x, y)) , ifIter^#(true(), x, y, z) -> c_8() , ifIter^#(false(), x, y, z) -> c_9(averIter^#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))), plus^#(x, s(s(s(0())))), plus^#(y, s(0())), plus^#(z, s(0()))) , plus^#(s(x), y) -> c_10(plus^#(x, y)) , plus^#(0(), y) -> c_11() , append^#(nil(), y) -> c_12() , append^#(cons(n, x), y) -> c_13() , low^#(n, nil()) -> c_14() , low^#(n, cons(m, x)) -> c_15(if_low^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , if_low^#(true(), n, cons(m, x)) -> c_16(low^#(n, x)) , if_low^#(false(), n, cons(m, x)) -> c_17(low^#(n, x)) , high^#(n, nil()) -> c_18() , high^#(n, cons(m, x)) -> c_19(if_high^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , if_high^#(true(), n, cons(m, x)) -> c_20(average^#(m, m), high^#(n, x)) , if_high^#(false(), n, cons(m, x)) -> c_21(high^#(n, x)) , quicksort^#(x) -> c_22(ifquick^#(isempty(x), x), isempty^#(x)) , ifquick^#(true(), x) -> c_23() , ifquick^#(false(), x) -> c_24(append^#(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))), quicksort^#(low(head(x), tail(x))), low^#(head(x), tail(x)), head^#(x), tail^#(x), tail^#(x), quicksort^#(high(head(x), tail(x))), high^#(head(x), tail(x)), head^#(x), tail^#(x)) , isempty^#(nil()) -> c_25() , isempty^#(cons(n, x)) -> c_26() , head^#(nil()) -> c_27() , head^#(cons(n, x)) -> c_28() , tail^#(nil()) -> c_29() , tail^#(cons(n, x)) -> c_30() , a^#() -> c_31() , a^#() -> c_32() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { average^#(x, y) -> c_1(if^#(ge(x, y), x, y), ge^#(x, y)) , if^#(true(), x, y) -> c_2(averIter^#(y, x, y)) , if^#(false(), x, y) -> c_3(averIter^#(x, y, x)) , ge^#(x, 0()) -> c_4() , ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , ge^#(0(), s(y)) -> c_6() , averIter^#(x, y, z) -> c_7(ifIter^#(ge(x, y), x, y, z), ge^#(x, y)) , ifIter^#(true(), x, y, z) -> c_8() , ifIter^#(false(), x, y, z) -> c_9(averIter^#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))), plus^#(x, s(s(s(0())))), plus^#(y, s(0())), plus^#(z, s(0()))) , plus^#(s(x), y) -> c_10(plus^#(x, y)) , plus^#(0(), y) -> c_11() , append^#(nil(), y) -> c_12() , append^#(cons(n, x), y) -> c_13() , low^#(n, nil()) -> c_14() , low^#(n, cons(m, x)) -> c_15(if_low^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , if_low^#(true(), n, cons(m, x)) -> c_16(low^#(n, x)) , if_low^#(false(), n, cons(m, x)) -> c_17(low^#(n, x)) , high^#(n, nil()) -> c_18() , high^#(n, cons(m, x)) -> c_19(if_high^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , if_high^#(true(), n, cons(m, x)) -> c_20(average^#(m, m), high^#(n, x)) , if_high^#(false(), n, cons(m, x)) -> c_21(high^#(n, x)) , quicksort^#(x) -> c_22(ifquick^#(isempty(x), x), isempty^#(x)) , ifquick^#(true(), x) -> c_23() , ifquick^#(false(), x) -> c_24(append^#(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))), quicksort^#(low(head(x), tail(x))), low^#(head(x), tail(x)), head^#(x), tail^#(x), tail^#(x), quicksort^#(high(head(x), tail(x))), high^#(head(x), tail(x)), head^#(x), tail^#(x)) , isempty^#(nil()) -> c_25() , isempty^#(cons(n, x)) -> c_26() , head^#(nil()) -> c_27() , head^#(cons(n, x)) -> c_28() , tail^#(nil()) -> c_29() , tail^#(cons(n, x)) -> c_30() , a^#() -> c_31() , a^#() -> c_32() } Weak Trs: { average(x, y) -> if(ge(x, y), x, y) , if(true(), x, y) -> averIter(y, x, y) , if(false(), x, y) -> averIter(x, y, x) , ge(x, 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , ge(0(), s(y)) -> false() , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) , ifIter(true(), x, y, z) -> z , ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))) , plus(s(x), y) -> s(plus(x, y)) , plus(0(), y) -> y , append(nil(), y) -> y , append(cons(n, x), y) -> cons(n, app(x, y)) , low(n, nil()) -> nil() , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) , if_low(true(), n, cons(m, x)) -> low(n, x) , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) , high(n, nil()) -> nil() , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) , if_high(false(), n, cons(m, x)) -> high(n, x) , quicksort(x) -> ifquick(isempty(x), x) , ifquick(true(), x) -> nil() , ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) , isempty(nil()) -> true() , isempty(cons(n, x)) -> false() , head(nil()) -> error() , head(cons(n, x)) -> n , tail(nil()) -> nil() , tail(cons(n, x)) -> x , a() -> b() , a() -> c() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {4,6,8,11,12,13,14,18,23,25,26,27,28,29,30,31,32} by applications of Pre({4,6,8,11,12,13,14,18,23,25,26,27,28,29,30,31,32}) = {1,5,7,9,10,15,16,17,19,20,21,22,24}. Here rules are labeled as follows: DPs: { 1: average^#(x, y) -> c_1(if^#(ge(x, y), x, y), ge^#(x, y)) , 2: if^#(true(), x, y) -> c_2(averIter^#(y, x, y)) , 3: if^#(false(), x, y) -> c_3(averIter^#(x, y, x)) , 4: ge^#(x, 0()) -> c_4() , 5: ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , 6: ge^#(0(), s(y)) -> c_6() , 7: averIter^#(x, y, z) -> c_7(ifIter^#(ge(x, y), x, y, z), ge^#(x, y)) , 8: ifIter^#(true(), x, y, z) -> c_8() , 9: ifIter^#(false(), x, y, z) -> c_9(averIter^#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))), plus^#(x, s(s(s(0())))), plus^#(y, s(0())), plus^#(z, s(0()))) , 10: plus^#(s(x), y) -> c_10(plus^#(x, y)) , 11: plus^#(0(), y) -> c_11() , 12: append^#(nil(), y) -> c_12() , 13: append^#(cons(n, x), y) -> c_13() , 14: low^#(n, nil()) -> c_14() , 15: low^#(n, cons(m, x)) -> c_15(if_low^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , 16: if_low^#(true(), n, cons(m, x)) -> c_16(low^#(n, x)) , 17: if_low^#(false(), n, cons(m, x)) -> c_17(low^#(n, x)) , 18: high^#(n, nil()) -> c_18() , 19: high^#(n, cons(m, x)) -> c_19(if_high^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , 20: if_high^#(true(), n, cons(m, x)) -> c_20(average^#(m, m), high^#(n, x)) , 21: if_high^#(false(), n, cons(m, x)) -> c_21(high^#(n, x)) , 22: quicksort^#(x) -> c_22(ifquick^#(isempty(x), x), isempty^#(x)) , 23: ifquick^#(true(), x) -> c_23() , 24: ifquick^#(false(), x) -> c_24(append^#(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))), quicksort^#(low(head(x), tail(x))), low^#(head(x), tail(x)), head^#(x), tail^#(x), tail^#(x), quicksort^#(high(head(x), tail(x))), high^#(head(x), tail(x)), head^#(x), tail^#(x)) , 25: isempty^#(nil()) -> c_25() , 26: isempty^#(cons(n, x)) -> c_26() , 27: head^#(nil()) -> c_27() , 28: head^#(cons(n, x)) -> c_28() , 29: tail^#(nil()) -> c_29() , 30: tail^#(cons(n, x)) -> c_30() , 31: a^#() -> c_31() , 32: a^#() -> c_32() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { average^#(x, y) -> c_1(if^#(ge(x, y), x, y), ge^#(x, y)) , if^#(true(), x, y) -> c_2(averIter^#(y, x, y)) , if^#(false(), x, y) -> c_3(averIter^#(x, y, x)) , ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , averIter^#(x, y, z) -> c_7(ifIter^#(ge(x, y), x, y, z), ge^#(x, y)) , ifIter^#(false(), x, y, z) -> c_9(averIter^#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))), plus^#(x, s(s(s(0())))), plus^#(y, s(0())), plus^#(z, s(0()))) , plus^#(s(x), y) -> c_10(plus^#(x, y)) , low^#(n, cons(m, x)) -> c_15(if_low^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , if_low^#(true(), n, cons(m, x)) -> c_16(low^#(n, x)) , if_low^#(false(), n, cons(m, x)) -> c_17(low^#(n, x)) , high^#(n, cons(m, x)) -> c_19(if_high^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , if_high^#(true(), n, cons(m, x)) -> c_20(average^#(m, m), high^#(n, x)) , if_high^#(false(), n, cons(m, x)) -> c_21(high^#(n, x)) , quicksort^#(x) -> c_22(ifquick^#(isempty(x), x), isempty^#(x)) , ifquick^#(false(), x) -> c_24(append^#(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))), quicksort^#(low(head(x), tail(x))), low^#(head(x), tail(x)), head^#(x), tail^#(x), tail^#(x), quicksort^#(high(head(x), tail(x))), high^#(head(x), tail(x)), head^#(x), tail^#(x)) } Weak DPs: { ge^#(x, 0()) -> c_4() , ge^#(0(), s(y)) -> c_6() , ifIter^#(true(), x, y, z) -> c_8() , plus^#(0(), y) -> c_11() , append^#(nil(), y) -> c_12() , append^#(cons(n, x), y) -> c_13() , low^#(n, nil()) -> c_14() , high^#(n, nil()) -> c_18() , ifquick^#(true(), x) -> c_23() , isempty^#(nil()) -> c_25() , isempty^#(cons(n, x)) -> c_26() , head^#(nil()) -> c_27() , head^#(cons(n, x)) -> c_28() , tail^#(nil()) -> c_29() , tail^#(cons(n, x)) -> c_30() , a^#() -> c_31() , a^#() -> c_32() } Weak Trs: { average(x, y) -> if(ge(x, y), x, y) , if(true(), x, y) -> averIter(y, x, y) , if(false(), x, y) -> averIter(x, y, x) , ge(x, 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , ge(0(), s(y)) -> false() , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) , ifIter(true(), x, y, z) -> z , ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))) , plus(s(x), y) -> s(plus(x, y)) , plus(0(), y) -> y , append(nil(), y) -> y , append(cons(n, x), y) -> cons(n, app(x, y)) , low(n, nil()) -> nil() , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) , if_low(true(), n, cons(m, x)) -> low(n, x) , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) , high(n, nil()) -> nil() , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) , if_high(false(), n, cons(m, x)) -> high(n, x) , quicksort(x) -> ifquick(isempty(x), x) , ifquick(true(), x) -> nil() , ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) , isempty(nil()) -> true() , isempty(cons(n, x)) -> false() , head(nil()) -> error() , head(cons(n, x)) -> n , tail(nil()) -> nil() , tail(cons(n, x)) -> x , 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. { ge^#(x, 0()) -> c_4() , ge^#(0(), s(y)) -> c_6() , ifIter^#(true(), x, y, z) -> c_8() , plus^#(0(), y) -> c_11() , append^#(nil(), y) -> c_12() , append^#(cons(n, x), y) -> c_13() , low^#(n, nil()) -> c_14() , high^#(n, nil()) -> c_18() , ifquick^#(true(), x) -> c_23() , isempty^#(nil()) -> c_25() , isempty^#(cons(n, x)) -> c_26() , head^#(nil()) -> c_27() , head^#(cons(n, x)) -> c_28() , tail^#(nil()) -> c_29() , tail^#(cons(n, x)) -> c_30() , a^#() -> c_31() , a^#() -> c_32() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { average^#(x, y) -> c_1(if^#(ge(x, y), x, y), ge^#(x, y)) , if^#(true(), x, y) -> c_2(averIter^#(y, x, y)) , if^#(false(), x, y) -> c_3(averIter^#(x, y, x)) , ge^#(s(x), s(y)) -> c_5(ge^#(x, y)) , averIter^#(x, y, z) -> c_7(ifIter^#(ge(x, y), x, y, z), ge^#(x, y)) , ifIter^#(false(), x, y, z) -> c_9(averIter^#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))), plus^#(x, s(s(s(0())))), plus^#(y, s(0())), plus^#(z, s(0()))) , plus^#(s(x), y) -> c_10(plus^#(x, y)) , low^#(n, cons(m, x)) -> c_15(if_low^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , if_low^#(true(), n, cons(m, x)) -> c_16(low^#(n, x)) , if_low^#(false(), n, cons(m, x)) -> c_17(low^#(n, x)) , high^#(n, cons(m, x)) -> c_19(if_high^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , if_high^#(true(), n, cons(m, x)) -> c_20(average^#(m, m), high^#(n, x)) , if_high^#(false(), n, cons(m, x)) -> c_21(high^#(n, x)) , quicksort^#(x) -> c_22(ifquick^#(isempty(x), x), isempty^#(x)) , ifquick^#(false(), x) -> c_24(append^#(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))), quicksort^#(low(head(x), tail(x))), low^#(head(x), tail(x)), head^#(x), tail^#(x), tail^#(x), quicksort^#(high(head(x), tail(x))), high^#(head(x), tail(x)), head^#(x), tail^#(x)) } Weak Trs: { average(x, y) -> if(ge(x, y), x, y) , if(true(), x, y) -> averIter(y, x, y) , if(false(), x, y) -> averIter(x, y, x) , ge(x, 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , ge(0(), s(y)) -> false() , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) , ifIter(true(), x, y, z) -> z , ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))) , plus(s(x), y) -> s(plus(x, y)) , plus(0(), y) -> y , append(nil(), y) -> y , append(cons(n, x), y) -> cons(n, app(x, y)) , low(n, nil()) -> nil() , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) , if_low(true(), n, cons(m, x)) -> low(n, x) , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) , high(n, nil()) -> nil() , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) , if_high(false(), n, cons(m, x)) -> high(n, x) , quicksort(x) -> ifquick(isempty(x), x) , ifquick(true(), x) -> nil() , ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) , isempty(nil()) -> true() , isempty(cons(n, x)) -> false() , head(nil()) -> error() , head(cons(n, x)) -> n , tail(nil()) -> nil() , tail(cons(n, x)) -> x , 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: { quicksort^#(x) -> c_22(ifquick^#(isempty(x), x), isempty^#(x)) , ifquick^#(false(), x) -> c_24(append^#(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))), quicksort^#(low(head(x), tail(x))), low^#(head(x), tail(x)), head^#(x), tail^#(x), tail^#(x), quicksort^#(high(head(x), tail(x))), high^#(head(x), tail(x)), head^#(x), tail^#(x)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { average^#(x, y) -> c_1(if^#(ge(x, y), x, y), ge^#(x, y)) , if^#(true(), x, y) -> c_2(averIter^#(y, x, y)) , if^#(false(), x, y) -> c_3(averIter^#(x, y, x)) , ge^#(s(x), s(y)) -> c_4(ge^#(x, y)) , averIter^#(x, y, z) -> c_5(ifIter^#(ge(x, y), x, y, z), ge^#(x, y)) , ifIter^#(false(), x, y, z) -> c_6(averIter^#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))), plus^#(x, s(s(s(0())))), plus^#(y, s(0())), plus^#(z, s(0()))) , plus^#(s(x), y) -> c_7(plus^#(x, y)) , low^#(n, cons(m, x)) -> c_8(if_low^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , if_low^#(true(), n, cons(m, x)) -> c_9(low^#(n, x)) , if_low^#(false(), n, cons(m, x)) -> c_10(low^#(n, x)) , high^#(n, cons(m, x)) -> c_11(if_high^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , if_high^#(true(), n, cons(m, x)) -> c_12(average^#(m, m), high^#(n, x)) , if_high^#(false(), n, cons(m, x)) -> c_13(high^#(n, x)) , quicksort^#(x) -> c_14(ifquick^#(isempty(x), x)) , ifquick^#(false(), x) -> c_15(quicksort^#(low(head(x), tail(x))), low^#(head(x), tail(x)), quicksort^#(high(head(x), tail(x))), high^#(head(x), tail(x))) } Weak Trs: { average(x, y) -> if(ge(x, y), x, y) , if(true(), x, y) -> averIter(y, x, y) , if(false(), x, y) -> averIter(x, y, x) , ge(x, 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , ge(0(), s(y)) -> false() , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) , ifIter(true(), x, y, z) -> z , ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))) , plus(s(x), y) -> s(plus(x, y)) , plus(0(), y) -> y , append(nil(), y) -> y , append(cons(n, x), y) -> cons(n, app(x, y)) , low(n, nil()) -> nil() , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) , if_low(true(), n, cons(m, x)) -> low(n, x) , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) , high(n, nil()) -> nil() , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) , if_high(false(), n, cons(m, x)) -> high(n, x) , quicksort(x) -> ifquick(isempty(x), x) , ifquick(true(), x) -> nil() , ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) , isempty(nil()) -> true() , isempty(cons(n, x)) -> false() , head(nil()) -> error() , head(cons(n, x)) -> n , tail(nil()) -> nil() , tail(cons(n, x)) -> x , a() -> b() , a() -> c() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { average(x, y) -> if(ge(x, y), x, y) , if(true(), x, y) -> averIter(y, x, y) , if(false(), x, y) -> averIter(x, y, x) , ge(x, 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , ge(0(), s(y)) -> false() , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) , ifIter(true(), x, y, z) -> z , ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))) , plus(s(x), y) -> s(plus(x, y)) , plus(0(), y) -> y , low(n, nil()) -> nil() , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) , if_low(true(), n, cons(m, x)) -> low(n, x) , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) , high(n, nil()) -> nil() , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) , if_high(false(), n, cons(m, x)) -> high(n, x) , isempty(nil()) -> true() , isempty(cons(n, x)) -> false() , head(nil()) -> error() , head(cons(n, x)) -> n , tail(nil()) -> nil() , tail(cons(n, x)) -> x } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { average^#(x, y) -> c_1(if^#(ge(x, y), x, y), ge^#(x, y)) , if^#(true(), x, y) -> c_2(averIter^#(y, x, y)) , if^#(false(), x, y) -> c_3(averIter^#(x, y, x)) , ge^#(s(x), s(y)) -> c_4(ge^#(x, y)) , averIter^#(x, y, z) -> c_5(ifIter^#(ge(x, y), x, y, z), ge^#(x, y)) , ifIter^#(false(), x, y, z) -> c_6(averIter^#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))), plus^#(x, s(s(s(0())))), plus^#(y, s(0())), plus^#(z, s(0()))) , plus^#(s(x), y) -> c_7(plus^#(x, y)) , low^#(n, cons(m, x)) -> c_8(if_low^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , if_low^#(true(), n, cons(m, x)) -> c_9(low^#(n, x)) , if_low^#(false(), n, cons(m, x)) -> c_10(low^#(n, x)) , high^#(n, cons(m, x)) -> c_11(if_high^#(ge(m, n), n, cons(m, x)), ge^#(m, n)) , if_high^#(true(), n, cons(m, x)) -> c_12(average^#(m, m), high^#(n, x)) , if_high^#(false(), n, cons(m, x)) -> c_13(high^#(n, x)) , quicksort^#(x) -> c_14(ifquick^#(isempty(x), x)) , ifquick^#(false(), x) -> c_15(quicksort^#(low(head(x), tail(x))), low^#(head(x), tail(x)), quicksort^#(high(head(x), tail(x))), high^#(head(x), tail(x))) } Weak Trs: { average(x, y) -> if(ge(x, y), x, y) , if(true(), x, y) -> averIter(y, x, y) , if(false(), x, y) -> averIter(x, y, x) , ge(x, 0()) -> true() , ge(s(x), s(y)) -> ge(x, y) , ge(0(), s(y)) -> false() , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) , ifIter(true(), x, y, z) -> z , ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))) , plus(s(x), y) -> s(plus(x, y)) , plus(0(), y) -> y , low(n, nil()) -> nil() , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) , if_low(true(), n, cons(m, x)) -> low(n, x) , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) , high(n, nil()) -> nil() , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) , if_high(false(), n, cons(m, x)) -> high(n, x) , isempty(nil()) -> true() , isempty(cons(n, x)) -> false() , head(nil()) -> error() , head(cons(n, x)) -> n , tail(nil()) -> nil() , tail(cons(n, x)) -> x } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..