MAYBE Time: 24.732280 TRS: { app(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app(app(app(app(app(if_reach_2(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> true(), app(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())), app(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(reach(), x), y), empty()), h) -> false(), 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(or(), true()), y) -> true(), app(app(or(), false()), y) -> y, app(app(union(), app(app(app(edge(), x), y), i)), h) -> app(app(app(edge(), x), y), app(app(union(), i), h)), app(app(union(), empty()), h) -> h, 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: DP: { app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), y), v), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(if_reach_2(), app(app(eq(), y), v)), x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(eq(), y), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(if_reach_2(), app(app(eq(), y), v)), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(edge(), u), v), h), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(reach(), x), y), i), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(reach(), x), y), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(reach(), x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(reach(), x), y), i), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(reach(), v), y), app(app(union(), i), h)), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(union(), i), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(reach(), x), y), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(reach(), v), y), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(or(), app(app(app(app(reach(), x), y), i), h)), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(union(), i), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(reach(), x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(reach(), v), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), x), u), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(if_reach_1(), app(app(eq(), x), u)), x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(eq(), x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(if_reach_1(), app(app(eq(), x), u)), 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(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(eq(), x), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(app(edge(), x), y), app(app(union(), i), h)), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(union(), i), h), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(union(), i), 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))} TRS: { app(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app(app(app(app(app(if_reach_2(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> true(), app(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())), app(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(reach(), x), y), empty()), h) -> false(), 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(or(), true()), y) -> true(), app(app(or(), false()), y) -> y, app(app(union(), app(app(app(edge(), x), y), i)), h) -> app(app(app(edge(), x), y), app(app(union(), i), h)), app(app(union(), empty()), h) -> h, 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()} UR: { app(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app(app(app(app(app(if_reach_2(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> true(), app(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())), app(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(reach(), x), y), empty()), h) -> false(), 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(or(), true()), y) -> true(), app(app(or(), false()), y) -> y, app(app(union(), app(app(app(edge(), x), y), i)), h) -> app(app(app(edge(), x), y), app(app(union(), i), h)), app(app(union(), empty()), h) -> h, 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(), a(z, w) -> z, a(z, w) -> w} EDG: { (app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(eq(), x)) (app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y)) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), x), u), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(eq(), x)) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), x), u), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y)) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(reach(), v)) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(reach(), x)) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(union(), i)) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(or(), app(app(app(app(reach(), x), y), i), h))) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(reach(), v), y)) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(reach(), x), y)) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(union(), i), h)) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()))) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(reach(), v), y), app(app(union(), i), h))) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(reach(), x), y), i)) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h)) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(if_reach_1(), app(app(eq(), x), u))) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(eq(), x)) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(if_reach_1(), app(app(eq(), x), u)), x)) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), x), u)) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(if_reach_1(), app(app(eq(), x), u)), x), y)) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i))) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h)) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(reach(), x)) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(reach(), x), y)) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(reach(), x), y), i)) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(edge(), u), v), h)) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h))) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(if_reach_2(), app(app(eq(), y), v))) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(eq(), y)) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(if_reach_2(), app(app(eq(), y), v)), x)) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), y), v)) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(if_reach_2(), app(app(eq(), y), v)), x), y)) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i))) (app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h)) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(if_reach_1(), app(app(eq(), x), u))) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(eq(), x)) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(if_reach_1(), app(app(eq(), x), u)), x)) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), x), u)) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(if_reach_1(), app(app(eq(), x), u)), x), y)) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i))) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h)) (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(union(), app(app(app(edge(), x), y), i)), h) -> app#(union(), i)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(union(), i), h)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(app(edge(), x), y), app(app(union(), i), h))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(eq(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), 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(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(if_reach_1(), app(app(eq(), x), u))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(eq(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(if_reach_1(), app(app(eq(), x), u)), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), x), u)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(if_reach_1(), app(app(eq(), x), u)), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(reach(), v)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(reach(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(union(), i)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(or(), app(app(app(app(reach(), x), y), i), h))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(reach(), v), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(reach(), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(union(), i), h)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(reach(), v), y), app(app(union(), i), h))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(reach(), x), y), i)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(reach(), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(reach(), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(reach(), x), y), i)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(edge(), u), v), h)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(if_reach_2(), app(app(eq(), y), v))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(eq(), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(if_reach_2(), app(app(eq(), y), v)), x)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), y), v)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(if_reach_2(), app(app(eq(), y), v)), x), y)) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i))) (app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h)) (app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x))) (app#(app(app(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#(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(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#(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(), false()), 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(), 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(), 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#(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(cons(), x), app(app(filter(), f), xs))) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), y), v), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y)) (app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), y), v), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(eq(), 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(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(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(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(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(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(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#(filter2(), app(f, x))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(if_reach_2(), app(app(eq(), y), v)), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), y), v)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(if_reach_2(), app(app(eq(), y), v)), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(eq(), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(if_reach_2(), app(app(eq(), y), v))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(edge(), u), v), h)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(reach(), x), y), i)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(reach(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(reach(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(reach(), x), y), i)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(reach(), v), y), app(app(union(), i), h))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(union(), i), h)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(reach(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(reach(), v), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(or(), app(app(app(app(reach(), x), y), i), h))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(union(), i)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(reach(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(reach(), v)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(if_reach_1(), app(app(eq(), x), u)), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), x), u)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(if_reach_1(), app(app(eq(), x), u)), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(eq(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(if_reach_1(), app(app(eq(), x), u))) (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(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(eq(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(app(edge(), x), y), app(app(union(), i), h))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(union(), i), h)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(union(), i)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(f, x)), f), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(filter2(), app(f, x)), f)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(filter2(), app(f, x))) (app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(union(), i), h), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(app(edge(), x), y), app(app(union(), i), h))) (app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(union(), i), h), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(union(), i), h)) (app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(union(), i), h), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(union(), i)) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(union(), i), h), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(app(edge(), x), y), app(app(union(), i), h))) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(union(), i), h), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(union(), i), h)) (app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(union(), i), h), app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(union(), i)) (app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h)) (app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i))) (app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(if_reach_1(), app(app(eq(), x), u)), x), y)) (app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(eq(), x), u)) (app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(if_reach_1(), app(app(eq(), x), u)), x)) (app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(eq(), x)) (app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(if_reach_1(), app(app(eq(), x), u))) } STATUS: arrows: 0.931180 SCCS (4): 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: { app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h)} Scc: {app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(union(), i), h)} Scc: {app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y)} SCC (6): 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(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app(app(app(app(app(if_reach_2(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> true(), app(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())), app(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(reach(), x), y), empty()), h) -> false(), 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(or(), true()), y) -> true(), app(app(or(), false()), y) -> y, app(app(union(), app(app(app(edge(), x), y), i)), h) -> app(app(app(edge(), x), y), app(app(union(), i), h)), app(app(union(), empty()), h) -> h, 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()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app](x0, x1) = x0 + x1, [true] = 0, [eq] = 0, [0] = 0, [false] = 0, [s] = 0, [or] = 0, [union] = 0, [empty] = 0, [edge] = 1, [reach] = 0, [if_reach_1] = 1, [if_reach_2] = 0, [nil] = 0, [map] = 0, [cons] = 1, [filter] = 0, [filter2] = 0, [app#](x0, x1) = x0 Strict: app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(f, x)), f), x), xs) 1 + 1x + 0f + 1xs >= 0 + 0x + 0f + 1xs app#(app(filter(), f), app(app(cons(), x), xs)) -> app#(f, x) 1 + 1x + 0f + 1xs >= 0 + 1x + 0f app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs) 1 + 1x + 0f + 1xs >= 0 + 0f + 1xs app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x) 1 + 1x + 0f + 1xs >= 0 + 1x + 0f app#(app(app(app(filter2(), false()), f), x), xs) -> app#(app(filter(), f), xs) 0 + 0x + 0f + 1xs >= 0 + 0f + 1xs app#(app(app(app(filter2(), true()), f), x), xs) -> app#(app(filter(), f), xs) 0 + 0x + 0f + 1xs >= 0 + 0f + 1xs Weak: app(app(filter(), f), nil()) -> nil() 0 + 1f >= 0 app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs) 1 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs app(app(map(), f), nil()) -> nil() 0 + 1f >= 0 app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)) 1 + 1x + 1f + 1xs >= 1 + 1x + 2f + 1xs app(app(union(), empty()), h) -> h 0 + 1h >= 1h app(app(union(), app(app(app(edge(), x), y), i)), h) -> app(app(app(edge(), x), y), app(app(union(), i), h)) 1 + 1x + 1y + 1h + 1i >= 1 + 1x + 1y + 1h + 1i app(app(or(), false()), y) -> y 0 + 1y >= 1y app(app(or(), true()), y) -> true() 0 + 1y >= 0 app(app(eq(), 0()), 0()) -> true() 0 >= 0 app(app(eq(), 0()), app(s(), x)) -> false() 0 + 1x >= 0 app(app(eq(), app(s(), x)), 0()) -> false() 0 + 1x >= 0 app(app(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y) 0 + 1x + 1y >= 0 + 1x + 1y app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs) 0 + 1x + 1f + 1xs >= 0 + 1f + 1xs app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)) 0 + 1x + 1f + 1xs >= 1 + 1x + 1f + 1xs app(app(app(app(reach(), x), y), empty()), h) -> false() 0 + 1x + 1y + 1h >= 0 app(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h) 1 + 1x + 1y + 1h + 1i + 1u + 1v >= 2 + 2x + 1y + 1h + 1i + 2u + 1v app(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())) 1 + 1x + 1y + 1h + 1i + 1u + 1v >= 0 + 1x + 2y + 2h + 2i + 1v app(app(app(app(app(if_reach_2(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> true() 1 + 1x + 1y + 1h + 1i + 1u + 1v >= 0 app(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)) 2 + 1x + 1y + 1h + 1i + 1u + 1v >= 1 + 1x + 1y + 1h + 1i + 1u + 1v app(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h) 2 + 1x + 1y + 1h + 1i + 1u + 1v >= 1 + 1x + 2y + 1h + 1i + 1u + 2v SCCS (0): SCC (5): Strict: { app#(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app#(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), x), y), i), h), app#(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(reach(), v), y), app(app(union(), i), h)), empty()), app#(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app#(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h)} Weak: { app(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app(app(app(app(app(if_reach_2(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> true(), app(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())), app(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(reach(), x), y), empty()), h) -> false(), 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(or(), true()), y) -> true(), app(app(or(), false()), y) -> y, app(app(union(), app(app(app(edge(), x), y), i)), h) -> app(app(app(edge(), x), y), app(app(union(), i), h)), app(app(union(), empty()), h) -> h, 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 (1): Strict: {app#(app(union(), app(app(app(edge(), x), y), i)), h) -> app#(app(union(), i), h)} Weak: { app(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app(app(app(app(app(if_reach_2(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> true(), app(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())), app(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(reach(), x), y), empty()), h) -> false(), 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(or(), true()), y) -> true(), app(app(or(), false()), y) -> y, app(app(union(), app(app(app(edge(), x), y), i)), h) -> app(app(app(edge(), x), y), app(app(union(), i), h)), app(app(union(), empty()), h) -> h, 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 (1): Strict: {app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y)} Weak: { app(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)), app(app(app(app(app(if_reach_2(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> true(), app(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())), app(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h), app(app(app(app(reach(), x), y), empty()), h) -> false(), 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(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y), app(app(eq(), app(s(), x)), 0()) -> false(), app(app(eq(), 0()), app(s(), x)) -> false(), app(app(eq(), 0()), 0()) -> true(), app(app(or(), true()), y) -> true(), app(app(or(), false()), y) -> y, app(app(union(), app(app(app(edge(), x), y), i)), h) -> app(app(app(edge(), x), y), app(app(union(), i), h)), app(app(union(), empty()), h) -> h, 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()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app](x0, x1) = x0 + x1, [true] = 0, [eq] = 0, [0] = 1, [false] = 0, [s] = 1, [or] = 0, [union] = 0, [empty] = 0, [edge] = 1, [reach] = 0, [if_reach_1] = 1, [if_reach_2] = 1, [nil] = 0, [map] = 0, [cons] = 0, [filter] = 0, [filter2] = 0, [app#](x0, x1) = x0 Strict: app#(app(eq(), app(s(), x)), app(s(), y)) -> app#(app(eq(), x), y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: app(app(filter(), f), nil()) -> nil() 0 + 1f >= 0 app(app(filter(), f), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(f, x)), f), x), xs) 0 + 1x + 1f + 1xs >= 0 + 2x + 2f + 1xs app(app(map(), f), nil()) -> nil() 0 + 1f >= 0 app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)) 0 + 1x + 1f + 1xs >= 0 + 1x + 2f + 1xs app(app(union(), empty()), h) -> h 0 + 1h >= 1h app(app(union(), app(app(app(edge(), x), y), i)), h) -> app(app(app(edge(), x), y), app(app(union(), i), h)) 1 + 1x + 1y + 1h + 1i >= 1 + 1x + 1y + 1h + 1i app(app(or(), false()), y) -> y 0 + 1y >= 1y app(app(or(), true()), y) -> true() 0 + 1y >= 0 app(app(eq(), 0()), 0()) -> true() 2 >= 0 app(app(eq(), 0()), app(s(), x)) -> false() 2 + 1x >= 0 app(app(eq(), app(s(), x)), 0()) -> false() 2 + 1x >= 0 app(app(eq(), app(s(), x)), app(s(), y)) -> app(app(eq(), x), y) 2 + 1x + 1y >= 0 + 1x + 1y app(app(app(app(filter2(), false()), f), x), xs) -> app(app(filter(), f), xs) 0 + 1x + 1f + 1xs >= 0 + 1f + 1xs app(app(app(app(filter2(), true()), f), x), xs) -> app(app(cons(), x), app(app(filter(), f), xs)) 0 + 1x + 1f + 1xs >= 0 + 1x + 1f + 1xs app(app(app(app(reach(), x), y), empty()), h) -> false() 0 + 1x + 1y + 1h >= 0 app(app(app(app(reach(), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_1(), app(app(eq(), x), u)), x), y), app(app(app(edge(), u), v), i)), h) 1 + 1x + 1y + 1h + 1i + 1u + 1v >= 2 + 2x + 1y + 1h + 1i + 2u + 1v app(app(app(app(app(if_reach_2(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(or(), app(app(app(app(reach(), x), y), i), h)), app(app(app(app(reach(), v), y), app(app(union(), i), h)), empty())) 2 + 1x + 1y + 1h + 1i + 1u + 1v >= 0 + 1x + 2y + 2h + 2i + 1v app(app(app(app(app(if_reach_2(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> true() 2 + 1x + 1y + 1h + 1i + 1u + 1v >= 0 app(app(app(app(app(if_reach_1(), false()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(reach(), x), y), i), app(app(app(edge(), u), v), h)) 2 + 1x + 1y + 1h + 1i + 1u + 1v >= 1 + 1x + 1y + 1h + 1i + 1u + 1v app(app(app(app(app(if_reach_1(), true()), x), y), app(app(app(edge(), u), v), i)), h) -> app(app(app(app(app(if_reach_2(), app(app(eq(), y), v)), x), y), app(app(app(edge(), u), v), i)), h) 2 + 1x + 1y + 1h + 1i + 1u + 1v >= 2 + 1x + 2y + 1h + 1i + 1u + 2v Qed