YES TRS: {app(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app(app(filter(), f), ys), app(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app(app(cons(), y), app(app(filter(), f), ys)), app(app(neq(), app(s(), x)), app(s(), y)) -> app(app(neq(), x), y), app(app(neq(), app(s(), x)), 0()) -> true(), app(app(neq(), 0()), app(s(), y)) -> true(), app(app(neq(), 0()), 0()) -> false(), app(app(filter(), f), app(app(cons(), y), ys)) -> app(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app(app(filter(), f), nil()) -> nil(), nonzero() -> app(filter(), app(neq(), 0()))} DP: Strict: {app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(filter(), f), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(filter(), f), ys)), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(filter(), f), app#(app(neq(), app(s(), x)), app(s(), y)) -> app#(app(neq(), x), y), app#(app(neq(), app(s(), x)), app(s(), y)) -> app#(neq(), x), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(filtersub(), app(f, y)), f), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y)), nonzero#() -> app#(neq(), 0()), nonzero#() -> app#(filter(), app(neq(), 0()))} Weak: {app(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app(app(filter(), f), ys), app(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app(app(cons(), y), app(app(filter(), f), ys)), app(app(neq(), app(s(), x)), app(s(), y)) -> app(app(neq(), x), y), app(app(neq(), app(s(), x)), 0()) -> true(), app(app(neq(), 0()), app(s(), y)) -> true(), app(app(neq(), 0()), 0()) -> false(), app(app(filter(), f), app(app(cons(), y), ys)) -> app(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app(app(filter(), f), nil()) -> nil(), nonzero() -> app(filter(), app(neq(), 0()))} EDG: {(app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y))) (app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(filtersub(), app(f, y)), f)) (app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))) (app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y))) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(filtersub(), app(f, y)), f)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(neq(), app(s(), x)), app(s(), y)) -> app#(neq(), x)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(neq(), app(s(), x)), app(s(), y)) -> app#(app(neq(), x), y)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(filter(), f)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(filter(), f), ys))) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(filter(), f)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(filter(), f)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(filter(), f), ys))) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(filter(), f)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys)) (app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y)) (app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))) (app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(filtersub(), app(f, y)), f)) (app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(filtersub(), app(f, y))) (app#(app(neq(), app(s(), x)), app(s(), y)) -> app#(app(neq(), x), y), app#(app(neq(), app(s(), x)), app(s(), y)) -> app#(app(neq(), x), y)) (app#(app(neq(), app(s(), x)), app(s(), y)) -> app#(app(neq(), x), y), app#(app(neq(), app(s(), x)), app(s(), y)) -> app#(neq(), x))} SCCS: Scc: {app#(app(neq(), app(s(), x)), app(s(), y)) -> app#(app(neq(), x), y)} Scc: {app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))} SCC: Strict: {app#(app(neq(), app(s(), x)), app(s(), y)) -> app#(app(neq(), x), y)} Weak: {app(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app(app(filter(), f), ys), app(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app(app(cons(), y), app(app(filter(), f), ys)), app(app(neq(), app(s(), x)), app(s(), y)) -> app(app(neq(), x), y), app(app(neq(), app(s(), x)), 0()) -> true(), app(app(neq(), 0()), app(s(), y)) -> true(), app(app(neq(), 0()), 0()) -> false(), app(app(filter(), f), app(app(cons(), y), ys)) -> app(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app(app(filter(), f), nil()) -> nil(), nonzero() -> app(filter(), app(neq(), 0()))} SPSC: Simple Projection: pi(app#) = 1 Strict: {} Qed SCC: Strict: {app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(f, y), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))} Weak: {app(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app(app(filter(), f), ys), app(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app(app(cons(), y), app(app(filter(), f), ys)), app(app(neq(), app(s(), x)), app(s(), y)) -> app(app(neq(), x), y), app(app(neq(), app(s(), x)), 0()) -> true(), app(app(neq(), 0()), app(s(), y)) -> true(), app(app(neq(), 0()), 0()) -> false(), app(app(filter(), f), app(app(cons(), y), ys)) -> app(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app(app(filter(), f), nil()) -> nil(), nonzero() -> app(filter(), app(neq(), 0()))} SPSC: Simple Projection: pi(app#) = 1 Strict: {app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))} EDG: {(app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys)) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys)) (app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)))} SCCS: Scc: {app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))} SCC: Strict: {app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))} Weak: {app(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app(app(filter(), f), ys), app(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app(app(cons(), y), app(app(filter(), f), ys)), app(app(neq(), app(s(), x)), app(s(), y)) -> app(app(neq(), x), y), app(app(neq(), app(s(), x)), 0()) -> true(), app(app(neq(), 0()), app(s(), y)) -> true(), app(app(neq(), 0()), 0()) -> false(), app(app(filter(), f), app(app(cons(), y), ys)) -> app(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app(app(filter(), f), nil()) -> nil(), nonzero() -> app(filter(), app(neq(), 0()))} SPSC: Simple Projection: pi(app#) = 1 Strict: {app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))} EDG: {(app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))) (app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys))} SCCS: Scc: {app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))} SCC: Strict: {app#(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app#(app(filter(), f), ys), app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))} Weak: {app(app(app(filtersub(), false()), f), app(app(cons(), y), ys)) -> app(app(filter(), f), ys), app(app(app(filtersub(), true()), f), app(app(cons(), y), ys)) -> app(app(cons(), y), app(app(filter(), f), ys)), app(app(neq(), app(s(), x)), app(s(), y)) -> app(app(neq(), x), y), app(app(neq(), app(s(), x)), 0()) -> true(), app(app(neq(), 0()), app(s(), y)) -> true(), app(app(neq(), 0()), 0()) -> false(), app(app(filter(), f), app(app(cons(), y), ys)) -> app(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys)), app(app(filter(), f), nil()) -> nil(), nonzero() -> app(filter(), app(neq(), 0()))} SPSC: Simple Projection: pi(app#) = 1 Strict: {app#(app(filter(), f), app(app(cons(), y), ys)) -> app#(app(app(filtersub(), app(f, y)), f), app(app(cons(), y), ys))} EDG: {} SCCS: Qed