MAYBE Time: 0.019623 TRS: { app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, app(app(times(), app(s(), x)), y) -> app(app(plus(), app(app(times(), x), y)), y), app(app(times(), 0()), y) -> 0(), 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(inc(), xs) -> app(app(map(), app(plus(), app(s(), 0()))), xs), app(double(), xs) -> app(app(map(), app(times(), app(s(), app(s(), 0())))), xs)} DP: DP: { app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y)), app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y), app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(plus(), app(app(times(), x), y)), app#(app(times(), app(s(), x)), y) -> app#(times(), 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#(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#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(inc(), xs) -> app#(plus(), app(s(), 0())), app#(inc(), xs) -> app#(s(), 0()), app#(inc(), xs) -> app#(map(), app(plus(), app(s(), 0()))), app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(double(), xs) -> app#(s(), app(s(), 0())), app#(double(), xs) -> app#(s(), 0()), app#(double(), xs) -> app#(times(), app(s(), app(s(), 0()))), app#(double(), xs) -> app#(map(), app(times(), app(s(), app(s(), 0()))))} TRS: { app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, app(app(times(), app(s(), x)), y) -> app(app(plus(), app(app(times(), x), y)), y), app(app(times(), 0()), y) -> 0(), 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(inc(), xs) -> app(app(map(), app(plus(), app(s(), 0()))), xs), app(double(), xs) -> app(app(map(), app(times(), app(s(), app(s(), 0())))), xs)} 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#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x))) (app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(map(), app(times(), app(s(), app(s(), 0()))))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(times(), app(s(), app(s(), 0())))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(s(), 0())) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(s(), app(s(), 0()))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(inc(), xs) -> app#(map(), app(plus(), app(s(), 0())))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(inc(), xs) -> app#(s(), 0())) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(inc(), xs) -> app#(plus(), app(s(), 0()))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), 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(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(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(times(), app(s(), x)), y) -> app#(times(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(times(), app(s(), x)), y) -> app#(plus(), app(app(times(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y)) (app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y)) (app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(plus(), app(app(times(), x), y))) (app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(times(), x)) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))} 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#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x))) (app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(map(), app(times(), app(s(), app(s(), 0()))))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(times(), app(s(), app(s(), 0())))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(s(), 0())) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(s(), app(s(), 0()))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(inc(), xs) -> app#(map(), app(plus(), app(s(), 0())))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(inc(), xs) -> app#(s(), 0())) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(inc(), xs) -> app#(plus(), app(s(), 0()))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), 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(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(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(times(), app(s(), x)), y) -> app#(times(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(times(), app(s(), x)), y) -> app#(plus(), app(app(times(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y)) (app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y)) (app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(plus(), app(app(times(), x), y))) (app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(times(), x)) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))} 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#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x))) (app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(map(), app(times(), app(s(), app(s(), 0()))))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(times(), app(s(), app(s(), 0())))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(s(), 0())) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(s(), app(s(), 0()))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(inc(), xs) -> app#(map(), app(plus(), app(s(), 0())))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(inc(), xs) -> app#(s(), 0())) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(inc(), xs) -> app#(plus(), app(s(), 0()))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), 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(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(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(times(), app(s(), x)), y) -> app#(times(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(times(), app(s(), x)), y) -> app#(plus(), app(app(times(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(app(plus(), app(app(times(), x), y)), y)) (app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y)) (app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(plus(), app(app(times(), x), y))) (app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y), app#(app(times(), app(s(), x)), y) -> app#(times(), x)) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(plus(), x)) (app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y), app#(app(plus(), app(s(), x)), y) -> app#(s(), app(app(plus(), x), y))) (app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(f, x)) (app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(map(), f), xs)) (app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(app(cons(), app(f, x)), app(app(map(), f), xs))) (app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(app(map(), f), app(app(cons(), x), xs)) -> app#(cons(), app(f, x)))} STATUS: arrows: 0.895000 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), app#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs)} Scc: {app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y)} Scc: {app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)} SCC (4): 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#(inc(), xs) -> app#(app(map(), app(plus(), app(s(), 0()))), xs), app#(double(), xs) -> app#(app(map(), app(times(), app(s(), app(s(), 0())))), xs)} Weak: { app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, app(app(times(), app(s(), x)), y) -> app(app(plus(), app(app(times(), x), y)), y), app(app(times(), 0()), y) -> 0(), 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(inc(), xs) -> app(app(map(), app(plus(), app(s(), 0()))), xs), app(double(), xs) -> app(app(map(), app(times(), app(s(), app(s(), 0())))), xs)} Open SCC (1): Strict: {app#(app(times(), app(s(), x)), y) -> app#(app(times(), x), y)} Weak: { app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, app(app(times(), app(s(), x)), y) -> app(app(plus(), app(app(times(), x), y)), y), app(app(times(), 0()), y) -> 0(), 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(inc(), xs) -> app(app(map(), app(plus(), app(s(), 0()))), xs), app(double(), xs) -> app(app(map(), app(times(), app(s(), app(s(), 0())))), xs)} Open SCC (1): Strict: {app#(app(plus(), app(s(), x)), y) -> app#(app(plus(), x), y)} Weak: { app(app(plus(), app(s(), x)), y) -> app(s(), app(app(plus(), x), y)), app(app(plus(), 0()), y) -> y, app(app(times(), app(s(), x)), y) -> app(app(plus(), app(app(times(), x), y)), y), app(app(times(), 0()), y) -> 0(), 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(inc(), xs) -> app(app(map(), app(plus(), app(s(), 0()))), xs), app(double(), xs) -> app(app(map(), app(times(), app(s(), app(s(), 0())))), xs)} Open