MAYBE Time: 3.118985 TRS: { app(app(map(), f), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app(app(div(), app(s(), x)), app(s(), y)) -> app(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))), app(app(div(), 0()), app(s(), y)) -> 0(), app(p(), app(s(), x)) -> x} DP: DP: {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(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), app(p(), app(s(), x))), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), x)), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), y)), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(minus(), x), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(div(), app(app(minus(), x), y))} TRS: { app(app(map(), f), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app(app(div(), app(s(), x)), app(s(), y)) -> app(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))), app(app(div(), 0()), app(s(), y)) -> 0(), app(p(), app(s(), x)) -> x} UR: { app(app(map(), f), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app(app(div(), app(s(), x)), app(s(), y)) -> app(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))), app(app(div(), 0()), app(s(), y)) -> 0(), app(p(), app(s(), x)) -> x, a(z, w) -> z, a(z, w) -> w} EDG: {(app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), y))) (app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), x))) (app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), app(p(), app(s(), x)))) (app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y)))) (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), y))) (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), x))) (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), app(p(), app(s(), x)))) (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y)))) (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y)) (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y))) (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(minus(), x)) (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y)))) (app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y)), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(div(), app(app(minus(), x), y))) (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(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(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(minus(), app(p(), app(s(), x)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), x))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(p(), app(s(), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(minus(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(minus(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(div(), app(s(), x)), app(s(), y)) -> app#(div(), app(app(minus(), x), y)))} STATUS: arrows: 0.822485 SCCS (3): 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(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y))} Scc: {app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y)))} SCC (2): 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(map(), f), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app(app(div(), app(s(), x)), app(s(), y)) -> app(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))), app(app(div(), 0()), app(s(), y)) -> 0(), app(p(), app(s(), x)) -> x} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app](x0, x1) = x0 + x1, [nil] = 0, [map] = 0, [cons] = 1, [minus] = 0, [0] = 0, [p] = 1, [s] = 1, [div] = 0, [app#](x0, x1) = x0 + 1 Strict: app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs) 2 + 0f + 1x + 1xs >= 1 + 0f + 1xs app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x) 2 + 0f + 1x + 1xs >= 1 + 0f + 1x Weak: app(p(), app(s(), x)) -> x 2 + 1x >= 1x app(app(div(), 0()), app(s(), y)) -> 0() 1 + 1y >= 0 app(app(div(), app(s(), x)), app(s(), y)) -> app(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))) 2 + 1x + 1y >= 2 + 1x + 2y app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))) 2 + 1x + 1y >= 4 + 1x + 1y app(app(minus(), x), 0()) -> x 0 + 1x >= 1x app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)) 1 + 1f + 1x + 1xs >= 1 + 2f + 1x + 1xs app(app(map(), f), nil()) -> nil() 0 + 1f >= 0 Qed SCC (1): Strict: {app#(app(div(), app(s(), x)), app(s(), y)) -> app#(app(div(), app(app(minus(), x), y)), app(s(), y))} Weak: { app(app(map(), f), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app(app(div(), app(s(), x)), app(s(), y)) -> app(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))), app(app(div(), 0()), app(s(), y)) -> 0(), app(p(), app(s(), x)) -> x} Fail SCC (1): Strict: {app#(app(minus(), app(s(), x)), app(s(), y)) -> app#(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y)))} Weak: { app(app(map(), f), nil()) -> nil(), app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)), app(app(minus(), x), 0()) -> x, app(app(minus(), app(s(), x)), app(s(), y)) -> app(app(minus(), app(p(), app(s(), x))), app(p(), app(s(), y))), app(app(div(), app(s(), x)), app(s(), y)) -> app(s(), app(app(div(), app(app(minus(), x), y)), app(s(), y))), app(app(div(), 0()), app(s(), y)) -> 0(), app(p(), app(s(), x)) -> x} Fail