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