MAYBE Time: 30.264348 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(append(), xs), nil()) -> xs, app(app(append(), nil()), ys) -> ys, app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)), app(app(zip(), xss), nil()) -> xss, app(app(zip(), nil()), yss) -> yss, app(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)), app(app(combine(), xs), nil()) -> xs, app(app(combine(), xs), app(app(cons(), ys), yss)) -> app(app(combine(), app(app(zip(), xs), ys)), yss), app(levels(), app(app(node(), x), xs)) -> app(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs)))} 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(append(), app(app(cons(), x), xs)), ys) -> app#(app(cons(), x), app(app(append(), xs), ys)), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(append(), xs), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(append(), xs), ys), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(cons(), app(app(append(), xs), ys)), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(append(), xs), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(zip(), xss), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(zip(), xs), ys), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(combine(), app(app(zip(), xs), ys)), yss), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(zip(), xs), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(combine(), app(app(zip(), xs), ys)), app#(levels(), app(app(node(), x), xs)) -> app#(app(map(), levels()), xs), app#(levels(), app(app(node(), x), xs)) -> app#(app(cons(), x), nil()), app#(levels(), app(app(node(), x), xs)) -> app#(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs))), app#(levels(), app(app(node(), x), xs)) -> app#(app(combine(), nil()), app(app(map(), levels()), xs)), app#(levels(), app(app(node(), x), xs)) -> app#(map(), levels()), app#(levels(), app(app(node(), x), xs)) -> app#(cons(), x), app#(levels(), app(app(node(), x), xs)) -> app#(cons(), app(app(cons(), x), nil())), app#(levels(), app(app(node(), x), xs)) -> app#(combine(), nil())} 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(append(), xs), nil()) -> xs, app(app(append(), nil()), ys) -> ys, app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)), app(app(zip(), xss), nil()) -> xss, app(app(zip(), nil()), yss) -> yss, app(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)), app(app(combine(), xs), nil()) -> xs, app(app(combine(), xs), app(app(cons(), ys), yss)) -> app(app(combine(), app(app(zip(), xs), ys)), yss), app(levels(), app(app(node(), x), xs)) -> app(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs)))} 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(append(), xs), nil()) -> xs, app(app(append(), nil()), ys) -> ys, app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)), app(app(zip(), xss), nil()) -> xss, app(app(zip(), nil()), yss) -> yss, app(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)), app(app(combine(), xs), nil()) -> xs, app(app(combine(), xs), app(app(cons(), ys), yss)) -> app(app(combine(), app(app(zip(), xs), ys)), yss), app(levels(), app(app(node(), x), xs)) -> app(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs))), a(y, z) -> y, a(y, z) -> z} EDG: {(app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(levels(), app(app(node(), x), xs)) -> app#(app(combine(), nil()), app(app(map(), levels()), xs)), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(combine(), app(app(zip(), xs), ys))) (app#(levels(), app(app(node(), x), xs)) -> app#(app(combine(), nil()), app(app(map(), levels()), xs)), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(zip(), xs)) (app#(levels(), app(app(node(), x), xs)) -> app#(app(combine(), nil()), app(app(map(), levels()), xs)), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(combine(), app(app(zip(), xs), ys)), yss)) (app#(levels(), app(app(node(), x), xs)) -> app#(app(combine(), nil()), app(app(map(), levels()), xs)), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(zip(), xs), ys)) (app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(combine(), app(app(zip(), xs), ys)), yss), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(combine(), app(app(zip(), xs), ys))) (app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(combine(), app(app(zip(), xs), ys)), yss), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(zip(), xs)) (app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(combine(), app(app(zip(), xs), ys)), yss), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(combine(), app(app(zip(), xs), ys)), yss)) (app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(combine(), app(app(zip(), xs), ys)), yss), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(zip(), xs), ys)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(levels(), app(app(node(), x), xs)) -> app#(combine(), nil())) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(levels(), app(app(node(), x), xs)) -> app#(cons(), app(app(cons(), x), nil()))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(levels(), app(app(node(), x), xs)) -> app#(cons(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(levels(), app(app(node(), x), xs)) -> app#(map(), levels())) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(levels(), app(app(node(), x), xs)) -> app#(app(combine(), nil()), app(app(map(), levels()), xs))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(levels(), app(app(node(), x), xs)) -> app#(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs)))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(levels(), app(app(node(), x), xs)) -> app#(app(cons(), x), nil())) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(levels(), app(app(node(), x), xs)) -> app#(app(map(), levels()), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(combine(), app(app(zip(), xs), ys))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(zip(), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(combine(), app(app(zip(), xs), ys)), yss)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(zip(), xs), ys)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(zip(), xss)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(append(), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(cons(), app(app(append(), xs), ys))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(append(), xs), ys)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(append(), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(cons(), x), app(app(append(), xs), ys))) (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(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#(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(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(append(), xs)) (app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys)) (app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(cons(), x), app(app(append(), xs), ys))) (app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(zip(), xs), ys), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss))) (app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(zip(), xs), ys), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(append(), xs), ys)) (app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(zip(), xs), ys), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss)) (app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(zip(), xs), ys), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(cons(), app(app(append(), xs), ys))) (app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(zip(), xs), ys), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(append(), xs)) (app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(zip(), xs), ys), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(zip(), xss)) (app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(cons(), x), app(app(append(), xs), ys))) (app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys)) (app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys), app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(append(), xs)) (app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss))) (app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(append(), xs), ys)) (app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss)) (app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(cons(), app(app(append(), xs), ys))) (app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(append(), xs)) (app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss), app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(zip(), xss)) (app#(levels(), app(app(node(), x), xs)) -> app#(app(map(), levels()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(levels(), app(app(node(), x), xs)) -> app#(app(map(), levels()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(levels(), app(app(node(), x), xs)) -> app#(app(map(), levels()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(levels(), app(app(node(), x), xs)) -> app#(app(map(), levels()), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))} STATUS: arrows: 0.905600 SCCS (4): 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), app#(levels(), app(app(node(), x), xs)) -> app#(app(map(), levels()), xs)} Scc: {app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(combine(), app(app(zip(), xs), ys)), yss)} Scc: {app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss)} Scc: {app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys)} SCC (3): 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), app#(levels(), app(app(node(), x), xs)) -> app#(app(map(), levels()), 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(append(), xs), nil()) -> xs, app(app(append(), nil()), ys) -> ys, app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)), app(app(zip(), xss), nil()) -> xss, app(app(zip(), nil()), yss) -> yss, app(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)), app(app(combine(), xs), nil()) -> xs, app(app(combine(), xs), app(app(cons(), ys), yss)) -> app(app(combine(), app(app(zip(), xs), ys)), yss), app(levels(), app(app(node(), x), xs)) -> app(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app](x0, x1) = x0 + x1, [nil] = 0, [map] = 0, [cons] = 0, [append] = 0, [zip] = 0, [combine] = 0, [levels] = 0, [node] = 1, [app#](x0, x1) = x0 Strict: app#(levels(), app(app(node(), x), xs)) -> app#(app(map(), levels()), xs) 1 + 1x + 1xs >= 0 + 1xs app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs) 0 + 0f + 1x + 1xs >= 0 + 0f + 1xs app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x) 0 + 0f + 1x + 1xs >= 0 + 0f + 1x Weak: app(levels(), app(app(node(), x), xs)) -> app(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs))) 1 + 1x + 1xs >= 0 + 1x + 1xs app(app(combine(), xs), app(app(cons(), ys), yss)) -> app(app(combine(), app(app(zip(), xs), ys)), yss) 0 + 1xs + 1ys + 1yss >= 0 + 1xs + 1ys + 1yss app(app(combine(), xs), nil()) -> xs 0 + 1xs >= 1xs app(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)) 0 + 1xs + 1ys + 1yss + 1xss >= 0 + 1xs + 1ys + 1yss + 1xss app(app(zip(), nil()), yss) -> yss 0 + 1yss >= 1yss app(app(zip(), xss), nil()) -> xss 0 + 1xss >= 1xss app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)) 0 + 1x + 1xs + 1ys >= 0 + 1x + 1xs + 1ys app(app(append(), nil()), ys) -> ys 0 + 1ys >= 1ys app(app(append(), xs), nil()) -> xs 0 + 1xs >= 1xs app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)) 0 + 1f + 1x + 1xs >= 0 + 2f + 1x + 1xs app(app(map(), f), nil()) -> nil() 0 + 1f >= 0 SCCS (1): 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 (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(append(), xs), nil()) -> xs, app(app(append(), nil()), ys) -> ys, app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)), app(app(zip(), xss), nil()) -> xss, app(app(zip(), nil()), yss) -> yss, app(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)), app(app(combine(), xs), nil()) -> xs, app(app(combine(), xs), app(app(cons(), ys), yss)) -> app(app(combine(), app(app(zip(), xs), ys)), yss), app(levels(), app(app(node(), x), xs)) -> app(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs)))} 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, [append] = 0, [zip] = 0, [combine] = 0, [levels] = 0, [node] = 0, [app#](x0, x1) = x0 Strict: app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs) 1 + 0f + 1x + 1xs >= 0 + 0f + 1xs app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x) 1 + 0f + 1x + 1xs >= 0 + 0f + 1x Weak: app(levels(), app(app(node(), x), xs)) -> app(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs))) 0 + 1x + 1xs >= 2 + 1x + 1xs app(app(combine(), xs), app(app(cons(), ys), yss)) -> app(app(combine(), app(app(zip(), xs), ys)), yss) 1 + 1xs + 1ys + 1yss >= 0 + 1xs + 1ys + 1yss app(app(combine(), xs), nil()) -> xs 0 + 1xs >= 1xs app(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)) 2 + 1xs + 1ys + 1yss + 1xss >= 1 + 1xs + 1ys + 1yss + 1xss app(app(zip(), nil()), yss) -> yss 0 + 1yss >= 1yss app(app(zip(), xss), nil()) -> xss 0 + 1xss >= 1xss app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)) 1 + 1x + 1xs + 1ys >= 1 + 1x + 1xs + 1ys app(app(append(), nil()), ys) -> ys 0 + 1ys >= 1ys app(app(append(), xs), nil()) -> xs 0 + 1xs >= 1xs 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(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(combine(), app(app(zip(), xs), ys)), yss)} 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(append(), xs), nil()) -> xs, app(app(append(), nil()), ys) -> ys, app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)), app(app(zip(), xss), nil()) -> xss, app(app(zip(), nil()), yss) -> yss, app(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)), app(app(combine(), xs), nil()) -> xs, app(app(combine(), xs), app(app(cons(), ys), yss)) -> app(app(combine(), app(app(zip(), xs), ys)), yss), app(levels(), app(app(node(), x), xs)) -> app(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs)))} 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, [append] = 0, [zip] = 0, [combine] = 0, [levels] = 0, [node] = 0, [app#](x0, x1) = x0 Strict: app#(app(combine(), xs), app(app(cons(), ys), yss)) -> app#(app(combine(), app(app(zip(), xs), ys)), yss) 1 + 0xs + 1ys + 1yss >= 0 + 0xs + 0ys + 1yss Weak: app(levels(), app(app(node(), x), xs)) -> app(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs))) 0 + 1x + 1xs >= 2 + 1x + 1xs app(app(combine(), xs), app(app(cons(), ys), yss)) -> app(app(combine(), app(app(zip(), xs), ys)), yss) 1 + 1xs + 1ys + 1yss >= 0 + 1xs + 1ys + 1yss app(app(combine(), xs), nil()) -> xs 0 + 1xs >= 1xs app(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)) 2 + 1xs + 1ys + 1yss + 1xss >= 1 + 1xs + 1ys + 1yss + 1xss app(app(zip(), nil()), yss) -> yss 0 + 1yss >= 1yss app(app(zip(), xss), nil()) -> xss 0 + 1xss >= 1xss app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)) 1 + 1x + 1xs + 1ys >= 1 + 1x + 1xs + 1ys app(app(append(), nil()), ys) -> ys 0 + 1ys >= 1ys app(app(append(), xs), nil()) -> xs 0 + 1xs >= 1xs 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(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss)} 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(append(), xs), nil()) -> xs, app(app(append(), nil()), ys) -> ys, app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)), app(app(zip(), xss), nil()) -> xss, app(app(zip(), nil()), yss) -> yss, app(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)), app(app(combine(), xs), nil()) -> xs, app(app(combine(), xs), app(app(cons(), ys), yss)) -> app(app(combine(), app(app(zip(), xs), ys)), yss), app(levels(), app(app(node(), x), xs)) -> app(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app](x0, x1) = x0 + 1, [nil] = 1, [map] = 0, [cons] = 0, [append] = 0, [zip] = 0, [combine] = 0, [levels] = 1, [node] = 0, [app#](x0, x1) = x0 + 1 Strict: app#(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app#(app(zip(), xss), yss) 2 + 0xs + 0ys + 1yss + 0xss >= 1 + 1yss + 0xss Weak: app(levels(), app(app(node(), x), xs)) -> app(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs))) 2 + 0x + 1xs >= 3 + 0x + 1xs app(app(combine(), xs), app(app(cons(), ys), yss)) -> app(app(combine(), app(app(zip(), xs), ys)), yss) 2 + 0xs + 0ys + 1yss >= 1 + 0xs + 0ys + 1yss app(app(combine(), xs), nil()) -> xs 2 + 0xs >= 1xs app(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)) 2 + 0xs + 0ys + 1yss + 0xss >= 2 + 0xs + 0ys + 1yss + 0xss app(app(zip(), nil()), yss) -> yss 1 + 1yss >= 1yss app(app(zip(), xss), nil()) -> xss 2 + 0xss >= 1xss app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)) 1 + 0x + 0xs + 1ys >= 2 + 0x + 0xs + 1ys app(app(append(), nil()), ys) -> ys 1 + 1ys >= 1ys app(app(append(), xs), nil()) -> xs 2 + 0xs >= 1xs app(app(map(), f), app(app(cons(), x), xs)) -> app(app(cons(), app(f, x)), app(app(map(), f), xs)) 2 + 0f + 0x + 1xs >= 2 + 0f + 0x + 1xs app(app(map(), f), nil()) -> nil() 2 + 0f >= 1 Qed SCC (1): Strict: {app#(app(append(), app(app(cons(), x), xs)), ys) -> app#(app(append(), xs), ys)} 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(append(), xs), nil()) -> xs, app(app(append(), nil()), ys) -> ys, app(app(append(), app(app(cons(), x), xs)), ys) -> app(app(cons(), x), app(app(append(), xs), ys)), app(app(zip(), xss), nil()) -> xss, app(app(zip(), nil()), yss) -> yss, app(app(zip(), app(app(cons(), xs), xss)), app(app(cons(), ys), yss)) -> app(app(cons(), app(app(append(), xs), ys)), app(app(zip(), xss), yss)), app(app(combine(), xs), nil()) -> xs, app(app(combine(), xs), app(app(cons(), ys), yss)) -> app(app(combine(), app(app(zip(), xs), ys)), yss), app(levels(), app(app(node(), x), xs)) -> app(app(cons(), app(app(cons(), x), nil())), app(app(combine(), nil()), app(app(map(), levels()), xs)))} Fail