YES TRS: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(*(), app(s(), x)), y) -> app(app(+(), app(app(*(), x), y)), y), app(app(*(), 0()), y) -> 0(), app(app(+(), x), app(s(), y)) -> app(s(), app(app(+(), x), y)), app(app(+(), x), 0()) -> 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), 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(p(), app(s(), x)) -> x, app(fact(), app(s(), x)) -> app(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app(fact(), 0()) -> app(s(), 0())} DP: Strict: { 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(*(), app(s(), x)), y) -> app#(app(*(), x), y), app#(app(*(), app(s(), x)), y) -> app#(app(+(), app(app(*(), x), y)), y), app#(app(*(), app(s(), x)), y) -> app#(*(), x), app#(app(*(), app(s(), x)), y) -> app#(+(), app(app(*(), x), y)), app#(app(+(), x), app(s(), y)) -> app#(app(+(), x), y), app#(app(+(), x), app(s(), y)) -> app#(s(), app(app(+(), x), y)), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(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#(fact(), app(s(), x)) -> app#(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app#(fact(), app(s(), x)) -> app#(p(), app(s(), x)), app#(fact(), app(s(), x)) -> app#(fact(), app(p(), app(s(), x))), app#(fact(), app(s(), x)) -> app#(*(), app(s(), x)), app#(fact(), 0()) -> app#(s(), 0())} Weak: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(*(), app(s(), x)), y) -> app(app(+(), app(app(*(), x), y)), y), app(app(*(), 0()), y) -> 0(), app(app(+(), x), app(s(), y)) -> app(s(), app(app(+(), x), y)), app(app(+(), x), 0()) -> 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), 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(p(), app(s(), x)) -> x, app(fact(), app(s(), x)) -> app(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app(fact(), 0()) -> app(s(), 0())} EDG: { (app#(app(*(), app(s(), x)), y) -> app#(app(*(), x), y), app#(app(*(), app(s(), x)), y) -> app#(+(), app(app(*(), x), y))) (app#(app(*(), app(s(), x)), y) -> app#(app(*(), x), y), app#(app(*(), app(s(), x)), y) -> app#(*(), x)) (app#(app(*(), app(s(), x)), y) -> app#(app(*(), x), y), app#(app(*(), app(s(), x)), y) -> app#(app(+(), app(app(*(), x), y)), y)) (app#(app(*(), app(s(), x)), y) -> app#(app(*(), x), y), app#(app(*(), app(s(), x)), y) -> app#(app(*(), x), y)) (app#(app(+(), x), app(s(), y)) -> app#(app(+(), x), y), app#(app(+(), x), app(s(), y)) -> app#(s(), app(app(+(), x), y))) (app#(app(+(), x), app(s(), y)) -> app#(app(+(), x), y), app#(app(+(), x), app(s(), y)) -> app#(app(+(), x), y)) (app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x))) (app#(app(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#(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(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#(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#(cons(), app(f, x))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(fact(), 0()) -> app#(s(), 0())) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(fact(), app(s(), x)) -> app#(*(), app(s(), x))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(fact(), app(s(), x)) -> app#(fact(), app(p(), app(s(), x)))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(fact(), app(s(), x)) -> app#(p(), app(s(), x))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(fact(), app(s(), x)) -> app#(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x))))) (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(+(), x), app(s(), y)) -> app#(s(), app(app(+(), x), y))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(+(), x), app(s(), y)) -> app#(app(+(), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(*(), app(s(), x)), y) -> app#(+(), app(app(*(), x), y))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(*(), app(s(), x)), y) -> app#(*(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(*(), app(s(), x)), y) -> app#(app(+(), app(app(*(), x), y)), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(*(), app(s(), x)), y) -> app#(app(*(), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), f)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs))) (app#(fact(), app(s(), x)) -> app#(fact(), app(p(), app(s(), x))), app#(fact(), 0()) -> app#(s(), 0())) (app#(fact(), app(s(), x)) -> app#(fact(), app(p(), app(s(), x))), app#(fact(), app(s(), x)) -> app#(*(), app(s(), x))) (app#(fact(), app(s(), x)) -> app#(fact(), app(p(), app(s(), x))), app#(fact(), app(s(), x)) -> app#(fact(), app(p(), app(s(), x)))) (app#(fact(), app(s(), x)) -> app#(fact(), app(p(), app(s(), x))), app#(fact(), app(s(), x)) -> app#(p(), app(s(), x))) (app#(fact(), app(s(), x)) -> app#(fact(), app(p(), app(s(), x))), app#(fact(), app(s(), x)) -> app#(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x))))) (app#(fact(), app(s(), x)) -> app#(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app#(app(*(), app(s(), x)), y) -> app#(app(*(), x), y)) (app#(fact(), app(s(), x)) -> app#(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app#(app(*(), app(s(), x)), y) -> app#(app(+(), app(app(*(), x), y)), y)) (app#(fact(), app(s(), x)) -> app#(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app#(app(*(), app(s(), x)), y) -> app#(*(), x)) (app#(fact(), app(s(), x)) -> app#(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app#(app(*(), app(s(), x)), y) -> app#(+(), app(app(*(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), f)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(*(), app(s(), x)), y) -> app#(app(*(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(*(), app(s(), x)), y) -> app#(app(+(), app(app(*(), x), y)), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(*(), app(s(), x)), y) -> app#(*(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(*(), app(s(), x)), y) -> app#(+(), app(app(*(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(+(), x), app(s(), y)) -> app#(app(+(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(+(), x), app(s(), y)) -> app#(s(), app(app(+(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(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#(fact(), app(s(), x)) -> app#(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x))))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(fact(), app(s(), x)) -> app#(p(), app(s(), x))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(fact(), app(s(), x)) -> app#(fact(), app(p(), app(s(), x)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(fact(), app(s(), x)) -> app#(*(), app(s(), x))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(fact(), 0()) -> app#(s(), 0())) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), 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#(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#(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(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#(filter2(), app(f, x))) (app#(app(*(), app(s(), x)), y) -> app#(app(+(), app(app(*(), x), y)), y), app#(app(+(), x), app(s(), y)) -> app#(app(+(), x), y)) (app#(app(*(), app(s(), x)), y) -> app#(app(+(), app(app(*(), x), y)), y), app#(app(+(), x), app(s(), y)) -> app#(s(), app(app(+(), x), y))) } SCCS: Scc: {app#(fact(), app(s(), x)) -> app#(fact(), app(p(), app(s(), x)))} Scc: {app#(app(+(), x), app(s(), y)) -> app#(app(+(), x), y)} Scc: {app#(app(*(), app(s(), x)), y) -> app#(app(*(), x), y)} Scc: { app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs)} SCC: Strict: {app#(fact(), app(s(), x)) -> app#(fact(), app(p(), app(s(), 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(*(), app(s(), x)), y) -> app(app(+(), app(app(*(), x), y)), y), app(app(*(), 0()), y) -> 0(), app(app(+(), x), app(s(), y)) -> app(s(), app(app(+(), x), y)), app(app(+(), x), 0()) -> 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), 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(p(), app(s(), x)) -> x, app(fact(), app(s(), x)) -> app(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app(fact(), 0()) -> app(s(), 0())} UR: {app(p(), app(s(), x)) -> x} BOUND: Bound: match(-raise)-bounded by 1 Automaton: { fact_1() -> 2* fact_0() -> 1* s_1() -> 4* s_0() -> 1* p_1() -> 3* p_0() -> 1* app#_1(2, 6) -> 1* app#_0(1, 1) -> 1* app_1(4, 1) -> 5* app_1(3, 5) -> 6* app_0(1, 1) -> 1* 1 -> 6*} Strict: {} Qed SCC: Strict: {app#(app(+(), x), app(s(), y)) -> app#(app(+(), x), y)} Weak: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(*(), app(s(), x)), y) -> app(app(+(), app(app(*(), x), y)), y), app(app(*(), 0()), y) -> 0(), app(app(+(), x), app(s(), y)) -> app(s(), app(app(+(), x), y)), app(app(+(), x), 0()) -> 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), 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(p(), app(s(), x)) -> x, app(fact(), app(s(), x)) -> app(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app(fact(), 0()) -> app(s(), 0())} SPSC: Simple Projection: pi(app#) = 1 Strict: {} Qed SCC: Strict: {app#(app(*(), app(s(), x)), y) -> app#(app(*(), x), y)} Weak: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(*(), app(s(), x)), y) -> app(app(+(), app(app(*(), x), y)), y), app(app(*(), 0()), y) -> 0(), app(app(+(), x), app(s(), y)) -> app(s(), app(app(+(), x), y)), app(app(+(), x), 0()) -> 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), 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(p(), app(s(), x)) -> x, app(fact(), app(s(), x)) -> app(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app(fact(), 0()) -> app(s(), 0())} UR: {} BOUND: Bound: match(-raise)-bounded by 1 Automaton: { *_1() -> 3* *_0() -> 1* s_0() -> 2* app#_1(4, 2) -> 1* app#_1(4, 1) -> 1* app#_0(2, 2) -> 1* app#_0(2, 1) -> 1* app#_0(1, 2) -> 1* app#_0(1, 1) -> 1* app_1(3, 2) -> 4* app_1(3, 1) -> 4* app_0(2, 2) -> 1* app_0(2, 1) -> 1* app_0(1, 2) -> 1* app_0(1, 1) -> 1*} Strict: {} Qed SCC: Strict: { app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs)} Weak: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(*(), app(s(), x)), y) -> app(app(+(), app(app(*(), x), y)), y), app(app(*(), 0()), y) -> 0(), app(app(+(), x), app(s(), y)) -> app(s(), app(app(+(), x), y)), app(app(+(), x), 0()) -> 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), 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(p(), app(s(), x)) -> x, app(fact(), app(s(), x)) -> app(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app(fact(), 0()) -> app(s(), 0())} SPSC: Simple Projection: pi(app#) = 1 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#(app(app(app(filter2(), app(f, x)), f), x), xs)} EDG: {(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(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(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(), 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#(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(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#(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(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))} SCCS: Scc: {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)} 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(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs)} SCC: Strict: {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)} Weak: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(*(), app(s(), x)), y) -> app(app(+(), app(app(*(), x), y)), y), app(app(*(), 0()), y) -> 0(), app(app(+(), x), app(s(), y)) -> app(s(), app(app(+(), x), y)), app(app(+(), x), 0()) -> 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), 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(p(), app(s(), x)) -> x, app(fact(), app(s(), x)) -> app(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app(fact(), 0()) -> app(s(), 0())} SPSC: Simple Projection: pi(app#) = 0 Strict: {app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)} EDG: {(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))} SCCS: Scc: {app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)} SCC: Strict: {app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)} Weak: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(*(), app(s(), x)), y) -> app(app(+(), app(app(*(), x), y)), y), app(app(*(), 0()), y) -> 0(), app(app(+(), x), app(s(), y)) -> app(s(), app(app(+(), x), y)), app(app(+(), x), 0()) -> 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), 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(p(), app(s(), x)) -> x, app(fact(), app(s(), x)) -> app(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app(fact(), 0()) -> app(s(), 0())} SPSC: Simple Projection: pi(app#) = 1 Strict: {} Qed SCC: 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(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs)} Weak: { app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)), app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs), app(app(*(), app(s(), x)), y) -> app(app(+(), app(app(*(), x), y)), y), app(app(*(), 0()), y) -> 0(), app(app(+(), x), app(s(), y)) -> app(s(), app(app(+(), x), y)), app(app(+(), x), 0()) -> 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), 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(p(), app(s(), x)) -> x, app(fact(), app(s(), x)) -> app(app(*(), app(s(), x)), app(fact(), app(p(), app(s(), x)))), app(fact(), 0()) -> app(s(), 0())} SPSC: Simple Projection: pi(app#) = 1 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)} EDG: {} SCCS: Qed