YES Time: 0.230605 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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)), app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))), app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)), app(D(), t()) -> 1(), app(D(), constant()) -> 0()} 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(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#(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#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y)), app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x)), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y)), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x)), app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x))), app#(D(), app(app(*(), x), y)) -> app#(*(), y), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y)), app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x))} 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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)), app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))), app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)), app(D(), t()) -> 1(), app(D(), constant()) -> 0()} 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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)), app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))), app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)), app(D(), t()) -> 1(), app(D(), constant()) -> 0(), a(z, w) -> z, a(z, w) -> w} EDG: { (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x))) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), y)) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), x)) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y))) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(*(), y)) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x)))) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), y)) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), x)) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x))) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y))) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x))) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), y)) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), x)) (app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y))) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x))) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), y)) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), x)) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y))) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(*(), y)) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x)))) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), y)) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), x)) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x))) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y))) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x))) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), y)) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), x)) (app#(D(), app(app(-(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y))) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x))) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), y)) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), x)) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y))) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(*(), y)) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x)))) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y)) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), x)) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x))) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y))) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x))) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y)) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), x)) (app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y))) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x))) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), y)) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), x)) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y))) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(*(), y)) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x)))) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y)) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), x)) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x))) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y))) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x))) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y)) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), x)) (app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y))) (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#(f, x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(D(), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(D(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(*(), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x)))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(D(), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(D(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(D(), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(D(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), 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(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#(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(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(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(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(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(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#(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#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(D(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(D(), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(D(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(D(), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(*(), x), y)) -> app#(*(), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(D(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(D(), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), 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#(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(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(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#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y))) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), x)) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y)) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x))) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y))) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x))) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), x)) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y)) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x)))) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(*(), y)) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y))) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), x)) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), y)) (app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x))) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(app(+(), app(D(), x)), app(D(), y))) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), x)) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(D(), y)) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(+(), x), y)) -> app#(+(), app(D(), x))) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y)))) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), x), app(D(), y))) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(app(*(), y), app(D(), x))) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), x)) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), y)) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(+(), app(app(*(), y), app(D(), x)))) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(*(), y)) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(app(-(), app(D(), x)), app(D(), y))) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), x)) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), y)) (app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(-(), app(D(), x))) } STATUS: arrows: 0.817778 SCCS (2): 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)} Scc: {app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), y)} SCC (5): 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)} 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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)), app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))), app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)), app(D(), t()) -> 1(), app(D(), constant()) -> 0()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app](x0, x1) = x0 + x1, [1] = 0, [D] = 0, [t] = 0, [0] = 0, [constant] = 0, [+] = 0, [*] = 0, [-] = 0, [nil] = 0, [map] = 0, [cons] = 1, [filter] = 0, [filter2] = 0, [true] = 0, [false] = 0, [app#](x0, x1) = x0 Strict: app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x) 1 + 1x + 0f + 1xs >= 0 + 1x + 0f app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs) 1 + 1x + 0f + 1xs >= 0 + 0f + 1xs app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x) 1 + 1x + 0f + 1xs >= 0 + 1x + 0f app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs) 0 + 0x + 0f + 1xs >= 0 + 0f + 1xs app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs) 0 + 0x + 0f + 1xs >= 0 + 0f + 1xs Weak: app(D(), constant()) -> 0() 0 >= 0 app(D(), t()) -> 1() 0 >= 0 app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)) 0 + 1x + 1y >= 0 + 1x + 1y app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))) 0 + 1x + 1y >= 0 + 2x + 2y app(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)) 0 + 1x + 1y >= 0 + 1x + 1y app(app(filter(), f), nil()) -> nil() 0 + 1f >= 0 app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs) 1 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs app(app(map(), f), nil()) -> nil() 0 + 1f >= 0 app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)) 1 + 1x + 1f + 1xs >= 1 + 1x + 2f + 1xs app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs) 0 + 1x + 1f + 1xs >= 0 + 1f + 1xs app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)) 0 + 1x + 1f + 1xs >= 1 + 1x + 1f + 1xs SCCS (0): SCC (6): Strict: {app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y), app#(D(), app(app(-(), x), y)) -> app#(D(), x), app#(D(), app(app(-(), x), y)) -> app#(D(), 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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)), app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))), app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)), app(D(), t()) -> 1(), app(D(), constant()) -> 0()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app](x0, x1) = x0 + x1, [1] = 0, [D] = 0, [t] = 0, [0] = 0, [constant] = 1, [+] = 0, [*] = 0, [-] = 1, [nil] = 0, [map] = 0, [cons] = 0, [filter] = 0, [filter2] = 0, [true] = 0, [false] = 0, [app#](x0, x1) = x0 + 1 Strict: app#(D(), app(app(-(), x), y)) -> app#(D(), y) 2 + 1x + 1y >= 1 + 1y app#(D(), app(app(-(), x), y)) -> app#(D(), x) 2 + 1x + 1y >= 1 + 1x app#(D(), app(app(*(), x), y)) -> app#(D(), y) 1 + 1x + 1y >= 1 + 1y app#(D(), app(app(*(), x), y)) -> app#(D(), x) 1 + 1x + 1y >= 1 + 1x app#(D(), app(app(+(), x), y)) -> app#(D(), y) 1 + 1x + 1y >= 1 + 1y app#(D(), app(app(+(), x), y)) -> app#(D(), x) 1 + 1x + 1y >= 1 + 1x Weak: app(D(), constant()) -> 0() 1 >= 0 app(D(), t()) -> 1() 0 >= 0 app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)) 1 + 1x + 1y >= 1 + 1x + 1y app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))) 0 + 1x + 1y >= 0 + 2x + 2y app(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)) 0 + 1x + 1y >= 0 + 1x + 1y app(app(filter(), f), nil()) -> nil() 0 + 1f >= 0 app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs) 0 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs app(app(map(), f), nil()) -> nil() 0 + 1f >= 0 app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)) 0 + 1x + 1f + 1xs >= 0 + 1x + 2f + 1xs app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs) 0 + 1x + 1f + 1xs >= 0 + 1f + 1xs app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)) 0 + 1x + 1f + 1xs >= 0 + 1x + 1f + 1xs SCCS (1): Scc: {app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), y)} SCC (4): Strict: {app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y), app#(D(), app(app(*(), x), y)) -> app#(D(), x), app#(D(), app(app(*(), x), y)) -> app#(D(), 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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)), app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))), app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)), app(D(), t()) -> 1(), app(D(), constant()) -> 0()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app](x0, x1) = x0 + x1, [1] = 0, [D] = 0, [t] = 0, [0] = 0, [constant] = 0, [+] = 0, [*] = 1, [-] = 0, [nil] = 0, [map] = 0, [cons] = 0, [filter] = 0, [filter2] = 0, [true] = 0, [false] = 0, [app#](x0, x1) = x0 + 1 Strict: app#(D(), app(app(*(), x), y)) -> app#(D(), y) 2 + 1x + 1y >= 1 + 1y app#(D(), app(app(*(), x), y)) -> app#(D(), x) 2 + 1x + 1y >= 1 + 1x app#(D(), app(app(+(), x), y)) -> app#(D(), y) 1 + 1x + 1y >= 1 + 1y app#(D(), app(app(+(), x), y)) -> app#(D(), x) 1 + 1x + 1y >= 1 + 1x Weak: app(D(), constant()) -> 0() 0 >= 0 app(D(), t()) -> 1() 0 >= 0 app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)) 0 + 1x + 1y >= 0 + 1x + 1y app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))) 1 + 1x + 1y >= 2 + 2x + 2y app(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)) 0 + 1x + 1y >= 0 + 1x + 1y app(app(filter(), f), nil()) -> nil() 0 + 1f >= 0 app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs) 0 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs app(app(map(), f), nil()) -> nil() 0 + 1f >= 0 app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)) 0 + 1x + 1f + 1xs >= 0 + 1x + 2f + 1xs app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs) 0 + 1x + 1f + 1xs >= 0 + 1f + 1xs app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)) 0 + 1x + 1f + 1xs >= 0 + 1x + 1f + 1xs SCCS (1): Scc: {app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), y)} SCC (2): Strict: {app#(D(), app(app(+(), x), y)) -> app#(D(), x), app#(D(), app(app(+(), x), y)) -> app#(D(), 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(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(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)), app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))), app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)), app(D(), t()) -> 1(), app(D(), constant()) -> 0()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app](x0, x1) = x0 + x1, [1] = 0, [D] = 0, [t] = 0, [0] = 0, [constant] = 0, [+] = 1, [*] = 1, [-] = 0, [nil] = 0, [map] = 0, [cons] = 0, [filter] = 0, [filter2] = 0, [true] = 0, [false] = 0, [app#](x0, x1) = x0 + 1 Strict: app#(D(), app(app(+(), x), y)) -> app#(D(), y) 2 + 1x + 1y >= 1 + 1y app#(D(), app(app(+(), x), y)) -> app#(D(), x) 2 + 1x + 1y >= 1 + 1x Weak: app(D(), constant()) -> 0() 0 >= 0 app(D(), t()) -> 1() 0 >= 0 app(D(), app(app(-(), x), y)) -> app(app(-(), app(D(), x)), app(D(), y)) 0 + 1x + 1y >= 0 + 1x + 1y app(D(), app(app(*(), x), y)) -> app(app(+(), app(app(*(), y), app(D(), x))), app(app(*(), x), app(D(), y))) 1 + 1x + 1y >= 3 + 2x + 2y app(D(), app(app(+(), x), y)) -> app(app(+(), app(D(), x)), app(D(), y)) 1 + 1x + 1y >= 1 + 1x + 1y app(app(filter(), f), nil()) -> nil() 0 + 1f >= 0 app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs) 0 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs app(app(map(), f), nil()) -> nil() 0 + 1f >= 0 app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)) 0 + 1x + 1f + 1xs >= 0 + 1x + 2f + 1xs app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs) 0 + 1x + 1f + 1xs >= 0 + 1f + 1xs app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)) 0 + 1x + 1f + 1xs >= 0 + 1x + 1f + 1xs Qed