MAYBE Time: 0.526231 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_rm(), true()), n), app'(app'(add(), m), x)) -> app'(app'(rm(), n), x), app'(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(rm(), n), x)), app'(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())), app'(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'(app'(minsort(), x), app'(app'(add(), n), y)), 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(), x)) -> false(), app'(app'(eq(), 0()), 0()) -> true(), 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'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), n), x)), app'(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), m), x)), app'(app'(rm(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'(app'(rm(), n), nil()) -> nil(), app'(app'(minsort(), app'(app'(add(), n), x)), y) -> app'(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'(app'(minsort(), nil()), 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'(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'(min(), app'(app'(add(), n), nil())) -> n} 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_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(rm(), n), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(add(), m), app'(app'(rm(), n), x)), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(rm(), n), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(app(), app'(app'(rm(), n), x)), y), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(rm(), n), x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil()), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app(), app'(app'(rm(), n), x)), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(rm(), n), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), y), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), x), app'(app'(add(), n), y)), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(minsort(), 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'(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'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(add(), n), x), app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), n), x)), app'#(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), m), x)), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(eq(), n), m), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(if_rm(), app'(app'(eq(), n), m)), n), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(eq(), n), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(if_rm(), app'(app'(eq(), n), m)), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(eq(), n), app'(min(), app'(app'(add(), n), x))), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(eq(), n), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(min(), app'(app'(add(), n), x)), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), 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'#(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'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(le(), n), m), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(le(), n), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(if_min(), app'(app'(le(), n), m))} 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_rm(), true()), n), app'(app'(add(), m), x)) -> app'(app'(rm(), n), x), app'(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(rm(), n), x)), app'(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())), app'(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'(app'(minsort(), x), app'(app'(add(), n), y)), 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(), x)) -> false(), app'(app'(eq(), 0()), 0()) -> true(), 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'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), n), x)), app'(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), m), x)), app'(app'(rm(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'(app'(rm(), n), nil()) -> nil(), app'(app'(minsort(), app'(app'(add(), n), x)), y) -> app'(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'(app'(minsort(), nil()), 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'(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'(min(), app'(app'(add(), n), nil())) -> n} 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_rm(), true()), n), app'(app'(add(), m), x)) -> app'(app'(rm(), n), x), app'(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(rm(), n), x)), app'(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())), app'(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'(app'(minsort(), x), app'(app'(add(), n), y)), 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(), x)) -> false(), app'(app'(eq(), 0()), 0()) -> true(), 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'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), n), x)), app'(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), m), x)), app'(app'(rm(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'(app'(rm(), n), nil()) -> nil(), app'(app'(minsort(), app'(app'(add(), n), x)), y) -> app'(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'(app'(minsort(), nil()), 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'(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'(min(), app'(app'(add(), n), nil())) -> n, a(z, w) -> z, a(z, w) -> w} EDG: { (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'(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'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(minsort(), x)) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), x), app'(app'(add(), n), y))) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), y)) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y))) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(rm(), n)) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app(), app'(app'(rm(), n), x))) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(rm(), n), x)) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil()))) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(app(), app'(app'(rm(), n), x)), y)) (app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), x), app'(app'(add(), n), y)), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x))))) (app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), x), app'(app'(add(), n), y)), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(min(), app'(app'(add(), n), x))) (app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), x), app'(app'(add(), n), y)), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(eq(), n)) (app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), x), app'(app'(add(), n), y)), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x))) (app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), x), app'(app'(add(), n), y)), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))) (app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), x), app'(app'(add(), n), y)), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y)) (app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), n), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(if_min(), app'(app'(le(), n), m))) (app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), n), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(le(), n)) (app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), n), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x)))) (app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), n), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(le(), n), m)) (app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(rm(), n)) (app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x)) (app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(add(), m), app'(app'(rm(), n), x))) (app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(rm(), n)) (app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x)) (app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(if_rm(), app'(app'(eq(), n), m))) (app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(eq(), n)) (app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(if_rm(), app'(app'(eq(), n), m)), n)) (app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(eq(), n), m)) (app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x))) (app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(if_rm(), app'(app'(eq(), n), m))) (app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(eq(), n)) (app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(if_rm(), app'(app'(eq(), n), m)), n)) (app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(eq(), n), m)) (app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x))) (app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(eq(), n), m), app'#(app'(eq(), app'(s(), x)), app'(s(), y)) -> app'#(eq(), x)) (app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(eq(), n), m), app'#(app'(eq(), app'(s(), x)), app'(s(), y)) -> app'#(app'(eq(), x), y)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(if_min(), app'(app'(le(), n), m))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(le(), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x)))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(le(), n), m)) (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'#(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'#(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'(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'#(f, x)) (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'(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'(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'#(f, x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x))))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(min(), app'(app'(add(), n), x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(eq(), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(if_rm(), app'(app'(eq(), n), m))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(eq(), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(if_rm(), app'(app'(eq(), n), m)), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(eq(), n), m)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), m), x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), n), x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(add(), n), x)) (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'(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'(app(), 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'(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'(eq(), app'(s(), x)), app'(s(), y)) -> app'#(eq(), x)) (app'#(app'(map(), f), app'(app'(add(), 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'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(minsort(), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), x), app'(app'(add(), n), y))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), y)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(rm(), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app(), app'(app'(rm(), n), x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(rm(), n), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil()))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(app(), app'(app'(rm(), n), x)), y)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(rm(), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(add(), m), app'(app'(rm(), n), x))) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(rm(), n)) (app'#(app'(map(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x)) (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'(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(), true()), f), x), xs) -> app'#(filter(), f)) (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'#(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'(add(), x), 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'#(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'#(add(), x)) (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(), 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(), false()), f), x), xs) -> app'#(filter(), f)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(rm(), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(add(), m), app'(app'(rm(), n), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(rm(), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(app(), app'(app'(rm(), n), x)), y)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil()))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(rm(), n), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app(), app'(app'(rm(), n), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(rm(), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), y)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), x), app'(app'(add(), n), y))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(minsort(), x)) (app'#(app'(filter(), f), app'(app'(add(), 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'(add(), x), xs)) -> app'#(f, x), app'#(app'(eq(), app'(s(), x)), app'(s(), y)) -> app'#(eq(), 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'(le(), app'(s(), x)), app'(s(), y)) -> app'#(le(), x)) (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'(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(), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(add(), n), x)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), n), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), m), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(eq(), n), m)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(if_rm(), app'(app'(eq(), n), m)), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(eq(), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(if_rm(), app'(app'(eq(), n), m))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(eq(), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(min(), app'(app'(add(), n), x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), 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'#(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'#(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'#(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'#(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'#(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'(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'#(filter2(), app'(f, x))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(le(), n), m)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x)))) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(le(), n)) (app'#(app'(filter(), f), app'(app'(add(), x), xs)) -> app'#(f, x), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(if_min(), app'(app'(le(), n), m))) (app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(le(), n), m), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y)) (app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(le(), n), m), app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(le(), x)) (app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x))) (app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(eq(), n), m)) (app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(if_rm(), app'(app'(eq(), n), m)), n)) (app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(eq(), n)) (app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(if_rm(), app'(app'(eq(), n), m))) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(min(), app'(app'(add(), n), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(le(), n), m)) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(min(), app'(app'(add(), n), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x)))) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(min(), app'(app'(add(), n), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(le(), n)) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(min(), app'(app'(add(), n), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(if_min(), app'(app'(le(), n), m))) (app'#(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), m), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(le(), n), m)) (app'#(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), m), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x)))) (app'#(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), m), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(le(), n)) (app'#(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), m), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(if_min(), app'(app'(le(), n), m))) (app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(add(), n), x)) (app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), n), x))) (app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'#(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), m), x))) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(eq(), n), app'(min(), app'(app'(add(), n), x))), app'#(app'(eq(), app'(s(), x)), app'(s(), y)) -> app'#(app'(eq(), x), y)) (app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(eq(), n), app'(min(), app'(app'(add(), n), x))), app'#(app'(eq(), app'(s(), x)), app'(s(), y)) -> app'#(eq(), 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'(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'(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(), 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'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(app(), app'(app'(rm(), n), x)), y), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(app(), x), y)) (app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(app(), app'(app'(rm(), n), x)), y), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(add(), n), app'(app'(app(), x), y))) (app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(app(), app'(app'(rm(), n), x)), y), app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app(), 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'#(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'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil()), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y)) (app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil()), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))) (app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil()), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x))) (app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil()), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(eq(), n)) (app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil()), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(min(), app'(app'(add(), n), x))) (app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil()), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x))))) } STATUS: arrows: 0.932893 SCCS (7): 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'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil()), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), x), app'(app'(add(), n), y)), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y)} Scc: { app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), n), x)), app'#(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), m), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x)))} Scc: {app'#(app'(le(), app'(s(), x)), app'(s(), y)) -> app'#(app'(le(), x), y)} Scc: { app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x))} Scc: {app'#(app'(eq(), app'(s(), x)), app'(s(), y)) -> app'#(app'(eq(), x), y)} Scc: {app'#(app'(app(), app'(app'(add(), n), x)), y) -> app'#(app'(app(), 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_rm(), true()), n), app'(app'(add(), m), x)) -> app'(app'(rm(), n), x), app'(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(rm(), n), x)), app'(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())), app'(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'(app'(minsort(), x), app'(app'(add(), n), y)), 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(), x)) -> false(), app'(app'(eq(), 0()), 0()) -> true(), 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'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), n), x)), app'(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), m), x)), app'(app'(rm(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'(app'(rm(), n), nil()) -> nil(), app'(app'(minsort(), app'(app'(add(), n), x)), y) -> app'(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'(app'(minsort(), nil()), 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'(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'(min(), app'(app'(add(), n), nil())) -> n} Open SCC (3): Strict: { app'#(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil()), app'#(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'#(app'(minsort(), x), app'(app'(add(), n), y)), app'#(app'(minsort(), app'(app'(add(), n), x)), y) -> app'#(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), 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_rm(), true()), n), app'(app'(add(), m), x)) -> app'(app'(rm(), n), x), app'(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(rm(), n), x)), app'(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())), app'(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'(app'(minsort(), x), app'(app'(add(), n), y)), 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(), x)) -> false(), app'(app'(eq(), 0()), 0()) -> true(), 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'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), n), x)), app'(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), m), x)), app'(app'(rm(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'(app'(rm(), n), nil()) -> nil(), app'(app'(minsort(), app'(app'(add(), n), x)), y) -> app'(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'(app'(minsort(), nil()), 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'(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'(min(), app'(app'(add(), n), nil())) -> n} Open SCC (3): Strict: { app'#(app'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), n), x)), app'#(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(min(), app'(app'(add(), m), x)), app'#(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'#(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), 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_rm(), true()), n), app'(app'(add(), m), x)) -> app'(app'(rm(), n), x), app'(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(rm(), n), x)), app'(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())), app'(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'(app'(minsort(), x), app'(app'(add(), n), y)), 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(), x)) -> false(), app'(app'(eq(), 0()), 0()) -> true(), 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'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), n), x)), app'(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), m), x)), app'(app'(rm(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'(app'(rm(), n), nil()) -> nil(), app'(app'(minsort(), app'(app'(add(), n), x)), y) -> app'(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'(app'(minsort(), nil()), 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'(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'(min(), app'(app'(add(), n), nil())) -> n} 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'(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_rm(), true()), n), app'(app'(add(), m), x)) -> app'(app'(rm(), n), x), app'(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(rm(), n), x)), app'(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())), app'(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'(app'(minsort(), x), app'(app'(add(), n), y)), 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(), x)) -> false(), app'(app'(eq(), 0()), 0()) -> true(), 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'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), n), x)), app'(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), m), x)), app'(app'(rm(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'(app'(rm(), n), nil()) -> nil(), app'(app'(minsort(), app'(app'(add(), n), x)), y) -> app'(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'(app'(minsort(), nil()), 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'(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'(min(), app'(app'(add(), n), nil())) -> n} Open SCC (3): Strict: { app'#(app'(app'(if_rm(), true()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'#(app'(rm(), n), x), app'#(app'(rm(), n), app'(app'(add(), m), x)) -> app'#(app'(app'(if_rm(), app'(app'(eq(), n), m)), 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_rm(), true()), n), app'(app'(add(), m), x)) -> app'(app'(rm(), n), x), app'(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(rm(), n), x)), app'(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())), app'(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'(app'(minsort(), x), app'(app'(add(), n), y)), 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(), x)) -> false(), app'(app'(eq(), 0()), 0()) -> true(), 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'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), n), x)), app'(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), m), x)), app'(app'(rm(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'(app'(rm(), n), nil()) -> nil(), app'(app'(minsort(), app'(app'(add(), n), x)), y) -> app'(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'(app'(minsort(), nil()), 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'(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'(min(), app'(app'(add(), n), nil())) -> n} 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'(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_rm(), true()), n), app'(app'(add(), m), x)) -> app'(app'(rm(), n), x), app'(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(rm(), n), x)), app'(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())), app'(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'(app'(minsort(), x), app'(app'(add(), n), y)), 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(), x)) -> false(), app'(app'(eq(), 0()), 0()) -> true(), 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'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), n), x)), app'(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), m), x)), app'(app'(rm(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'(app'(rm(), n), nil()) -> nil(), app'(app'(minsort(), app'(app'(add(), n), x)), y) -> app'(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'(app'(minsort(), nil()), 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'(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'(min(), app'(app'(add(), n), nil())) -> n} Open 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_rm(), true()), n), app'(app'(add(), m), x)) -> app'(app'(rm(), n), x), app'(app'(app'(if_rm(), false()), n), app'(app'(add(), m), x)) -> app'(app'(add(), m), app'(app'(rm(), n), x)), app'(app'(app'(if_minsort(), true()), app'(app'(add(), n), x)), y) -> app'(app'(add(), n), app'(app'(minsort(), app'(app'(app(), app'(app'(rm(), n), x)), y)), nil())), app'(app'(app'(if_minsort(), false()), app'(app'(add(), n), x)), y) -> app'(app'(minsort(), x), app'(app'(add(), n), y)), 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(), x)) -> false(), app'(app'(eq(), 0()), 0()) -> true(), 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'(if_min(), true()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), n), x)), app'(app'(if_min(), false()), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(min(), app'(app'(add(), m), x)), app'(app'(rm(), n), app'(app'(add(), m), x)) -> app'(app'(app'(if_rm(), app'(app'(eq(), n), m)), n), app'(app'(add(), m), x)), app'(app'(rm(), n), nil()) -> nil(), app'(app'(minsort(), app'(app'(add(), n), x)), y) -> app'(app'(app'(if_minsort(), app'(app'(eq(), n), app'(min(), app'(app'(add(), n), x)))), app'(app'(add(), n), x)), y), app'(app'(minsort(), nil()), 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'(min(), app'(app'(add(), n), app'(app'(add(), m), x))) -> app'(app'(if_min(), app'(app'(le(), n), m)), app'(app'(add(), n), app'(app'(add(), m), x))), app'(min(), app'(app'(add(), n), nil())) -> n} Open