MAYBE Time: 1.027857 TRS: { app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)), app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs), app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)), app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x), app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x), app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)), app'(app'(minus(), x), 0()) -> x, app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y), app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))), app'(app'(quot(), 0()), app'(s(), y)) -> 0(), app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y), app'(app'(le(), app'(s(), x)), 0()) -> false(), app'(app'(le(), 0()), y) -> true(), app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)), app'(app'(app(), nil()), y) -> y, app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(low(), n), nil()) -> nil(), app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(high(), n), nil()) -> nil(), app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)), app'(app'(map(), f), nil()) -> nil(), app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'(app'(filter(), f), nil()) -> nil(), app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'(quicksort(), nil()) -> nil()} DP: DP: { app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(add(), x), app'(app'(filter(), f), xs)), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(add(), x), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(filter(), f), app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(filter(), f), app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(add(), m), app'(app'(low(), n), x)), app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(low(), n), app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(low(), n), app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(high(), n), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(add(), m), app'(app'(high(), n), x)), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(high(), n), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(quot(), app'(app'(minus(), x), y)), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(le(), x), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(app(), x), y), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), app'(app'(app(), x), y)), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app(), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(if_low(), app'(app'(le(), m), n)), n), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(le(), m), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(if_low(), app'(app'(le(), m), n)), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(if_high(), app'(app'(le(), m), n)), n), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(le(), m), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(if_high(), app'(app'(le(), m), n)), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(add(), app'(f, x)), app'(app'(map(), f), xs)), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(map(), f), xs), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(add(), app'(f, x)), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(filter2(), app'(f, x)), f), x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(filter2(), app'(f, x)), f), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(filter2(), app'(f, x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x))), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(low(), n), x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(high(), n), x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app(), app'(quicksort(), app'(app'(low(), n), x))), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(low(), n), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(high(), n), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x))} TRS: { app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)), app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs), app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)), app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x), app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x), app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)), app'(app'(minus(), x), 0()) -> x, app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y), app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))), app'(app'(quot(), 0()), app'(s(), y)) -> 0(), app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y), app'(app'(le(), app'(s(), x)), 0()) -> false(), app'(app'(le(), 0()), y) -> true(), app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)), app'(app'(app(), nil()), y) -> y, app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(low(), n), nil()) -> nil(), app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(high(), n), nil()) -> nil(), app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)), app'(app'(map(), f), nil()) -> nil(), app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'(app'(filter(), f), nil()) -> nil(), app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'(quicksort(), nil()) -> nil()} UR: { app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)), app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs), app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)), app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x), app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x), app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)), app'(app'(minus(), x), 0()) -> x, app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y), app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))), app'(app'(quot(), 0()), app'(s(), y)) -> 0(), app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y), app'(app'(le(), app'(s(), x)), 0()) -> false(), app'(app'(le(), 0()), y) -> true(), app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)), app'(app'(app(), nil()), y) -> y, app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(low(), n), nil()) -> nil(), app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(high(), n), nil()) -> nil(), app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)), app'(app'(map(), f), nil()) -> nil(), app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'(app'(filter(), f), nil()) -> nil(), app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'(quicksort(), nil()) -> nil(), a(z, w) -> z, a(z, w) -> w} EDG: { (app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(if_low(), app'(app'(le(), m), n))) (app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(le(), m)) (app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(if_low(), app'(app'(le(), m), n)), n)) (app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n)) (app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))) (app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(if_high(), app'(app'(le(), m), n))) (app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(le(), m)) (app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(if_high(), app'(app'(le(), m), n)), n)) (app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n)) (app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(if_low(), app'(app'(le(), m), n))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(le(), m)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(if_low(), app'(app'(le(), m), n)), n)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(high(), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(low(), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app(), app'(quicksort(), app'(app'(low(), n), x)))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(high(), n), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(low(), n), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x))))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(filter2(), app'(f, x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(filter2(), app'(f, x)), f)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(filter2(), app'(f, x)), f), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(add(), app'(f, x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(map(), f), xs)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(add(), app'(f, x)), app'(app'(map(), f), xs))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(if_high(), app'(app'(le(), m), n))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(le(), m)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(if_high(), app'(app'(le(), m), n)), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(if_low(), app'(app'(le(), m), n))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(le(), m)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(if_low(), app'(app'(le(), m), n)), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app(), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), app'(app'(app(), x), y))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(app(), x), y)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(le(), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(quot(), app'(app'(minus(), x), y))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(high(), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(add(), m), app'(app'(high(), n), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(high(), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(low(), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(low(), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(add(), m), app'(app'(low(), n), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(filter(), f)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(app'(filter(), f), xs)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(filter(), f)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(add(), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(filter(), f), xs)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(add(), x), app'(app'(filter(), f), xs))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app(), x)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), app'(app'(app(), x), y))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(app(), x), y)) (app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(low(), n)) (app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x)) (app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(low(), n)) (app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x)) (app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(add(), m), app'(app'(low(), n), x))) (app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(high(), n)) (app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x)) (app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(add(), m), app'(app'(high(), n), x))) (app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(high(), n)) (app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(high(), n)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(low(), n)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app(), app'(quicksort(), app'(app'(low(), n), x)))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(high(), n), x)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(low(), n), x)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x))))) (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x)) (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y)) (app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(app(), x), y), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app(), x)) (app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(app(), x), y), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), app'(app'(app(), x), y))) (app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(app(), x), y), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(app(), x), y)) (app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(filter2(), app'(f, x))) (app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(filter2(), app'(f, x)), f)) (app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(filter2(), app'(f, x)), f), x)) (app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs)) (app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(filter(), f)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(app'(filter(), f), xs)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(filter(), f)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(add(), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(filter(), f), xs)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(add(), x), app'(app'(filter(), f), xs))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(map(), f), xs), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(map(), f), xs), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(add(), app'(f, x)), app'(app'(map(), f), xs))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(map(), f), xs), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(map(), f), xs)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(map(), f), xs), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(add(), app'(f, x))) (app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x)) (app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs)) (app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(filter2(), app'(f, x)), f), x)) (app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(filter2(), app'(f, x)), f)) (app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(filter2(), app'(f, x))) (app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y)) (app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(le(), x)) (app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y)) (app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x))))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(low(), n), x)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(high(), n), x)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app(), app'(quicksort(), app'(app'(low(), n), x)))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(low(), n)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(high(), n)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x))) (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y)) (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))) (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x)) (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)))) (app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(quot(), app'(app'(minus(), x), y))) (app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y)) (app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(le(), x)) (app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y)) (app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(le(), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(add(), x), app'(app'(filter(), f), xs))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(filter(), f), xs)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(add(), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(filter(), f)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(app'(filter(), f), xs)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(filter(), f)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(add(), m), app'(app'(low(), n), x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(low(), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(low(), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(high(), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(add(), m), app'(app'(high(), n), x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(high(), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(minus(), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y)))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(quot(), app'(app'(minus(), x), y))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(le(), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(app(), x), y)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), app'(app'(app(), x), y))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app(), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(if_low(), app'(app'(le(), m), n)), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(le(), m)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(if_low(), app'(app'(le(), m), n))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(if_high(), app'(app'(le(), m), n)), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(le(), m)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(if_high(), app'(app'(le(), m), n))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(add(), app'(f, x)), app'(app'(map(), f), xs))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(map(), f), xs)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(add(), app'(f, x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(filter2(), app'(f, x)), f), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(filter2(), app'(f, x)), f)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(filter2(), app'(f, x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x))))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(low(), n), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(high(), n), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app(), app'(quicksort(), app'(app'(low(), n), x)))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(low(), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(high(), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(if_high(), app'(app'(le(), m), n)), n)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(le(), m)) (app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(if_high(), app'(app'(le(), m), n))) (app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))) (app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n)) (app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(if_high(), app'(app'(le(), m), n)), n)) (app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(le(), m)) (app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(if_high(), app'(app'(le(), m), n))) (app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))) (app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(le(), m), n)) (app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(if_low(), app'(app'(le(), m), n)), n)) (app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(le(), m)) (app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(if_low(), app'(app'(le(), m), n))) } STATUS: arrows: 0.932717 SCCS (8): Scc: { app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(map(), f), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs)} Scc: {app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x))} Scc: {app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(app(), x), y)} Scc: {app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))} Scc: {app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y)} Scc: { app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))} Scc: { app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))} Scc: {app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y)} SCC (6): Strict: { app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(app'(filter(), f), xs), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(map(), f), xs), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs)} Weak: { app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)), app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs), app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)), app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x), app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x), app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)), app'(app'(minus(), x), 0()) -> x, app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y), app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))), app'(app'(quot(), 0()), app'(s(), y)) -> 0(), app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y), app'(app'(le(), app'(s(), x)), 0()) -> false(), app'(app'(le(), 0()), y) -> true(), app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)), app'(app'(app(), nil()), y) -> y, app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(low(), n), nil()) -> nil(), app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(high(), n), nil()) -> nil(), app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)), app'(app'(map(), f), nil()) -> nil(), app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'(app'(filter(), f), nil()) -> nil(), app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'(quicksort(), nil()) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app'](x0, x1) = x0 + x1, [minus] = 1, [0] = 1, [s] = 1, [quot] = 0, [true] = 1, [le] = 0, [false] = 1, [app] = 0, [nil] = 0, [add] = 1, [low] = 0, [if_low] = 1, [high] = 0, [if_high] = 1, [quicksort] = 0, [map] = 0, [filter] = 0, [filter2] = 1, [app'#](x0, x1) = x0 Strict: app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(app'(app'(app'(filter2(), app'(f, x)), f), x), xs) 1 + 1x + 0f + 1xs >= 0 + 0x + 0f + 1xs app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x) 1 + 1x + 0f + 1xs >= 0 + 1x + 0f app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(app'(map(), f), xs) 1 + 1x + 0f + 1xs >= 0 + 0f + 1xs app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x) 1 + 1x + 0f + 1xs >= 0 + 1x + 0f app'#(app'(app'(app'(filter2(), false()), f), x), xs) -> app'#(app'(filter(), f), xs) 0 + 0x + 0f + 1xs >= 0 + 0f + 1xs app'#(app'(app'(app'(filter2(), true()), f), x), xs) -> app'#(app'(filter(), f), xs) 0 + 0x + 0f + 1xs >= 0 + 0f + 1xs Weak: app'(quicksort(), nil()) -> nil() 0 >= 0 app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))) 1 + 1x + 1n >= 1 + 2x + 3n app'(app'(filter(), f), nil()) -> nil() 0 + 1f >= 0 app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs) 1 + 1x + 1f + 1xs >= 1 + 2x + 2f + 1xs app'(app'(map(), f), nil()) -> nil() 0 + 1f >= 0 app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)) 1 + 1x + 1f + 1xs >= 1 + 1x + 2f + 1xs app'(app'(high(), n), nil()) -> nil() 0 + 1n >= 0 app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)) 1 + 1x + 1n + 1m >= 2 + 1x + 2n + 2m app'(app'(low(), n), nil()) -> nil() 0 + 1n >= 0 app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)) 1 + 1x + 1n + 1m >= 2 + 1x + 2n + 2m app'(app'(app(), nil()), y) -> y 0 + 1y >= 1y app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)) 1 + 1x + 1y + 1n >= 1 + 1x + 1y + 1n app'(app'(le(), 0()), y) -> true() 1 + 1y >= 1 app'(app'(le(), app'(s(), x)), 0()) -> false() 2 + 1x >= 1 app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y) 2 + 1x + 1y >= 0 + 1x + 1y app'(app'(quot(), 0()), app'(s(), y)) -> 0() 2 + 1y >= 1 app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))) 2 + 1x + 1y >= 3 + 1x + 2y app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y) 3 + 1x + 1y >= 1 + 1x + 1y app'(app'(minus(), x), 0()) -> x 2 + 1x >= 1x app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)) 3 + 1x + 1n + 1m >= 1 + 1x + 1n + 1m app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x) 3 + 1x + 1n + 1m >= 0 + 1x + 1n app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x) 3 + 1x + 1n + 1m >= 0 + 1x + 1n app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)) 3 + 1x + 1n + 1m >= 1 + 1x + 1n + 1m app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs) 2 + 1x + 1f + 1xs >= 0 + 1f + 1xs app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)) 2 + 1x + 1f + 1xs >= 1 + 1x + 1f + 1xs SCCS (0): SCC (2): Strict: {app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(low(), n), x)), app'#(quicksort(), app'(app'(add(), n), x)) -> app'#(quicksort(), app'(app'(high(), n), x))} Weak: { app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)), app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs), app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)), app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x), app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x), app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)), app'(app'(minus(), x), 0()) -> x, app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y), app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))), app'(app'(quot(), 0()), app'(s(), y)) -> 0(), app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y), app'(app'(le(), app'(s(), x)), 0()) -> false(), app'(app'(le(), 0()), y) -> true(), app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)), app'(app'(app(), nil()), y) -> y, app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(low(), n), nil()) -> nil(), app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(high(), n), nil()) -> nil(), app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)), app'(app'(map(), f), nil()) -> nil(), app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'(app'(filter(), f), nil()) -> nil(), app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'(quicksort(), nil()) -> nil()} Fail SCC (1): Strict: {app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(app(), x), y)} Weak: { app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)), app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs), app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)), app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x), app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x), app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)), app'(app'(minus(), x), 0()) -> x, app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y), app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))), app'(app'(quot(), 0()), app'(s(), y)) -> 0(), app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y), app'(app'(le(), app'(s(), x)), 0()) -> false(), app'(app'(le(), 0()), y) -> true(), app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)), app'(app'(app(), nil()), y) -> y, app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(low(), n), nil()) -> nil(), app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(high(), n), nil()) -> nil(), app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)), app'(app'(map(), f), nil()) -> nil(), app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'(app'(filter(), f), nil()) -> nil(), app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'(quicksort(), nil()) -> nil()} Fail SCC (1): Strict: {app'#(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'#(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))} Weak: { app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)), app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs), app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)), app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x), app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x), app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)), app'(app'(minus(), x), 0()) -> x, app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y), app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))), app'(app'(quot(), 0()), app'(s(), y)) -> 0(), app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y), app'(app'(le(), app'(s(), x)), 0()) -> false(), app'(app'(le(), 0()), y) -> true(), app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)), app'(app'(app(), nil()), y) -> y, app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(low(), n), nil()) -> nil(), app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(high(), n), nil()) -> nil(), app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)), app'(app'(map(), f), nil()) -> nil(), app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'(app'(filter(), f), nil()) -> nil(), app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'(quicksort(), nil()) -> nil()} Fail SCC (1): Strict: {app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y)} Weak: { app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)), app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs), app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)), app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x), app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x), app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)), app'(app'(minus(), x), 0()) -> x, app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y), app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))), app'(app'(quot(), 0()), app'(s(), y)) -> 0(), app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y), app'(app'(le(), app'(s(), x)), 0()) -> false(), app'(app'(le(), 0()), y) -> true(), app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)), app'(app'(app(), nil()), y) -> y, app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(low(), n), nil()) -> nil(), app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(high(), n), nil()) -> nil(), app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)), app'(app'(map(), f), nil()) -> nil(), app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'(app'(filter(), f), nil()) -> nil(), app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'(quicksort(), nil()) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app'](x0, x1) = x0 + x1, [minus] = 1, [0] = 1, [s] = 1, [quot] = 0, [true] = 0, [le] = 1, [false] = 0, [app] = 0, [nil] = 0, [add] = 0, [low] = 0, [if_low] = 0, [high] = 0, [if_high] = 0, [quicksort] = 1, [map] = 0, [filter] = 0, [filter2] = 0, [app'#](x0, x1) = x0 Strict: app'#(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'#(app'(minus(), x), y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: app'(quicksort(), nil()) -> nil() 1 >= 0 app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))) 1 + 1x + 1n >= 2 + 2x + 3n app'(app'(filter(), f), nil()) -> nil() 0 + 1f >= 0 app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs) 0 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs app'(app'(map(), f), nil()) -> nil() 0 + 1f >= 0 app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)) 0 + 1x + 1f + 1xs >= 0 + 1x + 2f + 1xs app'(app'(high(), n), nil()) -> nil() 0 + 1n >= 0 app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)) 0 + 1x + 1n + 1m >= 1 + 1x + 2n + 2m app'(app'(low(), n), nil()) -> nil() 0 + 1n >= 0 app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)) 0 + 1x + 1n + 1m >= 1 + 1x + 2n + 2m app'(app'(app(), nil()), y) -> y 0 + 1y >= 1y app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)) 0 + 1x + 1y + 1n >= 0 + 1x + 1y + 1n app'(app'(le(), 0()), y) -> true() 2 + 1y >= 0 app'(app'(le(), app'(s(), x)), 0()) -> false() 3 + 1x >= 0 app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y) 3 + 1x + 1y >= 1 + 1x + 1y app'(app'(quot(), 0()), app'(s(), y)) -> 0() 2 + 1y >= 1 app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))) 2 + 1x + 1y >= 3 + 1x + 2y app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y) 3 + 1x + 1y >= 1 + 1x + 1y app'(app'(minus(), x), 0()) -> x 2 + 1x >= 1x app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)) 0 + 1x + 1n + 1m >= 0 + 1x + 1n + 1m app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x) 0 + 1x + 1n + 1m >= 0 + 1x + 1n app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x) 0 + 1x + 1n + 1m >= 0 + 1x + 1n app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)) 0 + 1x + 1n + 1m >= 0 + 1x + 1n + 1m app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs) 0 + 1x + 1f + 1xs >= 0 + 1f + 1xs app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)) 0 + 1x + 1f + 1xs >= 0 + 1x + 1f + 1xs Qed SCC (3): Strict: { app'#(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(high(), n), x), app'#(app'(high(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))} Weak: { app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)), app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs), app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)), app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x), app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x), app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)), app'(app'(minus(), x), 0()) -> x, app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y), app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))), app'(app'(quot(), 0()), app'(s(), y)) -> 0(), app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y), app'(app'(le(), app'(s(), x)), 0()) -> false(), app'(app'(le(), 0()), y) -> true(), app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)), app'(app'(app(), nil()), y) -> y, app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(low(), n), nil()) -> nil(), app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(high(), n), nil()) -> nil(), app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)), app'(app'(map(), f), nil()) -> nil(), app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'(app'(filter(), f), nil()) -> nil(), app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'(quicksort(), nil()) -> nil()} Fail SCC (3): Strict: { app'#(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(low(), n), x), app'#(app'(low(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x))} Weak: { app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)), app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs), app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)), app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x), app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x), app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)), app'(app'(minus(), x), 0()) -> x, app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y), app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))), app'(app'(quot(), 0()), app'(s(), y)) -> 0(), app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y), app'(app'(le(), app'(s(), x)), 0()) -> false(), app'(app'(le(), 0()), y) -> true(), app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)), app'(app'(app(), nil()), y) -> y, app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(low(), n), nil()) -> nil(), app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(high(), n), nil()) -> nil(), app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)), app'(app'(map(), f), nil()) -> nil(), app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'(app'(filter(), f), nil()) -> nil(), app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'(quicksort(), nil()) -> nil()} Fail SCC (1): Strict: {app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y)} Weak: { app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)), app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs), app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)), app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x), app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x), app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)), app'(app'(minus(), x), 0()) -> x, app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y), app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))), app'(app'(quot(), 0()), app'(s(), y)) -> 0(), app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y), app'(app'(le(), app'(s(), x)), 0()) -> false(), app'(app'(le(), 0()), y) -> true(), app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)), app'(app'(app(), nil()), y) -> y, app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(low(), n), nil()) -> nil(), app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)), app'(app'(high(), n), nil()) -> nil(), app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)), app'(app'(map(), f), nil()) -> nil(), app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs), app'(app'(filter(), f), nil()) -> nil(), app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))), app'(quicksort(), nil()) -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app'](x0, x1) = x0 + x1, [minus] = 1, [0] = 1, [s] = 1, [quot] = 0, [true] = 0, [le] = 0, [false] = 0, [app] = 0, [nil] = 0, [add] = 0, [low] = 0, [if_low] = 0, [high] = 0, [if_high] = 0, [quicksort] = 0, [map] = 0, [filter] = 0, [filter2] = 0, [app'#](x0, x1) = x0 Strict: app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: app'(quicksort(), nil()) -> nil() 0 >= 0 app'(quicksort(), app'(app'(add(), n), x)) -> app'(app'(app(), app'(quicksort(), app'(app'(low(), n), x))), app'(app'(add(), n), app'(quicksort(), app'(app'(high(), n), x)))) 0 + 1x + 1n >= 0 + 2x + 3n app'(app'(filter(), f), nil()) -> nil() 0 + 1f >= 0 app'(app'(filter(), f), app'(app'(add(), x), xs)) -> app'(app'(app'(app'(filter2(), app'(f, x)), f), x), xs) 0 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs app'(app'(map(), f), nil()) -> nil() 0 + 1f >= 0 app'(app'(map(), f), app'(app'(add(), x), xs)) -> app'(app'(add(), app'(f, x)), app'(app'(map(), f), xs)) 0 + 1x + 1f + 1xs >= 0 + 1x + 2f + 1xs app'(app'(high(), n), nil()) -> nil() 0 + 1n >= 0 app'(app'(high(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_high(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)) 0 + 1x + 1n + 1m >= 0 + 1x + 2n + 2m app'(app'(low(), n), nil()) -> nil() 0 + 1n >= 0 app'(app'(low(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_low(), app'(app'(le(), m), n)), n), app'(app'(add(), m), x)) 0 + 1x + 1n + 1m >= 0 + 1x + 2n + 2m app'(app'(app(), nil()), y) -> y 0 + 1y >= 1y app'(app'(app(), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(app(), x), y)) 0 + 1x + 1y + 1n >= 0 + 1x + 1y + 1n app'(app'(le(), 0()), y) -> true() 1 + 1y >= 0 app'(app'(le(), app'(s(), x)), 0()) -> false() 2 + 1x >= 0 app'(app'(le(), app'(s(), x)), app'(s(), y)) -> app'(app'(le(), x), y) 2 + 1x + 1y >= 0 + 1x + 1y app'(app'(quot(), 0()), app'(s(), y)) -> 0() 2 + 1y >= 1 app'(app'(quot(), app'(s(), x)), app'(s(), y)) -> app'(s(), app'(app'(quot(), app'(app'(minus(), x), y)), app'(s(), y))) 2 + 1x + 1y >= 3 + 1x + 2y app'(app'(minus(), app'(s(), x)), app'(s(), y)) -> app'(app'(minus(), x), y) 3 + 1x + 1y >= 1 + 1x + 1y app'(app'(minus(), x), 0()) -> x 2 + 1x >= 1x app'(app'(app'(if_high(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(high(), n), x)) 0 + 1x + 1n + 1m >= 0 + 1x + 1n + 1m app'(app'(app'(if_high(), true()), n), app'(app'(add(), m), x)) -> app'(app'(high(), n), x) 0 + 1x + 1n + 1m >= 0 + 1x + 1n app'(app'(app'(if_low(), false()), n), app'(app'(add(), m), x)) -> app'(app'(low(), n), x) 0 + 1x + 1n + 1m >= 0 + 1x + 1n app'(app'(app'(if_low(), true()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(low(), n), x)) 0 + 1x + 1n + 1m >= 0 + 1x + 1n + 1m app'(app'(app'(app'(filter2(), false()), f), x), xs) -> app'(app'(filter(), f), xs) 0 + 1x + 1f + 1xs >= 0 + 1f + 1xs app'(app'(app'(app'(filter2(), true()), f), x), xs) -> app'(app'(add(), x), app'(app'(filter(), f), xs)) 0 + 1x + 1f + 1xs >= 0 + 1x + 1f + 1xs Qed