MAYBE 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(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), x), y), app(app(quot(), app(s(), x)), app(s(), y)) -> app(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y))), app(app(quot(), 0()), app(s(), y)) -> 0(), app(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, 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()} 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(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), x), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(quot(), app(app(minus(), x), y)), app(s(), y)), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(minus(), x), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y))), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(quot(), app(app(minus(), x), y)), app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)), app#(app(plus(), app(s(), x)), y) -> app#(plus(), 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#(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))} 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(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), x), y), app(app(quot(), app(s(), x)), app(s(), y)) -> app(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y))), app(app(quot(), 0()), app(s(), y)) -> 0(), app(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, 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()} EDG: { (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(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(plus(), app(app(plus(), y), app(s(), app(s(), z))))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0())))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(plus(), app(app(minus(), y), app(s(), app(s(), z))))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0())))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(quot(), app(app(minus(), x), y))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y)))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(minus(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(quot(), app(app(minus(), x), y)), app(s(), y))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(filter(), f)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(filter(), f)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(cons(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(cons(), x), app(app(filter(), f), xs))) (app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), x)) (app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), 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#(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(quot(), app(s(), x)), app(s(), y)) -> app#(app(quot(), app(app(minus(), x), y)), app(s(), y)), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y)) (app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(quot(), app(app(minus(), x), y)), app(s(), y)), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(quot(), app(app(minus(), x), y)), app(s(), y))) (app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(quot(), app(app(minus(), x), y)), app(s(), y)), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(minus(), x)) (app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(quot(), app(app(minus(), x), y)), app(s(), y)), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y)))) (app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(quot(), app(app(minus(), x), y)), app(s(), y)), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(quot(), app(app(minus(), x), y))) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0())))) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(plus(), app(app(minus(), y), app(s(), app(s(), z))))) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0())))) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(plus(), app(app(plus(), y), app(s(), app(s(), z))))) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y)) (app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), x)) (app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0())))) (app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(plus(), app(app(minus(), y), app(s(), app(s(), z))))) (app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0())))) (app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(plus(), app(app(plus(), y), app(s(), app(s(), z))))) (app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0())))) (app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(plus(), app(app(minus(), y), app(s(), app(s(), z))))) (app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0())))) (app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(plus(), app(app(plus(), y), app(s(), app(s(), z))))) (app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (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(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(quot(), app(app(minus(), x), y)), app(s(), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(minus(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(quot(), app(app(minus(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0())))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(plus(), app(app(minus(), y), app(s(), app(s(), z))))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0())))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(plus(), app(app(plus(), y), app(s(), app(s(), z))))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(plus(), 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#(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))) } SCCS: Scc: {app#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)} Scc: {app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(quot(), app(app(minus(), x), y)), app(s(), y))} Scc: {app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), 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#(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app#(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app#(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), 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(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), x), y), app(app(quot(), app(s(), x)), app(s(), y)) -> app(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y))), app(app(quot(), 0()), app(s(), y)) -> 0(), app(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, 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()} Fail SCC: Strict: {app#(app(quot(), app(s(), x)), app(s(), y)) -> app#(app(quot(), app(app(minus(), x), y)), app(s(), 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(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), x), y), app(app(quot(), app(s(), x)), app(s(), y)) -> app(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y))), app(app(quot(), 0()), app(s(), y)) -> 0(), app(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, 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()} Fail SCC: Strict: {app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), 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(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), x), y), app(app(quot(), app(s(), x)), app(s(), y)) -> app(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y))), app(app(quot(), 0()), app(s(), y)) -> 0(), app(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, 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()} 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(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(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), x), y), app(app(quot(), app(s(), x)), app(s(), y)) -> app(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y))), app(app(quot(), 0()), app(s(), y)) -> 0(), app(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, 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()} 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(), 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(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#(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(), false()), 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)) (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))} 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(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), x), y), app(app(quot(), app(s(), x)), app(s(), y)) -> app(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y))), app(app(quot(), 0()), app(s(), y)) -> 0(), app(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, 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()} 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(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), x), y), app(app(quot(), app(s(), x)), app(s(), y)) -> app(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y))), app(app(quot(), 0()), app(s(), y)) -> 0(), app(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, 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()} 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(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), x), y), app(app(quot(), app(s(), x)), app(s(), y)) -> app(s(), app(app(quot(), app(app(minus(), x), y)), app(s(), y))), app(app(quot(), 0()), app(s(), y)) -> 0(), app(app(plus(), app(app(minus(), x), app(s(), 0()))), app(app(minus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(minus(), y), app(s(), app(s(), z)))), app(app(minus(), x), app(s(), 0()))), app(app(plus(), app(app(plus(), x), app(s(), 0()))), app(app(plus(), y), app(s(), app(s(), z)))) -> app(app(plus(), app(app(plus(), y), app(s(), app(s(), z)))), app(app(plus(), x), app(s(), 0()))), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, 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()} 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