YES Time: 0.075305 TRS: { app(app(app(app(filter2(), true()), fun), x), xs) -> app(app(cons(), x), app(app(filter(), fun), xs)), app(app(app(app(filter2(), false()), fun), x), xs) -> app(app(filter(), fun), xs), app(app(map(), fun), app(app(cons(), x), xs)) -> app(app(cons(), app(fun, x)), app(app(map(), fun), xs)), app(app(map(), fun), nil()) -> nil(), app(app(filter(), fun), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(fun, x)), fun), x), xs), app(app(filter(), fun), nil()) -> nil(), app(f(), app(g(), x)) -> app(g(), app(g(), app(g(), x))), app(f(), app(g(), x)) -> app(g(), app(g(), app(f(), x)))} DP: DP: { app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(cons(), x), app(app(filter(), fun), xs)), app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(cons(), x), app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(filter(), fun), app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(filter(), fun), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(map(), fun), xs), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(cons(), app(fun, x)), app(app(map(), fun), xs)), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(cons(), app(fun, x)), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(fun, x)), fun), x), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(fun, x)), fun), x), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(filter2(), app(fun, x)), fun), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(filter2(), app(fun, x)), app#(f(), app(g(), x)) -> app#(g(), app(g(), x)), app#(f(), app(g(), x)) -> app#(g(), app(g(), app(g(), x))), app#(f(), app(g(), x)) -> app#(g(), app(g(), app(f(), x))), app#(f(), app(g(), x)) -> app#(g(), app(f(), x)), app#(f(), app(g(), x)) -> app#(f(), x)} TRS: { app(app(app(app(filter2(), true()), fun), x), xs) -> app(app(cons(), x), app(app(filter(), fun), xs)), app(app(app(app(filter2(), false()), fun), x), xs) -> app(app(filter(), fun), xs), app(app(map(), fun), app(app(cons(), x), xs)) -> app(app(cons(), app(fun, x)), app(app(map(), fun), xs)), app(app(map(), fun), nil()) -> nil(), app(app(filter(), fun), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(fun, x)), fun), x), xs), app(app(filter(), fun), nil()) -> nil(), app(f(), app(g(), x)) -> app(g(), app(g(), app(g(), x))), app(f(), app(g(), x)) -> app(g(), app(g(), app(f(), x)))} UR: { app(app(app(app(filter2(), true()), fun), x), xs) -> app(app(cons(), x), app(app(filter(), fun), xs)), app(app(app(app(filter2(), false()), fun), x), xs) -> app(app(filter(), fun), xs), app(app(map(), fun), app(app(cons(), x), xs)) -> app(app(cons(), app(fun, x)), app(app(map(), fun), xs)), app(app(map(), fun), nil()) -> nil(), app(app(filter(), fun), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(fun, x)), fun), x), xs), app(app(filter(), fun), nil()) -> nil(), app(f(), app(g(), x)) -> app(g(), app(g(), app(g(), x))), app(f(), app(g(), x)) -> app(g(), app(g(), app(f(), x))), a(y, z) -> y, a(y, z) -> z} EDG: {(app#(f(), app(g(), x)) -> app#(f(), x), app#(f(), app(g(), x)) -> app#(f(), x)) (app#(f(), app(g(), x)) -> app#(f(), x), app#(f(), app(g(), x)) -> app#(g(), app(f(), x))) (app#(f(), app(g(), x)) -> app#(f(), x), app#(f(), app(g(), x)) -> app#(g(), app(g(), app(f(), x)))) (app#(f(), app(g(), x)) -> app#(f(), x), app#(f(), app(g(), x)) -> app#(g(), app(g(), app(g(), x)))) (app#(f(), app(g(), x)) -> app#(f(), x), app#(f(), app(g(), x)) -> app#(g(), app(g(), x))) (app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(filter2(), app(fun, x))) (app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(filter2(), app(fun, x)), fun)) (app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(fun, x)), fun), x)) (app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(fun, x)), fun), x), xs)) (app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(f(), app(g(), x)) -> app#(f(), x)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(f(), app(g(), x)) -> app#(g(), app(f(), x))) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(f(), app(g(), x)) -> app#(g(), app(g(), app(f(), x)))) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(f(), app(g(), x)) -> app#(g(), app(g(), app(g(), x)))) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(f(), app(g(), x)) -> app#(g(), app(g(), x))) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(filter2(), app(fun, x))) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(filter2(), app(fun, x)), fun)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(fun, x)), fun), x)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(fun, x)), fun), x), xs)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(cons(), app(fun, x))) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(cons(), app(fun, x)), app(app(map(), fun), xs))) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(map(), fun), xs)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(filter(), fun)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(app(filter(), fun), xs)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(filter(), fun)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(cons(), x)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(filter(), fun), xs)) (app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(cons(), x), app(app(filter(), fun), xs))) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(cons(), x), app(app(filter(), fun), xs))) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(filter(), fun), xs)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(cons(), x)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(filter(), fun)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(app(filter(), fun), xs)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(filter(), fun)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(map(), fun), xs)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(cons(), app(fun, x)), app(app(map(), fun), xs))) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(cons(), app(fun, x))) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(fun, x)), fun), x), xs)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(fun, x)), fun), x)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(filter2(), app(fun, x)), fun)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(filter2(), app(fun, x))) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(f(), app(g(), x)) -> app#(g(), app(g(), x))) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(f(), app(g(), x)) -> app#(g(), app(g(), app(g(), x)))) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(f(), app(g(), x)) -> app#(g(), app(g(), app(f(), x)))) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(f(), app(g(), x)) -> app#(g(), app(f(), x))) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(f(), app(g(), x)) -> app#(f(), x)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(map(), fun), xs), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(map(), fun), xs), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(map(), fun), xs)) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(map(), fun), xs), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(cons(), app(fun, x)), app(app(map(), fun), xs))) (app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(map(), fun), xs), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(cons(), app(fun, x))) (app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x)) (app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(app(app(filter2(), app(fun, x)), fun), x), xs)) (app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(app(filter2(), app(fun, x)), fun), x)) (app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(app(filter2(), app(fun, x)), fun)) (app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(filter2(), app(fun, x)))} STATUS: arrows: 0.852500 SCCS (2): Scc: { app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(map(), fun), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x)} Scc: {app#(f(), app(g(), x)) -> app#(f(), x)} SCC (5): Strict: { app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(app(filter(), fun), xs), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x), app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(map(), fun), xs), app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x)} Weak: { app(app(app(app(filter2(), true()), fun), x), xs) -> app(app(cons(), x), app(app(filter(), fun), xs)), app(app(app(app(filter2(), false()), fun), x), xs) -> app(app(filter(), fun), xs), app(app(map(), fun), app(app(cons(), x), xs)) -> app(app(cons(), app(fun, x)), app(app(map(), fun), xs)), app(app(map(), fun), nil()) -> nil(), app(app(filter(), fun), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(fun, x)), fun), x), xs), app(app(filter(), fun), nil()) -> nil(), app(f(), app(g(), x)) -> app(g(), app(g(), app(g(), x))), app(f(), app(g(), x)) -> app(g(), app(g(), app(f(), x)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app](x0, x1) = x0 + x1, [g] = 0, [f] = 0, [nil] = 0, [map] = 0, [cons] = 1, [filter] = 0, [filter2] = 0, [true] = 0, [false] = 0, [app#](x0, x1) = x0 Strict: app#(app(filter(), fun), app(app(cons(), x), xs)) -> app#(fun, x) 1 + 1x + 0fun + 1xs >= 0 + 1x + 0fun app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(app(map(), fun), xs) 1 + 1x + 0fun + 1xs >= 0 + 0fun + 1xs app#(app(map(), fun), app(app(cons(), x), xs)) -> app#(fun, x) 1 + 1x + 0fun + 1xs >= 0 + 1x + 0fun app#(app(app(app(filter2(), false()), fun), x), xs) -> app#(app(filter(), fun), xs) 0 + 0x + 0fun + 1xs >= 0 + 0fun + 1xs app#(app(app(app(filter2(), true()), fun), x), xs) -> app#(app(filter(), fun), xs) 0 + 0x + 0fun + 1xs >= 0 + 0fun + 1xs Weak: app(f(), app(g(), x)) -> app(g(), app(g(), app(f(), x))) 0 + 1x >= 0 + 1x app(f(), app(g(), x)) -> app(g(), app(g(), app(g(), x))) 0 + 1x >= 0 + 1x app(app(filter(), fun), nil()) -> nil() 0 + 1fun >= 0 app(app(filter(), fun), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(fun, x)), fun), x), xs) 1 + 1x + 1fun + 1xs >= 0 + 2x + 2fun + 1xs app(app(map(), fun), nil()) -> nil() 0 + 1fun >= 0 app(app(map(), fun), app(app(cons(), x), xs)) -> app(app(cons(), app(fun, x)), app(app(map(), fun), xs)) 1 + 1x + 1fun + 1xs >= 1 + 1x + 2fun + 1xs app(app(app(app(filter2(), false()), fun), x), xs) -> app(app(filter(), fun), xs) 0 + 1x + 1fun + 1xs >= 0 + 1fun + 1xs app(app(app(app(filter2(), true()), fun), x), xs) -> app(app(cons(), x), app(app(filter(), fun), xs)) 0 + 1x + 1fun + 1xs >= 1 + 1x + 1fun + 1xs SCCS (0): SCC (1): Strict: {app#(f(), app(g(), x)) -> app#(f(), x)} Weak: { app(app(app(app(filter2(), true()), fun), x), xs) -> app(app(cons(), x), app(app(filter(), fun), xs)), app(app(app(app(filter2(), false()), fun), x), xs) -> app(app(filter(), fun), xs), app(app(map(), fun), app(app(cons(), x), xs)) -> app(app(cons(), app(fun, x)), app(app(map(), fun), xs)), app(app(map(), fun), nil()) -> nil(), app(app(filter(), fun), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(fun, x)), fun), x), xs), app(app(filter(), fun), nil()) -> nil(), app(f(), app(g(), x)) -> app(g(), app(g(), app(g(), x))), app(f(), app(g(), x)) -> app(g(), app(g(), app(f(), x)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [app](x0, x1) = x0 + x1, [g] = 1, [f] = 1, [nil] = 0, [map] = 0, [cons] = 0, [filter] = 0, [filter2] = 0, [true] = 0, [false] = 0, [app#](x0, x1) = x0 + x1 Strict: app#(f(), app(g(), x)) -> app#(f(), x) 2 + 1x >= 1 + 1x Weak: app(f(), app(g(), x)) -> app(g(), app(g(), app(f(), x))) 2 + 1x >= 3 + 1x app(f(), app(g(), x)) -> app(g(), app(g(), app(g(), x))) 2 + 1x >= 3 + 1x app(app(filter(), fun), nil()) -> nil() 0 + 1fun >= 0 app(app(filter(), fun), app(app(cons(), x), xs)) -> app(app(app(app(filter2(), app(fun, x)), fun), x), xs) 0 + 1x + 1fun + 1xs >= 0 + 2x + 2fun + 1xs app(app(map(), fun), nil()) -> nil() 0 + 1fun >= 0 app(app(map(), fun), app(app(cons(), x), xs)) -> app(app(cons(), app(fun, x)), app(app(map(), fun), xs)) 0 + 1x + 1fun + 1xs >= 0 + 1x + 2fun + 1xs app(app(app(app(filter2(), false()), fun), x), xs) -> app(app(filter(), fun), xs) 0 + 1x + 1fun + 1xs >= 0 + 1fun + 1xs app(app(app(app(filter2(), true()), fun), x), xs) -> app(app(cons(), x), app(app(filter(), fun), xs)) 0 + 1x + 1fun + 1xs >= 0 + 1x + 1fun + 1xs Qed