YES TRS: { app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(if(), app(f, x)), app(app(cons(), x), app(app(filter(), f), xs))), app(app(filter(), f), xs)), app(app(filter(), f), nil()) -> nil()} DP: Strict: {app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(if(), app(f, x)), app(app(cons(), x), app(app(filter(), f), xs))), app(app(filter(), f), xs)), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(if(), app(f, x)), app(app(cons(), x), app(app(filter(), f), xs))), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(cons(), x), app(app(filter(), f), xs)), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(if(), app(f, x))} Weak: { app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(if(), app(f, x)), app(app(cons(), x), app(app(filter(), f), xs))), app(app(filter(), f), xs)), app(app(filter(), f), nil()) -> nil()} EDG: {(app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(if(), 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(cons(), x), app(app(filter(), f), xs))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(if(), app(f, x)), app(app(cons(), x), app(app(filter(), f), xs)))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(if(), app(f, x)), app(app(cons(), x), app(app(filter(), f), 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#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(if(), app(f, x))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(cons(), x), app(app(filter(), f), xs))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(if(), app(f, x)), app(app(cons(), x), app(app(filter(), f), xs)))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(if(), app(f, x)), app(app(cons(), x), app(app(filter(), f), xs))), app(app(filter(), f), xs))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x))} SCCS: Scc: {app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs)} SCC: Strict: {app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs)} Weak: { app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(if(), app(f, x)), app(app(cons(), x), app(app(filter(), f), xs))), app(app(filter(), f), xs)), app(app(filter(), f), nil()) -> nil()} SPSC: Simple Projection: pi(app#) = 0 Strict: {app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs)} EDG: {(app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs))} SCCS: Scc: {app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs)} SCC: Strict: {app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter(), f), xs)} Weak: { app(app(app(if(), true()), x), y) -> x, app(app(app(if(), false()), x), y) -> y, app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(if(), app(f, x)), app(app(cons(), x), app(app(filter(), f), xs))), app(app(filter(), f), xs)), app(app(filter(), f), nil()) -> nil()} SPSC: Simple Projection: pi(app#) = 1 Strict: {} Qed