YES Time: 0.182138 TRS: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), low(n, nil()) -> nil(), low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)), if_low(true(), n, add(m, x)) -> add(m, low(n, x)), if_low(false(), n, add(m, x)) -> low(n, x), high(n, nil()) -> nil(), high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)), if_high(true(), n, add(m, x)) -> high(n, x), if_high(false(), n, add(m, x)) -> add(m, high(n, x)), quicksort nil() -> nil(), quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))} DP: DP: { minus#(s x, s y) -> minus#(x, y), quot#(s x, s y) -> minus#(x, y), quot#(s x, s y) -> quot#(minus(x, y), s y), le#(s x, s y) -> le#(x, y), app#(add(n, x), y) -> app#(x, y), low#(n, add(m, x)) -> le#(m, n), low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)), if_low#(true(), n, add(m, x)) -> low#(n, x), if_low#(false(), n, add(m, x)) -> low#(n, x), high#(n, add(m, x)) -> le#(m, n), high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)), if_high#(true(), n, add(m, x)) -> high#(n, x), if_high#(false(), n, add(m, x)) -> high#(n, x), quicksort# add(n, x) -> app#(quicksort low(n, x), add(n, quicksort high(n, x))), quicksort# add(n, x) -> low#(n, x), quicksort# add(n, x) -> high#(n, x), quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> quicksort# high(n, x)} TRS: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), low(n, nil()) -> nil(), low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)), if_low(true(), n, add(m, x)) -> add(m, low(n, x)), if_low(false(), n, add(m, x)) -> low(n, x), high(n, nil()) -> nil(), high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)), if_high(true(), n, add(m, x)) -> high(n, x), if_high(false(), n, add(m, x)) -> add(m, high(n, x)), quicksort nil() -> nil(), quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))} UR: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), low(n, nil()) -> nil(), low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)), if_low(true(), n, add(m, x)) -> add(m, low(n, x)), if_low(false(), n, add(m, x)) -> low(n, x), high(n, nil()) -> nil(), high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)), if_high(true(), n, add(m, x)) -> high(n, x), if_high(false(), n, add(m, x)) -> add(m, high(n, x)), quicksort nil() -> nil(), quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x))), a(z, w) -> z, a(z, w) -> w} EDG: {(high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)), if_high#(false(), n, add(m, x)) -> high#(n, x)) (high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)), if_high#(true(), n, add(m, x)) -> high#(n, x)) (low#(n, add(m, x)) -> le#(m, n), le#(s x, s y) -> le#(x, y)) (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y)) (if_low#(true(), n, add(m, x)) -> low#(n, x), low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x))) (if_low#(true(), n, add(m, x)) -> low#(n, x), low#(n, add(m, x)) -> le#(m, n)) (if_high#(true(), n, add(m, x)) -> high#(n, x), high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x))) (if_high#(true(), n, add(m, x)) -> high#(n, x), high#(n, add(m, x)) -> le#(m, n)) (quicksort# add(n, x) -> low#(n, x), low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x))) (quicksort# add(n, x) -> low#(n, x), low#(n, add(m, x)) -> le#(m, n)) (quicksort# add(n, x) -> app#(quicksort low(n, x), add(n, quicksort high(n, x))), app#(add(n, x), y) -> app#(x, y)) (quicksort# add(n, x) -> quicksort# high(n, x), quicksort# add(n, x) -> quicksort# high(n, x)) (quicksort# add(n, x) -> quicksort# high(n, x), quicksort# add(n, x) -> quicksort# low(n, x)) (quicksort# add(n, x) -> quicksort# high(n, x), quicksort# add(n, x) -> high#(n, x)) (quicksort# add(n, x) -> quicksort# high(n, x), quicksort# add(n, x) -> low#(n, x)) (quicksort# add(n, x) -> quicksort# high(n, x), quicksort# add(n, x) -> app#(quicksort low(n, x), add(n, quicksort high(n, x)))) (quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> app#(quicksort low(n, x), add(n, quicksort high(n, x)))) (quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> low#(n, x)) (quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> high#(n, x)) (quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> quicksort# low(n, x)) (quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> quicksort# high(n, x)) (quicksort# add(n, x) -> high#(n, x), high#(n, add(m, x)) -> le#(m, n)) (quicksort# add(n, x) -> high#(n, x), high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x))) (if_high#(false(), n, add(m, x)) -> high#(n, x), high#(n, add(m, x)) -> le#(m, n)) (if_high#(false(), n, add(m, x)) -> high#(n, x), high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x))) (if_low#(false(), n, add(m, x)) -> low#(n, x), low#(n, add(m, x)) -> le#(m, n)) (if_low#(false(), n, add(m, x)) -> low#(n, x), low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x))) (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y)) (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (high#(n, add(m, x)) -> le#(m, n), le#(s x, s y) -> le#(x, y)) (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y)) (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y)) (low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)), if_low#(true(), n, add(m, x)) -> low#(n, x)) (low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)), if_low#(false(), n, add(m, x)) -> low#(n, x))} STATUS: arrows: 0.891975 SCCS (7): Scc: {quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> quicksort# high(n, x)} Scc: {app#(add(n, x), y) -> app#(x, y)} Scc: {quot#(s x, s y) -> quot#(minus(x, y), s y)} Scc: {minus#(s x, s y) -> minus#(x, y)} Scc: { high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)), if_high#(true(), n, add(m, x)) -> high#(n, x), if_high#(false(), n, add(m, x)) -> high#(n, x)} Scc: { low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)), if_low#(true(), n, add(m, x)) -> low#(n, x), if_low#(false(), n, add(m, x)) -> low#(n, x)} Scc: {le#(s x, s y) -> le#(x, y)} SCC (2): Strict: {quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> quicksort# high(n, x)} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), low(n, nil()) -> nil(), low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)), if_low(true(), n, add(m, x)) -> add(m, low(n, x)), if_low(false(), n, add(m, x)) -> low(n, x), high(n, nil()) -> nil(), high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)), if_high(true(), n, add(m, x)) -> high(n, x), if_high(false(), n, add(m, x)) -> add(m, high(n, x)), quicksort nil() -> nil(), quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_low](x0, x1, x2) = x0 + 1, [if_high](x0, x1, x2) = x0, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [le](x0, x1) = 0, [app](x0, x1) = x0 + 1, [add](x0, x1) = x0 + 1, [low](x0, x1) = x0 + 1, [high](x0, x1) = x0, [s](x0) = 1, [quicksort](x0) = 0, [0] = 1, [true] = 0, [false] = 0, [nil] = 1, [quicksort#](x0) = x0 + 1 Strict: quicksort# add(n, x) -> quicksort# high(n, x) 2 + 1x + 0n >= 1 + 1x + 0n quicksort# add(n, x) -> quicksort# low(n, x) 2 + 1x + 0n >= 2 + 1x + 0n Weak: quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x))) 0 + 0x + 0n >= 1 + 0x + 0n quicksort nil() -> nil() 0 >= 1 if_high(false(), n, add(m, x)) -> add(m, high(n, x)) 1 + 1x + 0n + 0m >= 1 + 1x + 0n + 0m if_high(true(), n, add(m, x)) -> high(n, x) 1 + 1x + 0n + 0m >= 0 + 1x + 0n high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)) 1 + 1x + 0n + 0m >= 1 + 1x + 0n + 0m high(n, nil()) -> nil() 1 + 0n >= 1 if_low(false(), n, add(m, x)) -> low(n, x) 2 + 1x + 0n + 0m >= 1 + 1x + 0n if_low(true(), n, add(m, x)) -> add(m, low(n, x)) 2 + 1x + 0n + 0m >= 2 + 1x + 0n + 0m low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)) 2 + 1x + 0n + 0m >= 2 + 1x + 0n + 0m low(n, nil()) -> nil() 2 + 0n >= 1 app(add(n, x), y) -> add(n, app(x, y)) 2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n app(nil(), y) -> y 2 + 0y >= 1y le(s x, s y) -> le(x, y) 0 + 0x + 0y >= 0 + 0x + 0y le(s x, 0()) -> false() 0 + 0x >= 0 le(0(), y) -> true() 0 + 0y >= 0 quot(s x, s y) -> s quot(minus(x, y), s y) 2 + 0x + 0y >= 1 + 0x + 0y quot(0(), s y) -> 0() 2 + 0y >= 1 minus(s x, s y) -> minus(x, y) 2 + 0x + 0y >= 1 + 0x + 1y minus(x, 0()) -> x 2 + 0x >= 1x SCCS (1): Scc: {quicksort# add(n, x) -> quicksort# low(n, x)} SCC (1): Strict: {quicksort# add(n, x) -> quicksort# low(n, x)} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), low(n, nil()) -> nil(), low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)), if_low(true(), n, add(m, x)) -> add(m, low(n, x)), if_low(false(), n, add(m, x)) -> low(n, x), high(n, nil()) -> nil(), high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)), if_high(true(), n, add(m, x)) -> high(n, x), if_high(false(), n, add(m, x)) -> add(m, high(n, x)), quicksort nil() -> nil(), quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_low](x0, x1, x2) = x0, [if_high](x0, x1, x2) = x0 + x1, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + x1 + 1, [le](x0, x1) = x0, [app](x0, x1) = x0 + 1, [add](x0, x1) = x0 + x1 + 1, [low](x0, x1) = x0, [high](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [quicksort](x0) = x0, [0] = 0, [true] = 0, [false] = 0, [nil] = 1, [quicksort#](x0) = x0 + 1 Strict: quicksort# add(n, x) -> quicksort# low(n, x) 2 + 1x + 1n >= 1 + 1x + 0n Weak: quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x))) 1 + 1x + 1n >= 1 + 1x + 0n quicksort nil() -> nil() 1 >= 1 if_high(false(), n, add(m, x)) -> add(m, high(n, x)) 0 + 0x + 1n + 0m >= 2 + 1x + 0n + 1m if_high(true(), n, add(m, x)) -> high(n, x) 0 + 0x + 1n + 0m >= 1 + 1x + 0n high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)) 2 + 1x + 0n + 1m >= 0 + 0x + 2n + 0m high(n, nil()) -> nil() 2 + 0n >= 1 if_low(false(), n, add(m, x)) -> low(n, x) 1 + 1x + 0n + 1m >= 0 + 1x + 0n if_low(true(), n, add(m, x)) -> add(m, low(n, x)) 1 + 1x + 0n + 1m >= 1 + 1x + 0n + 1m low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)) 1 + 1x + 0n + 1m >= 1 + 1x + 0n + 1m low(n, nil()) -> nil() 1 + 0n >= 1 app(add(n, x), y) -> add(n, app(x, y)) 2 + 1x + 0y + 1n >= 2 + 1x + 0y + 1n app(nil(), y) -> y 2 + 0y >= 1y le(s x, s y) -> le(x, y) 1 + 0x + 1y >= 0 + 0x + 1y le(s x, 0()) -> false() 0 + 0x >= 0 le(0(), y) -> true() 0 + 1y >= 0 quot(s x, s y) -> s quot(minus(x, y), s y) 3 + 1x + 1y >= 4 + 0x + 2y quot(0(), s y) -> 0() 2 + 1y >= 0 minus(s x, s y) -> minus(x, y) 2 + 0x + 1y >= 1 + 0x + 1y minus(x, 0()) -> x 1 + 0x >= 1x Qed SCC (1): Strict: {app#(add(n, x), y) -> app#(x, y)} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), low(n, nil()) -> nil(), low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)), if_low(true(), n, add(m, x)) -> add(m, low(n, x)), if_low(false(), n, add(m, x)) -> low(n, x), high(n, nil()) -> nil(), high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)), if_high(true(), n, add(m, x)) -> high(n, x), if_high(false(), n, add(m, x)) -> add(m, high(n, x)), quicksort nil() -> nil(), quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_low](x0, x1, x2) = 0, [if_high](x0, x1, x2) = 0, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [le](x0, x1) = x0 + x1 + 1, [app](x0, x1) = x0 + x1 + 1, [add](x0, x1) = x0 + 1, [low](x0, x1) = x0 + 1, [high](x0, x1) = x0 + 1, [s](x0) = 0, [quicksort](x0) = x0 + 1, [0] = 1, [true] = 0, [false] = 0, [nil] = 1, [app#](x0, x1) = x0 Strict: app#(add(n, x), y) -> app#(x, y) 1 + 1x + 0y + 0n >= 0 + 1x + 0y Weak: quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x))) 2 + 1x + 0n >= 6 + 2x + 0n quicksort nil() -> nil() 2 >= 1 if_high(false(), n, add(m, x)) -> add(m, high(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m if_high(true(), n, add(m, x)) -> high(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)) 2 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m high(n, nil()) -> nil() 2 + 0n >= 1 if_low(false(), n, add(m, x)) -> low(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n if_low(true(), n, add(m, x)) -> add(m, low(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)) 2 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m low(n, nil()) -> nil() 2 + 0n >= 1 app(add(n, x), y) -> add(n, app(x, y)) 2 + 1x + 1y + 0n >= 2 + 1x + 1y + 0n app(nil(), y) -> y 2 + 1y >= 1y le(s x, s y) -> le(x, y) 1 + 0x + 0y >= 1 + 1x + 1y le(s x, 0()) -> false() 2 + 0x >= 0 le(0(), y) -> true() 2 + 1y >= 0 quot(s x, s y) -> s quot(minus(x, y), s y) 1 + 0x + 0y >= 0 + 0x + 0y quot(0(), s y) -> 0() 2 + 0y >= 1 minus(s x, s y) -> minus(x, y) 1 + 0x + 0y >= 1 + 0x + 1y minus(x, 0()) -> x 2 + 0x >= 1x Qed SCC (1): Strict: {quot#(s x, s y) -> quot#(minus(x, y), s y)} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), low(n, nil()) -> nil(), low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)), if_low(true(), n, add(m, x)) -> add(m, low(n, x)), if_low(false(), n, add(m, x)) -> low(n, x), high(n, nil()) -> nil(), high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)), if_high(true(), n, add(m, x)) -> high(n, x), if_high(false(), n, add(m, x)) -> add(m, high(n, x)), quicksort nil() -> nil(), quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_low](x0, x1, x2) = 0, [if_high](x0, x1, x2) = 1, [minus](x0, x1) = x0, [quot](x0, x1) = x0 + 1, [le](x0, x1) = x0 + 1, [app](x0, x1) = x0 + 1, [add](x0, x1) = x0 + 1, [low](x0, x1) = x0 + 1, [high](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [quicksort](x0) = 1, [0] = 1, [true] = 0, [false] = 0, [nil] = 1, [quot#](x0, x1) = x0 + 1 Strict: quot#(s x, s y) -> quot#(minus(x, y), s y) 2 + 1x + 0y >= 1 + 1x + 0y Weak: quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x))) 1 + 0x + 0n >= 2 + 0x + 0n quicksort nil() -> nil() 1 >= 1 if_high(false(), n, add(m, x)) -> add(m, high(n, x)) 1 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m if_high(true(), n, add(m, x)) -> high(n, x) 1 + 0x + 0n + 0m >= 1 + 1x + 0n high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)) 2 + 1x + 0n + 0m >= 1 + 0x + 0n + 0m high(n, nil()) -> nil() 2 + 0n >= 1 if_low(false(), n, add(m, x)) -> low(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n if_low(true(), n, add(m, x)) -> add(m, low(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)) 2 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m low(n, nil()) -> nil() 2 + 0n >= 1 app(add(n, x), y) -> add(n, app(x, y)) 2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n app(nil(), y) -> y 2 + 0y >= 1y le(s x, s y) -> le(x, y) 2 + 1x + 0y >= 1 + 1x + 0y le(s x, 0()) -> false() 2 + 1x >= 0 le(0(), y) -> true() 2 + 0y >= 0 quot(s x, s y) -> s quot(minus(x, y), s y) 2 + 0x + 1y >= 3 + 0x + 1y quot(0(), s y) -> 0() 2 + 1y >= 1 minus(s x, s y) -> minus(x, y) 1 + 1x + 0y >= 0 + 1x + 0y minus(x, 0()) -> x 0 + 1x >= 1x Qed SCC (1): Strict: {minus#(s x, s y) -> minus#(x, y)} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), low(n, nil()) -> nil(), low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)), if_low(true(), n, add(m, x)) -> add(m, low(n, x)), if_low(false(), n, add(m, x)) -> low(n, x), high(n, nil()) -> nil(), high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)), if_high(true(), n, add(m, x)) -> high(n, x), if_high(false(), n, add(m, x)) -> add(m, high(n, x)), quicksort nil() -> nil(), quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_low](x0, x1, x2) = 0, [if_high](x0, x1, x2) = 1, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [le](x0, x1) = x0 + 1, [app](x0, x1) = x0 + 1, [add](x0, x1) = x0 + 1, [low](x0, x1) = x0 + 1, [high](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [quicksort](x0) = x0 + 1, [0] = 1, [true] = 0, [false] = 0, [nil] = 1, [minus#](x0, x1) = x0 Strict: minus#(s x, s y) -> minus#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x))) 2 + 1x + 0n >= 3 + 1x + 0n quicksort nil() -> nil() 2 >= 1 if_high(false(), n, add(m, x)) -> add(m, high(n, x)) 1 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m if_high(true(), n, add(m, x)) -> high(n, x) 1 + 0x + 0n + 0m >= 1 + 1x + 0n high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)) 2 + 1x + 0n + 0m >= 1 + 0x + 0n + 0m high(n, nil()) -> nil() 2 + 0n >= 1 if_low(false(), n, add(m, x)) -> low(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n if_low(true(), n, add(m, x)) -> add(m, low(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)) 2 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m low(n, nil()) -> nil() 2 + 0n >= 1 app(add(n, x), y) -> add(n, app(x, y)) 2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n app(nil(), y) -> y 2 + 0y >= 1y le(s x, s y) -> le(x, y) 2 + 1x + 0y >= 1 + 1x + 0y le(s x, 0()) -> false() 2 + 1x >= 0 le(0(), y) -> true() 2 + 0y >= 0 quot(s x, s y) -> s quot(minus(x, y), s y) 2 + 0x + 1y >= 3 + 0x + 1y quot(0(), s y) -> 0() 2 + 1y >= 1 minus(s x, s y) -> minus(x, y) 2 + 0x + 1y >= 1 + 0x + 1y minus(x, 0()) -> x 2 + 0x >= 1x Qed SCC (3): Strict: { high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)), if_high#(true(), n, add(m, x)) -> high#(n, x), if_high#(false(), n, add(m, x)) -> high#(n, x)} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), low(n, nil()) -> nil(), low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)), if_low(true(), n, add(m, x)) -> add(m, low(n, x)), if_low(false(), n, add(m, x)) -> low(n, x), high(n, nil()) -> nil(), high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)), if_high(true(), n, add(m, x)) -> high(n, x), if_high(false(), n, add(m, x)) -> add(m, high(n, x)), quicksort nil() -> nil(), quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_low](x0, x1, x2) = 0, [if_high](x0, x1, x2) = 1, [minus](x0, x1) = 0, [quot](x0, x1) = x0 + x1, [le](x0, x1) = 0, [app](x0, x1) = 0, [add](x0, x1) = x0 + 1, [low](x0, x1) = x0 + 1, [high](x0, x1) = 0, [s](x0) = 1, [quicksort](x0) = x0 + 1, [0] = 0, [true] = 0, [false] = 0, [nil] = 1, [if_high#](x0, x1, x2) = x0, [high#](x0, x1) = x0 Strict: if_high#(false(), n, add(m, x)) -> high#(n, x) 1 + 1x + 0n + 0m >= 0 + 1x + 0n if_high#(true(), n, add(m, x)) -> high#(n, x) 1 + 1x + 0n + 0m >= 0 + 1x + 0n high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)) 1 + 1x + 0n + 0m >= 1 + 1x + 0n + 0m Weak: quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x))) 2 + 1x + 0n >= 0 + 0x + 0n quicksort nil() -> nil() 2 >= 1 if_high(false(), n, add(m, x)) -> add(m, high(n, x)) 1 + 0x + 0n + 0m >= 1 + 0x + 0n + 0m if_high(true(), n, add(m, x)) -> high(n, x) 1 + 0x + 0n + 0m >= 0 + 0x + 0n high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)) 0 + 0x + 0n + 0m >= 1 + 0x + 0n + 0m high(n, nil()) -> nil() 0 + 0n >= 1 if_low(false(), n, add(m, x)) -> low(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n if_low(true(), n, add(m, x)) -> add(m, low(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)) 2 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m low(n, nil()) -> nil() 2 + 0n >= 1 app(add(n, x), y) -> add(n, app(x, y)) 0 + 0x + 0y + 0n >= 1 + 0x + 0y + 0n app(nil(), y) -> y 0 + 0y >= 1y le(s x, s y) -> le(x, y) 0 + 0x + 0y >= 0 + 0x + 0y le(s x, 0()) -> false() 0 + 0x >= 0 le(0(), y) -> true() 0 + 0y >= 0 quot(s x, s y) -> s quot(minus(x, y), s y) 2 + 0x + 0y >= 1 + 0x + 0y quot(0(), s y) -> 0() 1 + 0y >= 0 minus(s x, s y) -> minus(x, y) 0 + 0x + 0y >= 0 + 0x + 0y minus(x, 0()) -> x 0 + 0x >= 1x SCCS (0): SCC (3): Strict: { low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)), if_low#(true(), n, add(m, x)) -> low#(n, x), if_low#(false(), n, add(m, x)) -> low#(n, x)} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), low(n, nil()) -> nil(), low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)), if_low(true(), n, add(m, x)) -> add(m, low(n, x)), if_low(false(), n, add(m, x)) -> low(n, x), high(n, nil()) -> nil(), high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)), if_high(true(), n, add(m, x)) -> high(n, x), if_high(false(), n, add(m, x)) -> add(m, high(n, x)), quicksort nil() -> nil(), quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_low](x0, x1, x2) = 0, [if_high](x0, x1, x2) = 1, [minus](x0, x1) = 0, [quot](x0, x1) = x0 + x1, [le](x0, x1) = 0, [app](x0, x1) = 0, [add](x0, x1) = x0 + 1, [low](x0, x1) = x0 + 1, [high](x0, x1) = 0, [s](x0) = 1, [quicksort](x0) = x0 + 1, [0] = 0, [true] = 0, [false] = 0, [nil] = 1, [if_low#](x0, x1, x2) = x0, [low#](x0, x1) = x0 Strict: if_low#(false(), n, add(m, x)) -> low#(n, x) 1 + 1x + 0n + 0m >= 0 + 1x + 0n if_low#(true(), n, add(m, x)) -> low#(n, x) 1 + 1x + 0n + 0m >= 0 + 1x + 0n low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)) 1 + 1x + 0n + 0m >= 1 + 1x + 0n + 0m Weak: quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x))) 2 + 1x + 0n >= 0 + 0x + 0n quicksort nil() -> nil() 2 >= 1 if_high(false(), n, add(m, x)) -> add(m, high(n, x)) 1 + 0x + 0n + 0m >= 1 + 0x + 0n + 0m if_high(true(), n, add(m, x)) -> high(n, x) 1 + 0x + 0n + 0m >= 0 + 0x + 0n high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)) 0 + 0x + 0n + 0m >= 1 + 0x + 0n + 0m high(n, nil()) -> nil() 0 + 0n >= 1 if_low(false(), n, add(m, x)) -> low(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n if_low(true(), n, add(m, x)) -> add(m, low(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)) 2 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m low(n, nil()) -> nil() 2 + 0n >= 1 app(add(n, x), y) -> add(n, app(x, y)) 0 + 0x + 0y + 0n >= 1 + 0x + 0y + 0n app(nil(), y) -> y 0 + 0y >= 1y le(s x, s y) -> le(x, y) 0 + 0x + 0y >= 0 + 0x + 0y le(s x, 0()) -> false() 0 + 0x >= 0 le(0(), y) -> true() 0 + 0y >= 0 quot(s x, s y) -> s quot(minus(x, y), s y) 2 + 0x + 0y >= 1 + 0x + 0y quot(0(), s y) -> 0() 1 + 0y >= 0 minus(s x, s y) -> minus(x, y) 0 + 0x + 0y >= 0 + 0x + 0y minus(x, 0()) -> x 0 + 0x >= 1x SCCS (0): SCC (1): Strict: {le#(s x, s y) -> le#(x, y)} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), low(n, nil()) -> nil(), low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)), if_low(true(), n, add(m, x)) -> add(m, low(n, x)), if_low(false(), n, add(m, x)) -> low(n, x), high(n, nil()) -> nil(), high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)), if_high(true(), n, add(m, x)) -> high(n, x), if_high(false(), n, add(m, x)) -> add(m, high(n, x)), quicksort nil() -> nil(), quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_low](x0, x1, x2) = 0, [if_high](x0, x1, x2) = 1, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [le](x0, x1) = x0 + 1, [app](x0, x1) = x0 + 1, [add](x0, x1) = x0 + 1, [low](x0, x1) = x0 + 1, [high](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [quicksort](x0) = x0 + 1, [0] = 1, [true] = 0, [false] = 0, [nil] = 1, [le#](x0, x1) = x0 Strict: le#(s x, s y) -> le#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x))) 2 + 1x + 0n >= 3 + 1x + 0n quicksort nil() -> nil() 2 >= 1 if_high(false(), n, add(m, x)) -> add(m, high(n, x)) 1 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m if_high(true(), n, add(m, x)) -> high(n, x) 1 + 0x + 0n + 0m >= 1 + 1x + 0n high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)) 2 + 1x + 0n + 0m >= 1 + 0x + 0n + 0m high(n, nil()) -> nil() 2 + 0n >= 1 if_low(false(), n, add(m, x)) -> low(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n if_low(true(), n, add(m, x)) -> add(m, low(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)) 2 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m low(n, nil()) -> nil() 2 + 0n >= 1 app(add(n, x), y) -> add(n, app(x, y)) 2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n app(nil(), y) -> y 2 + 0y >= 1y le(s x, s y) -> le(x, y) 2 + 1x + 0y >= 1 + 1x + 0y le(s x, 0()) -> false() 2 + 1x >= 0 le(0(), y) -> true() 2 + 0y >= 0 quot(s x, s y) -> s quot(minus(x, y), s y) 2 + 0x + 1y >= 3 + 0x + 1y quot(0(), s y) -> 0() 2 + 1y >= 1 minus(s x, s y) -> minus(x, y) 2 + 0x + 1y >= 1 + 0x + 1y minus(x, 0()) -> x 2 + 0x >= 1x Qed