MAYBE Time: 0.153024 TRS: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), y)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(min(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z)), app(app(min(), x), nil()) -> x, app(app(del(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z))), app(app(del(), x), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(map(), f), nil()) -> nil(), app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs), app(app(filter(), f), nil()) -> nil(), app(minsort(), app(app(cons(), x), y)) -> app(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))), app(minsort(), nil()) -> nil()} DP: DP: { app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), 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#(cons(), 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(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(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(eq(), x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z)), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(le(), x), y), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(le(), x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(if(), app(app(le(), x), y)), app#(app(min(), x), app(app(cons(), y), z)) -> app#(min(), y), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z))), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(eq(), x), y), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(if(), app(app(eq(), x), y)), z), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(cons(), y), app(app(del(), x), z)), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z), app#(app(del(), x), app(app(cons(), y), z)) -> app#(eq(), x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(if(), app(app(eq(), x), y)), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs)), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x)), app#(minsort(), app(app(cons(), x), y)) -> app#(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))), app#(minsort(), app(app(cons(), x), y)) -> app#(app(min(), x), y), app#(minsort(), app(app(cons(), x), y)) -> app#(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)), app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))), app#(minsort(), app(app(cons(), x), y)) -> app#(cons(), app(app(min(), x), y)), app#(minsort(), app(app(cons(), x), y)) -> app#(min(), x), app#(minsort(), app(app(cons(), x), y)) -> app#(del(), app(app(min(), x), y))} TRS: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), y)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(min(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z)), app(app(min(), x), nil()) -> x, app(app(del(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z))), app(app(del(), x), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(map(), f), nil()) -> nil(), app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs), app(app(filter(), f), nil()) -> nil(), app(minsort(), app(app(cons(), x), y)) -> app(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))), app(minsort(), nil()) -> nil()} UR: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), y)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(min(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z)), app(app(min(), x), nil()) -> x, app(app(del(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z))), app(app(del(), x), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(map(), f), nil()) -> nil(), app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs), app(app(filter(), f), nil()) -> nil(), app(minsort(), app(app(cons(), x), y)) -> app(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))), app(minsort(), nil()) -> nil(), a(w, v) -> w, a(w, v) -> v} EDG: { (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(del(), app(app(min(), x), y))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(min(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(cons(), app(app(min(), x), y))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(app(min(), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(if(), app(app(eq(), x), y))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(eq(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(cons(), y), app(app(del(), x), z))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(if(), app(app(eq(), x), y)), z)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(eq(), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z)))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(min(), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(if(), app(app(le(), x), y))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(le(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(if(), app(app(le(), x), y)), app(app(min(), x), z))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(le(), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(eq(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x)) (app#(app(filter(), f), app(app(cons(), 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(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), f)) (app#(app(filter(), f), app(app(cons(), 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(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x)) (app#(app(filter(), f), app(app(cons(), 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(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs))) (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(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(min(), x), app(app(cons(), y), z)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x)) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(le(), x), y), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(app(le(), x), y)) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(min(), x), y), app#(app(min(), x), app(app(cons(), y), z)) -> app#(min(), y)) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(min(), x), y), app#(app(min(), x), app(app(cons(), y), z)) -> app#(if(), app(app(le(), x), y))) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(min(), x), y), app#(app(min(), x), app(app(cons(), y), z)) -> app#(le(), x)) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(min(), x), y), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z)) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(min(), x), y), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z)) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(min(), x), y), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(if(), app(app(le(), x), y)), app(app(min(), x), z))) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(min(), x), y), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(le(), x), y)) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(min(), x), y), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z))) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)), app#(app(del(), x), app(app(cons(), y), z)) -> app#(if(), app(app(eq(), x), y))) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)), app#(app(del(), x), app(app(cons(), y), z)) -> app#(eq(), x)) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z)) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(cons(), y), app(app(del(), x), z))) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(if(), app(app(eq(), x), y)), z)) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(eq(), x), y)) (app#(minsort(), app(app(cons(), x), y)) -> app#(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z)))) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(min(), y)) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(if(), app(app(le(), x), y))) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(le(), x)) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z)) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z)) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(if(), app(app(le(), x), y)), app(app(min(), x), z))) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(le(), x), y)) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z))) (app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z), app#(app(del(), x), app(app(cons(), y), z)) -> app#(if(), app(app(eq(), x), y))) (app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z), app#(app(del(), x), app(app(cons(), y), z)) -> app#(eq(), x)) (app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z)) (app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(cons(), y), app(app(del(), x), z))) (app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(if(), app(app(eq(), x), y)), z)) (app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(eq(), x), y)) (app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z)))) (app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), 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(cons(), 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(cons(), 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(cons(), 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(cons(), x), xs)) -> app#(f, x)) (app#(app(filter(), f), app(app(cons(), 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(cons(), 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(cons(), 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(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x)) (app#(app(filter(), f), app(app(cons(), 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(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x))) (app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), 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(cons(), 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(cons(), 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(cons(), 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(cons(), x), xs)) -> app#(filter2(), app(f, x))) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z))) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(le(), x), y)) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(if(), app(app(le(), x), y)), app(app(min(), x), z))) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z)) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z)) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(le(), x)) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(if(), app(app(le(), x), y))) (app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(min(), y)) (app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(eq(), x), y), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y)) (app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(eq(), x), y), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(eq(), x)) (app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y)) (app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(eq(), x)) (app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))), app#(minsort(), app(app(cons(), x), y)) -> app#(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))))) (app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))), app#(minsort(), app(app(cons(), x), y)) -> app#(app(min(), x), y)) (app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))), app#(minsort(), app(app(cons(), x), y)) -> app#(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))) (app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))), app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))) (app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))), app#(minsort(), app(app(cons(), x), y)) -> app#(cons(), app(app(min(), x), y))) (app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))), app#(minsort(), app(app(cons(), x), y)) -> app#(min(), x)) (app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))), app#(minsort(), app(app(cons(), x), y)) -> app#(del(), app(app(min(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs))) (app#(app(map(), f), app(app(cons(), 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(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f)) (app#(app(map(), f), app(app(cons(), 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(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), f)) (app#(app(map(), f), app(app(cons(), 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(cons(), x), xs)) -> app#(f, x), app#(app(le(), app(s(), x)), app(s(), y)) -> app#(le(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(eq(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(le(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(if(), app(app(le(), x), y)), app(app(min(), x), z))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(le(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(if(), app(app(le(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(min(), x), app(app(cons(), y), z)) -> app#(min(), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(eq(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(if(), app(app(eq(), x), y)), z)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(cons(), y), app(app(del(), x), z))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(eq(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(del(), x), app(app(cons(), y), z)) -> app#(if(), app(app(eq(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(app(min(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(app(del(), app(app(min(), x), y)), app(app(cons(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(cons(), app(app(min(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(min(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(minsort(), app(app(cons(), x), y)) -> app#(del(), app(app(min(), x), y))) } STATUS: arrows: 0.907793 SCCS (6): 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(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs)} Scc: {app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))} Scc: {app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z)} Scc: {app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z)} Scc: {app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y)} 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(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), 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(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), y)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(min(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z)), app(app(min(), x), nil()) -> x, app(app(del(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z))), app(app(del(), x), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(map(), f), nil()) -> nil(), app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs), app(app(filter(), f), nil()) -> nil(), app(minsort(), app(app(cons(), x), y)) -> app(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))), app(minsort(), nil()) -> nil()} Open SCC (1): Strict: {app#(minsort(), app(app(cons(), x), y)) -> app#(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))} Weak: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), y)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(min(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z)), app(app(min(), x), nil()) -> x, app(app(del(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z))), app(app(del(), x), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(map(), f), nil()) -> nil(), app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs), app(app(filter(), f), nil()) -> nil(), app(minsort(), app(app(cons(), x), y)) -> app(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))), app(minsort(), nil()) -> nil()} Open SCC (1): Strict: {app#(app(del(), x), app(app(cons(), y), z)) -> app#(app(del(), x), z)} Weak: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), y)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(min(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z)), app(app(min(), x), nil()) -> x, app(app(del(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z))), app(app(del(), x), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(map(), f), nil()) -> nil(), app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs), app(app(filter(), f), nil()) -> nil(), app(minsort(), app(app(cons(), x), y)) -> app(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))), app(minsort(), nil()) -> nil()} Open SCC (2): Strict: {app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), y), z), app#(app(min(), x), app(app(cons(), y), z)) -> app#(app(min(), x), z)} Weak: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), y)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(min(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z)), app(app(min(), x), nil()) -> x, app(app(del(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z))), app(app(del(), x), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(map(), f), nil()) -> nil(), app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs), app(app(filter(), f), nil()) -> nil(), app(minsort(), app(app(cons(), x), y)) -> app(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))), app(minsort(), nil()) -> nil()} Open SCC (1): Strict: {app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y)} Weak: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), y)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(min(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z)), app(app(min(), x), nil()) -> x, app(app(del(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z))), app(app(del(), x), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(map(), f), nil()) -> nil(), app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs), app(app(filter(), f), nil()) -> nil(), app(minsort(), app(app(cons(), x), y)) -> app(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))), app(minsort(), nil()) -> nil()} Open 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(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), y)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(min(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(le(), x), y)), app(app(min(), x), z)), app(app(min(), y), z)), app(app(min(), x), nil()) -> x, app(app(del(), x), app(app(cons(), y), z)) -> app(app(app(if(), app(app(eq(), x), y)), z), app(app(cons(), y), app(app(del(), x), z))), app(app(del(), x), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(map(), f), nil()) -> nil(), app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs), app(app(filter(), f), nil()) -> nil(), app(minsort(), app(app(cons(), x), y)) -> app(app(cons(), app(app(min(), x), y)), app(minsort(), app(app(del(), app(app(min(), x), y)), app(app(cons(), x), y)))), app(minsort(), nil()) -> nil()} Open