MAYBE TRS: { app(app(app(if(), true()), xs), ys) -> xs, app(app(app(if(), false()), xs), ys) -> ys, app(app(lt(), y), 0()) -> false(), app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y), app(app(lt(), 0()), app(s(), y)) -> true(), app(app(eq(), x), x) -> true(), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(merge(), xs), nil()) -> xs, app(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))), app(app(merge(), nil()), ys) -> ys, 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(mult(), app(s(), x)), y) -> app(app(plus(), y), app(app(mult(), x), y)), app(app(mult(), 0()), x) -> 0(), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), x) -> 0(), hamming() -> app(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3()))), list1() -> app(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), list2() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), list3() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming())} DP: Strict: { app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y), app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(lt(), x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(lt(), x), y), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(eq(), x), y), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys))), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(lt(), x), y)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(eq(), x), y)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(lt(), x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(eq(), x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(merge(), 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#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)), app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y), app#(app(mult(), app(s(), x)), y) -> app#(app(plus(), y), app(app(mult(), x), y)), app#(app(mult(), app(s(), x)), y) -> app#(mult(), x), app#(app(mult(), app(s(), x)), y) -> app#(plus(), 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#(plus(), x), hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), hamming#() -> app#(app(merge(), list2()), list3()), hamming#() -> app#(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3()))), hamming#() -> app#(s(), 0()), hamming#() -> app#(merge(), list1()), hamming#() -> app#(merge(), list2()), hamming#() -> app#(cons(), app(s(), 0())), hamming#() -> list1#(), hamming#() -> list2#(), hamming#() -> list3#(), list1#() -> app#(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), list1#() -> app#(s(), app(s(), 0())), list1#() -> app#(s(), 0()), list1#() -> app#(map(), app(mult(), app(s(), app(s(), 0())))), list1#() -> app#(mult(), app(s(), app(s(), 0()))), list1#() -> hamming#(), list2#() -> app#(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), list2#() -> app#(s(), app(s(), app(s(), 0()))), list2#() -> app#(s(), app(s(), 0())), list2#() -> app#(s(), 0()), list2#() -> app#(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), list2#() -> app#(mult(), app(s(), app(s(), app(s(), 0())))), list2#() -> hamming#(), list3#() -> app#(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming()), list3#() -> app#(s(), app(s(), app(s(), app(s(), app(s(), 0()))))), list3#() -> app#(s(), app(s(), app(s(), app(s(), 0())))), list3#() -> app#(s(), app(s(), app(s(), 0()))), list3#() -> app#(s(), app(s(), 0())), list3#() -> app#(s(), 0()), list3#() -> app#(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), list3#() -> app#(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0())))))), list3#() -> hamming#()} Weak: { app(app(app(if(), true()), xs), ys) -> xs, app(app(app(if(), false()), xs), ys) -> ys, app(app(lt(), y), 0()) -> false(), app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y), app(app(lt(), 0()), app(s(), y)) -> true(), app(app(eq(), x), x) -> true(), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(merge(), xs), nil()) -> xs, app(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))), app(app(merge(), nil()), ys) -> ys, 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(mult(), app(s(), x)), y) -> app(app(plus(), y), app(app(mult(), x), y)), app(app(mult(), 0()), x) -> 0(), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), x) -> 0(), hamming() -> app(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3()))), list1() -> app(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), list2() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), list3() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming())} EDG: { (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(merge(), xs)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(eq(), x)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(lt(), x)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(eq(), x), y))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(lt(), x), y))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), ys))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(eq(), x), y)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(lt(), x), y)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys)))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys))))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))))) (app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y), app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(lt(), x)) (app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y), app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), 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(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#(app(plus(), x), y)) (app#(app(mult(), app(s(), x)), y) -> app#(app(plus(), y), app(app(mult(), x), y)), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(mult(), app(s(), x)), y) -> app#(app(plus(), y), app(app(mult(), x), y)), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(app(mult(), app(s(), x)), y) -> app#(app(plus(), y), app(app(mult(), x), y)), 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#(plus(), x)) (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#(app(plus(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(mult(), app(s(), x)), y) -> app#(plus(), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(mult(), app(s(), x)), y) -> app#(mult(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(mult(), app(s(), x)), y) -> app#(app(plus(), y), app(app(mult(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y)) (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(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#(f, x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(merge(), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(eq(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(lt(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(eq(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(lt(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), ys))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(eq(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(lt(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys))))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(lt(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y)) (hamming#() -> list1#(), list1#() -> hamming#()) (hamming#() -> list1#(), list1#() -> app#(mult(), app(s(), app(s(), 0())))) (hamming#() -> list1#(), list1#() -> app#(map(), app(mult(), app(s(), app(s(), 0()))))) (hamming#() -> list1#(), list1#() -> app#(s(), 0())) (hamming#() -> list1#(), list1#() -> app#(s(), app(s(), 0()))) (hamming#() -> list1#(), list1#() -> app#(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming())) (hamming#() -> list3#(), list3#() -> hamming#()) (hamming#() -> list3#(), list3#() -> app#(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))) (hamming#() -> list3#(), list3#() -> app#(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0())))))))) (hamming#() -> list3#(), list3#() -> app#(s(), 0())) (hamming#() -> list3#(), list3#() -> app#(s(), app(s(), 0()))) (hamming#() -> list3#(), list3#() -> app#(s(), app(s(), app(s(), 0())))) (hamming#() -> list3#(), list3#() -> app#(s(), app(s(), app(s(), app(s(), 0()))))) (hamming#() -> list3#(), list3#() -> app#(s(), app(s(), app(s(), app(s(), app(s(), 0())))))) (hamming#() -> list3#(), list3#() -> app#(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming())) (list2#() -> hamming#(), hamming#() -> list3#()) (list2#() -> hamming#(), hamming#() -> list2#()) (list2#() -> hamming#(), hamming#() -> list1#()) (list2#() -> hamming#(), hamming#() -> app#(cons(), app(s(), 0()))) (list2#() -> hamming#(), hamming#() -> app#(merge(), list2())) (list2#() -> hamming#(), hamming#() -> app#(merge(), list1())) (list2#() -> hamming#(), hamming#() -> app#(s(), 0())) (list2#() -> hamming#(), hamming#() -> app#(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3())))) (list2#() -> hamming#(), hamming#() -> app#(app(merge(), list2()), list3())) (list2#() -> hamming#(), hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3()))) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(merge(), xs)) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(eq(), x)) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(lt(), x)) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(eq(), x), y))) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(lt(), x), y))) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), ys))) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys)) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys)) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(eq(), x), y)) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(lt(), x), y)) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys)))) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys))))) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))) (hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3())), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))))) (list3#() -> hamming#(), hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3()))) (list3#() -> hamming#(), hamming#() -> app#(app(merge(), list2()), list3())) (list3#() -> hamming#(), hamming#() -> app#(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3())))) (list3#() -> hamming#(), hamming#() -> app#(s(), 0())) (list3#() -> hamming#(), hamming#() -> app#(merge(), list1())) (list3#() -> hamming#(), hamming#() -> app#(merge(), list2())) (list3#() -> hamming#(), hamming#() -> app#(cons(), app(s(), 0()))) (list3#() -> hamming#(), hamming#() -> list1#()) (list3#() -> hamming#(), hamming#() -> list2#()) (list3#() -> hamming#(), hamming#() -> list3#()) (list1#() -> hamming#(), hamming#() -> app#(app(merge(), list1()), app(app(merge(), list2()), list3()))) (list1#() -> hamming#(), hamming#() -> app#(app(merge(), list2()), list3())) (list1#() -> hamming#(), hamming#() -> app#(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3())))) (list1#() -> hamming#(), hamming#() -> app#(s(), 0())) (list1#() -> hamming#(), hamming#() -> app#(merge(), list1())) (list1#() -> hamming#(), hamming#() -> app#(merge(), list2())) (list1#() -> hamming#(), hamming#() -> app#(cons(), app(s(), 0()))) (list1#() -> hamming#(), hamming#() -> list1#()) (list1#() -> hamming#(), hamming#() -> list2#()) (list1#() -> hamming#(), hamming#() -> list3#()) (hamming#() -> list2#(), list2#() -> app#(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming())) (hamming#() -> list2#(), list2#() -> app#(s(), app(s(), app(s(), 0())))) (hamming#() -> list2#(), list2#() -> app#(s(), app(s(), 0()))) (hamming#() -> list2#(), list2#() -> app#(s(), 0())) (hamming#() -> list2#(), list2#() -> app#(map(), app(mult(), app(s(), app(s(), app(s(), 0())))))) (hamming#() -> list2#(), list2#() -> app#(mult(), app(s(), app(s(), app(s(), 0()))))) (hamming#() -> list2#(), list2#() -> hamming#()) (list3#() -> app#(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming()), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (list3#() -> app#(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming()), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (list3#() -> app#(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming()), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (list3#() -> app#(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming()), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x))) (list2#() -> app#(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (list2#() -> app#(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (list2#() -> app#(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (list2#() -> app#(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x))) (list1#() -> app#(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (list1#() -> app#(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (list1#() -> app#(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (list1#() -> app#(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x))) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))))) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys))))) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys)))) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(lt(), x), y)) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(eq(), x), y)) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys)) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys)) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), ys))) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(lt(), x), y))) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(eq(), x), y))) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(lt(), x)) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(eq(), x)) (hamming#() -> app#(app(merge(), list2()), list3()), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(merge(), xs)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys))))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys)))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(lt(), x), y)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(eq(), x), y)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), ys))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(lt(), x), y))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(eq(), x), y))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(lt(), x)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(eq(), x)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(merge(), xs)) (app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y), app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y)) (app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y), app#(app(mult(), app(s(), x)), y) -> app#(app(plus(), y), app(app(mult(), x), y))) (app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y), app#(app(mult(), app(s(), x)), y) -> app#(mult(), x)) (app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y), app#(app(mult(), app(s(), x)), y) -> app#(plus(), y)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(lt(), x), y), app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(lt(), x), y), app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(lt(), x)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys))))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys)))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(lt(), x), y)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(eq(), x), y)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), ys))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(lt(), x), y))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(if(), app(app(eq(), x), y))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(lt(), x)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(eq(), x)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(merge(), 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(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#(cons(), app(f, x))) } SCCS: Scc: {hamming#() -> list1#(), hamming#() -> list2#(), hamming#() -> list3#(), list1#() -> hamming#(), list2#() -> hamming#(), list3#() -> hamming#()} Scc: {app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)} Scc: {app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y)} 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(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys)} Scc: {app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y)} SCC: Strict: {hamming#() -> list1#(), hamming#() -> list2#(), hamming#() -> list3#(), list1#() -> hamming#(), list2#() -> hamming#(), list3#() -> hamming#()} Weak: { app(app(app(if(), true()), xs), ys) -> xs, app(app(app(if(), false()), xs), ys) -> ys, app(app(lt(), y), 0()) -> false(), app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y), app(app(lt(), 0()), app(s(), y)) -> true(), app(app(eq(), x), x) -> true(), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(merge(), xs), nil()) -> xs, app(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))), app(app(merge(), nil()), ys) -> ys, 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(mult(), app(s(), x)), y) -> app(app(plus(), y), app(app(mult(), x), y)), app(app(mult(), 0()), x) -> 0(), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), x) -> 0(), hamming() -> app(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3()))), list1() -> app(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), list2() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), list3() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming())} Fail SCC: Strict: {app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)} Weak: { app(app(app(if(), true()), xs), ys) -> xs, app(app(app(if(), false()), xs), ys) -> ys, app(app(lt(), y), 0()) -> false(), app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y), app(app(lt(), 0()), app(s(), y)) -> true(), app(app(eq(), x), x) -> true(), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(merge(), xs), nil()) -> xs, app(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))), app(app(merge(), nil()), ys) -> ys, 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(mult(), app(s(), x)), y) -> app(app(plus(), y), app(app(mult(), x), y)), app(app(mult(), 0()), x) -> 0(), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), x) -> 0(), hamming() -> app(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3()))), list1() -> app(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), list2() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), list3() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming())} Fail SCC: Strict: {app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y)} Weak: { app(app(app(if(), true()), xs), ys) -> xs, app(app(app(if(), false()), xs), ys) -> ys, app(app(lt(), y), 0()) -> false(), app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y), app(app(lt(), 0()), app(s(), y)) -> true(), app(app(eq(), x), x) -> true(), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(merge(), xs), nil()) -> xs, app(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))), app(app(merge(), nil()), ys) -> ys, 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(mult(), app(s(), x)), y) -> app(app(plus(), y), app(app(mult(), x), y)), app(app(mult(), 0()), x) -> 0(), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), x) -> 0(), hamming() -> app(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3()))), list1() -> app(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), list2() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), list3() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming())} Fail 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(if(), true()), xs), ys) -> xs, app(app(app(if(), false()), xs), ys) -> ys, app(app(lt(), y), 0()) -> false(), app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y), app(app(lt(), 0()), app(s(), y)) -> true(), app(app(eq(), x), x) -> true(), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(merge(), xs), nil()) -> xs, app(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))), app(app(merge(), nil()), ys) -> ys, 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(mult(), app(s(), x)), y) -> app(app(plus(), y), app(app(mult(), x), y)), app(app(mult(), 0()), x) -> 0(), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), x) -> 0(), hamming() -> app(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3()))), list1() -> app(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), list2() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), list3() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming())} SPSC: Simple Projection: pi(app#) = 1 Strict: {app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)} EDG: {(app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x))} SCCS: Scc: {app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)} SCC: Strict: {app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)} Weak: { app(app(app(if(), true()), xs), ys) -> xs, app(app(app(if(), false()), xs), ys) -> ys, app(app(lt(), y), 0()) -> false(), app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y), app(app(lt(), 0()), app(s(), y)) -> true(), app(app(eq(), x), x) -> true(), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(merge(), xs), nil()) -> xs, app(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))), app(app(merge(), nil()), ys) -> ys, 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(mult(), app(s(), x)), y) -> app(app(plus(), y), app(app(mult(), x), y)), app(app(mult(), 0()), x) -> 0(), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), x) -> 0(), hamming() -> app(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3()))), list1() -> app(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), list2() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), list3() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming())} SPSC: Simple Projection: pi(app#) = 0 Strict: {} Qed SCC: Strict: {app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), app(app(cons(), x), xs)), ys)} Weak: { app(app(app(if(), true()), xs), ys) -> xs, app(app(app(if(), false()), xs), ys) -> ys, app(app(lt(), y), 0()) -> false(), app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y), app(app(lt(), 0()), app(s(), y)) -> true(), app(app(eq(), x), x) -> true(), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(merge(), xs), nil()) -> xs, app(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))), app(app(merge(), nil()), ys) -> ys, 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(mult(), app(s(), x)), y) -> app(app(plus(), y), app(app(mult(), x), y)), app(app(mult(), 0()), x) -> 0(), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), x) -> 0(), hamming() -> app(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3()))), list1() -> app(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), list2() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), list3() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming())} SPSC: Simple Projection: pi(app#) = 1 Strict: {app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))} EDG: {(app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys)) (app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)))} SCCS: Scc: {app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))} SCC: Strict: {app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), ys), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))} Weak: { app(app(app(if(), true()), xs), ys) -> xs, app(app(app(if(), false()), xs), ys) -> ys, app(app(lt(), y), 0()) -> false(), app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y), app(app(lt(), 0()), app(s(), y)) -> true(), app(app(eq(), x), x) -> true(), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(merge(), xs), nil()) -> xs, app(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))), app(app(merge(), nil()), ys) -> ys, 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(mult(), app(s(), x)), y) -> app(app(plus(), y), app(app(mult(), x), y)), app(app(mult(), 0()), x) -> 0(), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), x) -> 0(), hamming() -> app(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3()))), list1() -> app(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), list2() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), list3() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming())} SPSC: Simple Projection: pi(app#) = 1 Strict: {app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))} EDG: {(app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)), app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys)))} SCCS: Scc: {app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))} SCC: Strict: {app#(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app#(app(merge(), xs), app(app(cons(), y), ys))} Weak: { app(app(app(if(), true()), xs), ys) -> xs, app(app(app(if(), false()), xs), ys) -> ys, app(app(lt(), y), 0()) -> false(), app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y), app(app(lt(), 0()), app(s(), y)) -> true(), app(app(eq(), x), x) -> true(), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(merge(), xs), nil()) -> xs, app(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))), app(app(merge(), nil()), ys) -> ys, 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(mult(), app(s(), x)), y) -> app(app(plus(), y), app(app(mult(), x), y)), app(app(mult(), 0()), x) -> 0(), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), x) -> 0(), hamming() -> app(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3()))), list1() -> app(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), list2() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), list3() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming())} Fail SCC: Strict: {app#(app(lt(), app(s(), x)), app(s(), y)) -> app#(app(lt(), x), y)} Weak: { app(app(app(if(), true()), xs), ys) -> xs, app(app(app(if(), false()), xs), ys) -> ys, app(app(lt(), y), 0()) -> false(), app(app(lt(), app(s(), x)), app(s(), y)) -> app(app(lt(), x), y), app(app(lt(), 0()), app(s(), y)) -> true(), app(app(eq(), x), x) -> true(), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(merge(), xs), nil()) -> xs, app(app(merge(), app(app(cons(), x), xs)), app(app(cons(), y), ys)) -> app(app(app(if(), app(app(lt(), x), y)), app(app(cons(), x), app(app(merge(), xs), app(app(cons(), y), ys)))), app(app(app(if(), app(app(eq(), x), y)), app(app(cons(), x), app(app(merge(), xs), ys))), app(app(cons(), y), app(app(merge(), app(app(cons(), x), xs)), ys)))), app(app(merge(), nil()), ys) -> ys, 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(mult(), app(s(), x)), y) -> app(app(plus(), y), app(app(mult(), x), y)), app(app(mult(), 0()), x) -> 0(), app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), x) -> 0(), hamming() -> app(app(cons(), app(s(), 0())), app(app(merge(), list1()), app(app(merge(), list2()), list3()))), list1() -> app(app(map(), app(mult(), app(s(), app(s(), 0())))), hamming()), list2() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), 0()))))), hamming()), list3() -> app(app(map(), app(mult(), app(s(), app(s(), app(s(), app(s(), app(s(), 0()))))))), hamming())} SPSC: Simple Projection: pi(app#) = 1 Strict: {} Qed