MAYBE Time: 0.328993 TRS: { 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(), average(x, y) -> if(ge(x, y), x, y), 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), 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(), quicksort x -> ifquick(isempty x, x), head nil() -> error(), head cons(n, x) -> n, tail nil() -> nil(), tail cons(n, x) -> x, a() -> b(), a() -> c()} DP: DP: { if#(true(), x, y) -> averIter#(y, x, y), if#(false(), x, y) -> averIter#(x, y, x), ge#(s x, s y) -> ge#(x, y), average#(x, y) -> if#(ge(x, y), x, y), average#(x, y) -> ge#(x, y), averIter#(x, y, z) -> ge#(x, y), averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z), ifIter#(false(), x, y, z) -> averIter#(plus(x, s s s 0()), plus(y, s 0()), plus(z, s 0())), ifIter#(false(), x, y, z) -> plus#(x, s s s 0()), ifIter#(false(), x, y, z) -> plus#(y, s 0()), ifIter#(false(), x, y, z) -> plus#(z, s 0()), plus#(s x, y) -> plus#(x, y), low#(n, cons(m, x)) -> ge#(m, n), 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)) -> low#(n, x), high#(n, cons(m, x)) -> ge#(m, n), high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)), if_high#(true(), n, cons(m, x)) -> average#(m, m), if_high#(true(), n, cons(m, x)) -> high#(n, x), if_high#(false(), n, cons(m, x)) -> high#(n, x), ifquick#(false(), x) -> append#(quicksort low(head x, tail x), cons(tail x, quicksort high(head x, tail x))), ifquick#(false(), x) -> low#(head x, tail x), ifquick#(false(), x) -> high#(head x, tail x), ifquick#(false(), x) -> quicksort# low(head x, tail x), ifquick#(false(), x) -> quicksort# high(head x, tail x), ifquick#(false(), x) -> head# x, ifquick#(false(), x) -> tail# x, quicksort# x -> ifquick#(isempty x, x), quicksort# x -> isempty# x} TRS: { 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(), average(x, y) -> if(ge(x, y), x, y), 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), 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(), quicksort x -> ifquick(isempty x, x), head nil() -> error(), head cons(n, x) -> n, tail nil() -> nil(), tail cons(n, x) -> x, a() -> b(), a() -> c()} UR: { 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(), average(x, y) -> if(ge(x, y), x, y), 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), 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(), quicksort x -> ifquick(isempty x, x), head nil() -> error(), head cons(n, x) -> n, tail nil() -> nil(), tail cons(n, x) -> x, d(w, v) -> w, d(w, v) -> v} EDG: {(ifIter#(false(), x, y, z) -> plus#(y, s 0()), plus#(s x, y) -> plus#(x, y)) (ifquick#(false(), x) -> low#(head x, tail x), low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x))) (ifquick#(false(), x) -> low#(head x, tail x), low#(n, cons(m, x)) -> ge#(m, n)) (if#(true(), x, y) -> averIter#(y, x, y), averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z)) (if#(true(), x, y) -> averIter#(y, x, y), averIter#(x, y, z) -> ge#(x, y)) (if#(false(), x, y) -> averIter#(x, y, x), averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z)) (if#(false(), x, y) -> averIter#(x, y, x), averIter#(x, y, z) -> ge#(x, y)) (if_high#(true(), n, cons(m, x)) -> average#(m, m), average#(x, y) -> ge#(x, y)) (if_high#(true(), n, cons(m, x)) -> average#(m, m), average#(x, y) -> if#(ge(x, y), x, y)) (high#(n, cons(m, x)) -> ge#(m, n), ge#(s x, s y) -> ge#(x, y)) (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y)) (averIter#(x, y, z) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y)) (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y)) (if_low#(true(), n, cons(m, x)) -> low#(n, x), low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x))) (if_low#(true(), n, cons(m, x)) -> low#(n, x), low#(n, cons(m, x)) -> ge#(m, n)) (high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)), if_high#(false(), n, cons(m, x)) -> high#(n, x)) (high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)), if_high#(true(), n, cons(m, x)) -> high#(n, x)) (high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)), if_high#(true(), n, cons(m, x)) -> average#(m, m)) (if_high#(false(), n, cons(m, x)) -> high#(n, x), high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x))) (if_high#(false(), n, cons(m, x)) -> high#(n, x), high#(n, cons(m, x)) -> ge#(m, n)) (ifquick#(false(), x) -> quicksort# high(head x, tail x), quicksort# x -> isempty# x) (ifquick#(false(), x) -> quicksort# high(head x, tail x), quicksort# x -> ifquick#(isempty x, x)) (ifquick#(false(), x) -> quicksort# low(head x, tail x), quicksort# x -> ifquick#(isempty x, x)) (ifquick#(false(), x) -> quicksort# low(head x, tail x), quicksort# x -> isempty# x) (if_high#(true(), n, cons(m, x)) -> high#(n, x), high#(n, cons(m, x)) -> ge#(m, n)) (if_high#(true(), n, cons(m, x)) -> high#(n, x), high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x))) (if_low#(false(), n, cons(m, x)) -> low#(n, x), low#(n, cons(m, x)) -> ge#(m, n)) (if_low#(false(), n, cons(m, x)) -> low#(n, x), low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x))) (low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)), if_low#(true(), n, cons(m, x)) -> low#(n, x)) (low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)), if_low#(false(), n, cons(m, x)) -> low#(n, x)) (ifIter#(false(), x, y, z) -> averIter#(plus(x, s s s 0()), plus(y, s 0()), plus(z, s 0())), averIter#(x, y, z) -> ge#(x, y)) (ifIter#(false(), x, y, z) -> averIter#(plus(x, s s s 0()), plus(y, s 0()), plus(z, s 0())), averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z)) (average#(x, y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y)) (averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z), ifIter#(false(), x, y, z) -> averIter#(plus(x, s s s 0()), plus(y, s 0()), plus(z, s 0()))) (averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z), ifIter#(false(), x, y, z) -> plus#(x, s s s 0())) (averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z), ifIter#(false(), x, y, z) -> plus#(y, s 0())) (averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z), ifIter#(false(), x, y, z) -> plus#(z, s 0())) (low#(n, cons(m, x)) -> ge#(m, n), ge#(s x, s y) -> ge#(x, y)) (quicksort# x -> ifquick#(isempty x, x), ifquick#(false(), x) -> append#(quicksort low(head x, tail x), cons(tail x, quicksort high(head x, tail x)))) (quicksort# x -> ifquick#(isempty x, x), ifquick#(false(), x) -> low#(head x, tail x)) (quicksort# x -> ifquick#(isempty x, x), ifquick#(false(), x) -> high#(head x, tail x)) (quicksort# x -> ifquick#(isempty x, x), ifquick#(false(), x) -> quicksort# low(head x, tail x)) (quicksort# x -> ifquick#(isempty x, x), ifquick#(false(), x) -> quicksort# high(head x, tail x)) (quicksort# x -> ifquick#(isempty x, x), ifquick#(false(), x) -> head# x) (quicksort# x -> ifquick#(isempty x, x), ifquick#(false(), x) -> tail# x) (average#(x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> averIter#(y, x, y)) (average#(x, y) -> if#(ge(x, y), x, y), if#(false(), x, y) -> averIter#(x, y, x)) (ifquick#(false(), x) -> high#(head x, tail x), high#(n, cons(m, x)) -> ge#(m, n)) (ifquick#(false(), x) -> high#(head x, tail x), high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x))) (ifIter#(false(), x, y, z) -> plus#(z, s 0()), plus#(s x, y) -> plus#(x, y)) (ifIter#(false(), x, y, z) -> plus#(x, s s s 0()), plus#(s x, y) -> plus#(x, y))} STATUS: arrows: 0.943333 SCCS (6): Scc: {ifquick#(false(), x) -> quicksort# low(head x, tail x), ifquick#(false(), x) -> quicksort# high(head x, tail x), quicksort# x -> ifquick#(isempty x, x)} Scc: { high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)), if_high#(true(), n, cons(m, x)) -> high#(n, x), if_high#(false(), n, cons(m, x)) -> high#(n, x)} Scc: { averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z), ifIter#(false(), x, y, z) -> averIter#(plus(x, s s s 0()), plus(y, s 0()), plus(z, s 0()))} Scc: { 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)) -> low#(n, x)} Scc: {ge#(s x, s y) -> ge#(x, y)} Scc: {plus#(s x, y) -> plus#(x, y)} SCC (3): Strict: {ifquick#(false(), x) -> quicksort# low(head x, tail x), ifquick#(false(), x) -> quicksort# high(head x, tail x), quicksort# x -> ifquick#(isempty x, x)} Weak: { 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(), average(x, y) -> if(ge(x, y), x, y), 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), 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(), quicksort x -> ifquick(isempty x, x), head nil() -> error(), head cons(n, x) -> n, tail nil() -> nil(), tail cons(n, x) -> x, a() -> b(), a() -> c()} Fail SCC (3): Strict: { high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)), if_high#(true(), n, cons(m, x)) -> high#(n, x), if_high#(false(), n, cons(m, x)) -> high#(n, x)} Weak: { 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(), average(x, y) -> if(ge(x, y), x, y), 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), 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(), quicksort x -> ifquick(isempty x, x), head nil() -> error(), head cons(n, x) -> n, tail nil() -> nil(), tail cons(n, x) -> x, a() -> b(), a() -> c()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifIter](x0, x1, x2, x3) = 0, [if](x0, x1, x2) = 0, [averIter](x0, x1, x2) = x0 + 1, [if_low](x0, x1, x2) = 0, [if_high](x0, x1, x2) = 0, [ge](x0, x1) = 0, [average](x0, x1) = 1, [plus](x0, x1) = 1, [append](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + x1 + 1, [app](x0, x1) = 1, [low](x0, x1) = 0, [high](x0, x1) = x0 + 1, [ifquick](x0, x1) = 0, [s](x0) = 0, [isempty](x0) = x0 + 1, [quicksort](x0) = x0 + 1, [head](x0) = x0 + 1, [tail](x0) = x0 + 1, [true] = 0, [false] = 0, [0] = 0, [nil] = 1, [error] = 0, [b] = 0, [a] = 0, [c] = 0, [if_high#](x0, x1, x2) = x0, [high#](x0, x1) = x0 + 1 Strict: if_high#(false(), n, cons(m, x)) -> high#(n, x) 1 + 1x + 0n + 1m >= 1 + 1x + 0n if_high#(true(), n, cons(m, x)) -> high#(n, x) 1 + 1x + 0n + 1m >= 1 + 1x + 0n high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)) 2 + 1x + 0n + 1m >= 1 + 1x + 0n + 1m Weak: a() -> c() 0 >= 0 a() -> b() 0 >= 0 tail cons(n, x) -> x 2 + 1x + 1n >= 1x tail nil() -> nil() 2 >= 1 head cons(n, x) -> n 2 + 1x + 1n >= 1n head nil() -> error() 2 >= 0 quicksort x -> ifquick(isempty x, x) 1 + 1x >= 0 + 0x isempty cons(n, x) -> false() 2 + 1x + 1n >= 0 isempty nil() -> true() 2 >= 0 ifquick(false(), x) -> append(quicksort low(head x, tail x), cons(tail x, quicksort high(head x, tail x))) 0 + 0x >= 2 + 0x ifquick(true(), x) -> nil() 0 + 0x >= 1 if_high(false(), n, cons(m, x)) -> high(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) 0 + 0x + 0n + 0m >= 3 + 1x + 0n + 0m high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) 2 + 1x + 0n + 1m >= 0 + 0x + 0n + 0m high(n, nil()) -> nil() 2 + 0n >= 1 if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) 0 + 0x + 0n + 0m >= 1 + 0x + 0n + 1m if_low(true(), n, cons(m, x)) -> low(n, x) 0 + 0x + 0n + 0m >= 0 + 0x + 0n low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) 0 + 0x + 0n + 0m >= 0 + 0x + 0n + 0m low(n, nil()) -> nil() 0 + 0n >= 1 append(cons(n, x), y) -> cons(n, app(x, y)) 2 + 1x + 0y + 1n >= 2 + 0x + 0y + 1n append(nil(), y) -> y 2 + 0y >= 1y plus(0(), y) -> y 1 + 0y >= 1y plus(s x, y) -> s plus(x, y) 1 + 0x + 0y >= 0 + 0x + 0y ifIter(false(), x, y, z) -> averIter(plus(x, s s s 0()), plus(y, s 0()), plus(z, s 0())) 0 + 0x + 0y + 0z >= 2 + 0x + 0y + 0z ifIter(true(), x, y, z) -> z 0 + 0x + 0y + 0z >= 1z averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) 1 + 0x + 1y + 0z >= 0 + 0x + 0y + 0z average(x, y) -> if(ge(x, y), x, y) 1 + 0x + 0y >= 0 + 0x + 0y ge(0(), s y) -> false() 0 + 0y >= 0 ge(s x, s y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(x, 0()) -> true() 0 + 0x >= 0 if(false(), x, y) -> averIter(x, y, x) 0 + 0x + 0y >= 1 + 0x + 1y if(true(), x, y) -> averIter(y, x, y) 0 + 0x + 0y >= 1 + 1x + 0y SCCS (0): SCC (2): Strict: { averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z), ifIter#(false(), x, y, z) -> averIter#(plus(x, s s s 0()), plus(y, s 0()), plus(z, s 0()))} Weak: { 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(), average(x, y) -> if(ge(x, y), x, y), 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), 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(), quicksort x -> ifquick(isempty x, x), head nil() -> error(), head cons(n, x) -> n, tail nil() -> nil(), tail cons(n, x) -> x, a() -> b(), a() -> c()} Fail SCC (3): Strict: { 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)) -> low#(n, x)} Weak: { 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(), average(x, y) -> if(ge(x, y), x, y), 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), 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(), quicksort x -> ifquick(isempty x, x), head nil() -> error(), head cons(n, x) -> n, tail nil() -> nil(), tail cons(n, x) -> x, a() -> b(), a() -> c()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifIter](x0, x1, x2, x3) = 0, [if](x0, x1, x2) = 0, [averIter](x0, x1, x2) = x0 + 1, [if_low](x0, x1, x2) = 0, [if_high](x0, x1, x2) = 0, [ge](x0, x1) = 0, [average](x0, x1) = 1, [plus](x0, x1) = 1, [append](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + x1 + 1, [app](x0, x1) = 1, [low](x0, x1) = 0, [high](x0, x1) = x0 + 1, [ifquick](x0, x1) = 0, [s](x0) = 0, [isempty](x0) = x0 + 1, [quicksort](x0) = x0 + 1, [head](x0) = x0 + 1, [tail](x0) = x0 + 1, [true] = 0, [false] = 0, [0] = 0, [nil] = 1, [error] = 0, [b] = 0, [a] = 0, [c] = 0, [if_low#](x0, x1, x2) = x0, [low#](x0, x1) = x0 + 1 Strict: if_low#(false(), n, cons(m, x)) -> low#(n, x) 1 + 1x + 0n + 1m >= 1 + 1x + 0n if_low#(true(), n, cons(m, x)) -> low#(n, x) 1 + 1x + 0n + 1m >= 1 + 1x + 0n low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)) 2 + 1x + 0n + 1m >= 1 + 1x + 0n + 1m Weak: a() -> c() 0 >= 0 a() -> b() 0 >= 0 tail cons(n, x) -> x 2 + 1x + 1n >= 1x tail nil() -> nil() 2 >= 1 head cons(n, x) -> n 2 + 1x + 1n >= 1n head nil() -> error() 2 >= 0 quicksort x -> ifquick(isempty x, x) 1 + 1x >= 0 + 0x isempty cons(n, x) -> false() 2 + 1x + 1n >= 0 isempty nil() -> true() 2 >= 0 ifquick(false(), x) -> append(quicksort low(head x, tail x), cons(tail x, quicksort high(head x, tail x))) 0 + 0x >= 2 + 0x ifquick(true(), x) -> nil() 0 + 0x >= 1 if_high(false(), n, cons(m, x)) -> high(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) 0 + 0x + 0n + 0m >= 3 + 1x + 0n + 0m high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) 2 + 1x + 0n + 1m >= 0 + 0x + 0n + 0m high(n, nil()) -> nil() 2 + 0n >= 1 if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) 0 + 0x + 0n + 0m >= 1 + 0x + 0n + 1m if_low(true(), n, cons(m, x)) -> low(n, x) 0 + 0x + 0n + 0m >= 0 + 0x + 0n low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) 0 + 0x + 0n + 0m >= 0 + 0x + 0n + 0m low(n, nil()) -> nil() 0 + 0n >= 1 append(cons(n, x), y) -> cons(n, app(x, y)) 2 + 1x + 0y + 1n >= 2 + 0x + 0y + 1n append(nil(), y) -> y 2 + 0y >= 1y plus(0(), y) -> y 1 + 0y >= 1y plus(s x, y) -> s plus(x, y) 1 + 0x + 0y >= 0 + 0x + 0y ifIter(false(), x, y, z) -> averIter(plus(x, s s s 0()), plus(y, s 0()), plus(z, s 0())) 0 + 0x + 0y + 0z >= 2 + 0x + 0y + 0z ifIter(true(), x, y, z) -> z 0 + 0x + 0y + 0z >= 1z averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) 1 + 0x + 1y + 0z >= 0 + 0x + 0y + 0z average(x, y) -> if(ge(x, y), x, y) 1 + 0x + 0y >= 0 + 0x + 0y ge(0(), s y) -> false() 0 + 0y >= 0 ge(s x, s y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(x, 0()) -> true() 0 + 0x >= 0 if(false(), x, y) -> averIter(x, y, x) 0 + 0x + 0y >= 1 + 0x + 1y if(true(), x, y) -> averIter(y, x, y) 0 + 0x + 0y >= 1 + 1x + 0y SCCS (0): SCC (1): Strict: {ge#(s x, s y) -> ge#(x, y)} Weak: { 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(), average(x, y) -> if(ge(x, y), x, y), 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), 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(), quicksort x -> ifquick(isempty x, x), head nil() -> error(), head cons(n, x) -> n, tail nil() -> nil(), tail cons(n, x) -> x, a() -> b(), a() -> c()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifIter](x0, x1, x2, x3) = x0 + x1 + 1, [if](x0, x1, x2) = x0 + x1 + 1, [averIter](x0, x1, x2) = x0, [if_low](x0, x1, x2) = 0, [if_high](x0, x1, x2) = 0, [ge](x0, x1) = x0 + 1, [average](x0, x1) = 0, [plus](x0, x1) = x0, [append](x0, x1) = x0 + 1, [cons](x0, x1) = x0, [app](x0, x1) = 0, [low](x0, x1) = x0 + 1, [high](x0, x1) = x0 + 1, [ifquick](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [isempty](x0) = x0, [quicksort](x0) = x0, [head](x0) = x0 + 1, [tail](x0) = x0, [true] = 1, [false] = 1, [0] = 1, [nil] = 1, [error] = 0, [b] = 0, [a] = 0, [c] = 0, [ge#](x0, x1) = x0 Strict: ge#(s x, s y) -> ge#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: a() -> c() 0 >= 0 a() -> b() 0 >= 0 tail cons(n, x) -> x 0 + 1x + 0n >= 1x tail nil() -> nil() 1 >= 1 head cons(n, x) -> n 1 + 1x + 0n >= 1n head nil() -> error() 2 >= 0 quicksort x -> ifquick(isempty x, x) 0 + 1x >= 1 + 2x isempty cons(n, x) -> false() 0 + 1x + 0n >= 1 isempty nil() -> true() 1 >= 1 ifquick(false(), x) -> append(quicksort low(head x, tail x), cons(tail x, quicksort high(head x, tail x))) 2 + 1x >= 2 + 1x ifquick(true(), x) -> nil() 2 + 1x >= 1 if_high(false(), n, cons(m, x)) -> high(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) 0 + 0x + 0n + 0m >= 1 + 1x + 0n + 0m high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) 1 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m high(n, nil()) -> nil() 2 + 0n >= 1 if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) 0 + 0x + 0n + 0m >= 1 + 1x + 0n + 0m if_low(true(), n, cons(m, x)) -> low(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) 1 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m low(n, nil()) -> nil() 2 + 0n >= 1 append(cons(n, x), y) -> cons(n, app(x, y)) 1 + 1x + 0y + 0n >= 0 + 0x + 0y + 0n append(nil(), y) -> y 2 + 0y >= 1y plus(0(), y) -> y 0 + 1y >= 1y plus(s x, y) -> s plus(x, y) 0 + 0x + 1y >= 1 + 0x + 1y ifIter(false(), x, y, z) -> averIter(plus(x, s s s 0()), plus(y, s 0()), plus(z, s 0())) 2 + 0x + 1y + 0z >= 2 + 0x + 0y + 0z ifIter(true(), x, y, z) -> z 2 + 0x + 1y + 0z >= 1z averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) 0 + 0x + 1y + 0z >= 2 + 0x + 2y + 0z average(x, y) -> if(ge(x, y), x, y) 0 + 0x + 0y >= 2 + 0x + 2y ge(0(), s y) -> false() 2 + 1y >= 1 ge(s x, s y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(x, 0()) -> true() 2 + 0x >= 1 if(false(), x, y) -> averIter(x, y, x) 2 + 0x + 1y >= 0 + 0x + 1y if(true(), x, y) -> averIter(y, x, y) 2 + 0x + 1y >= 0 + 1x + 0y Qed SCC (1): Strict: {plus#(s x, y) -> plus#(x, y)} Weak: { 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(), average(x, y) -> if(ge(x, y), x, y), 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), 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(), quicksort x -> ifquick(isempty x, x), head nil() -> error(), head cons(n, x) -> n, tail nil() -> nil(), tail cons(n, x) -> x, a() -> b(), a() -> c()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifIter](x0, x1, x2, x3) = x0 + x1 + 1, [if](x0, x1, x2) = x0 + x1 + 1, [averIter](x0, x1, x2) = x0, [if_low](x0, x1, x2) = 0, [if_high](x0, x1, x2) = 0, [ge](x0, x1) = x0 + 1, [average](x0, x1) = 0, [plus](x0, x1) = x0, [append](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + 1, [app](x0, x1) = 1, [low](x0, x1) = x0 + 1, [high](x0, x1) = x0 + 1, [ifquick](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [isempty](x0) = x0 + 1, [quicksort](x0) = x0 + 1, [head](x0) = x0 + 1, [tail](x0) = x0 + 1, [true] = 1, [false] = 1, [0] = 1, [nil] = 1, [error] = 0, [b] = 0, [a] = 0, [c] = 0, [plus#](x0, x1) = x0 Strict: plus#(s x, y) -> plus#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y Weak: a() -> c() 0 >= 0 a() -> b() 0 >= 0 tail cons(n, x) -> x 2 + 1x + 0n >= 1x tail nil() -> nil() 2 >= 1 head cons(n, x) -> n 2 + 1x + 0n >= 1n head nil() -> error() 2 >= 0 quicksort x -> ifquick(isempty x, x) 1 + 1x >= 2 + 2x isempty cons(n, x) -> false() 2 + 1x + 0n >= 1 isempty nil() -> true() 2 >= 1 ifquick(false(), x) -> append(quicksort low(head x, tail x), cons(tail x, quicksort high(head x, tail x))) 2 + 1x >= 4 + 1x ifquick(true(), x) -> nil() 2 + 1x >= 1 if_high(false(), n, cons(m, x)) -> high(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) 2 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m high(n, nil()) -> nil() 2 + 0n >= 1 if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m if_low(true(), n, cons(m, x)) -> low(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) 2 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m low(n, nil()) -> nil() 2 + 0n >= 1 append(cons(n, x), y) -> cons(n, app(x, y)) 2 + 1x + 0y + 0n >= 2 + 0x + 0y + 0n append(nil(), y) -> y 2 + 0y >= 1y plus(0(), y) -> y 0 + 1y >= 1y plus(s x, y) -> s plus(x, y) 0 + 0x + 1y >= 1 + 0x + 1y ifIter(false(), x, y, z) -> averIter(plus(x, s s s 0()), plus(y, s 0()), plus(z, s 0())) 2 + 0x + 1y + 0z >= 2 + 0x + 0y + 0z ifIter(true(), x, y, z) -> z 2 + 0x + 1y + 0z >= 1z averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) 0 + 0x + 1y + 0z >= 2 + 0x + 2y + 0z average(x, y) -> if(ge(x, y), x, y) 0 + 0x + 0y >= 2 + 0x + 2y ge(0(), s y) -> false() 2 + 1y >= 1 ge(s x, s y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(x, 0()) -> true() 2 + 0x >= 1 if(false(), x, y) -> averIter(x, y, x) 2 + 0x + 1y >= 0 + 0x + 1y if(true(), x, y) -> averIter(y, x, y) 2 + 0x + 1y >= 0 + 1x + 0y Qed