MAYBE Time: 0.037031 TRS: {app(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app(app(app(app(fold(), f_3), g_2), x), nil()) -> x, app(app(app(uncurry(), f_2), x), y) -> app(app(f_2, x), y), app(app(app(swap(), f_2), y), x) -> app(app(f_2, x), y), app(app(app(compose(), g_1), f_1), x) -> app(g_1, app(f_1, x)), app(app(apply(), f_1), x) -> app(f_1, x), app(app(uncurry(), app(app(fold(), cons()), id())), nil()) -> id(), app(app(const(), x), y) -> x, app(id(), x) -> x, app(listify(), x) -> app(app(cons(), x), nil()), app(sum(), l) -> app(app(app(app(fold(), add()), id()), 0()), l), append() -> app(app(compose(), app(app(swap(), fold()), cons())), id()), reverse() -> app(app(uncurry(), app(app(fold(), app(swap(), append())), listify())), nil()), length() -> app(app(uncurry(), app(app(fold(), add()), app(cons(), 1()))), 0())} DP: DP: {app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(apply(), f_1), x) -> app#(f_1, x), app#(listify(), x) -> app#(app(cons(), x), nil()), app#(listify(), x) -> app#(cons(), x), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l), app#(sum(), l) -> app#(app(app(fold(), add()), id()), 0()), app#(sum(), l) -> app#(app(fold(), add()), id()), app#(sum(), l) -> app#(fold(), add()), append#() -> app#(app(swap(), fold()), cons()), append#() -> app#(app(compose(), app(app(swap(), fold()), cons())), id()), append#() -> app#(swap(), fold()), append#() -> app#(compose(), app(app(swap(), fold()), cons())), reverse#() -> app#(app(uncurry(), app(app(fold(), app(swap(), append())), listify())), nil()), reverse#() -> app#(app(fold(), app(swap(), append())), listify()), reverse#() -> app#(uncurry(), app(app(fold(), app(swap(), append())), listify())), reverse#() -> app#(swap(), append()), reverse#() -> app#(fold(), app(swap(), append())), reverse#() -> append#(), length#() -> app#(app(uncurry(), app(app(fold(), add()), app(cons(), 1()))), 0()), length#() -> app#(app(fold(), add()), app(cons(), 1())), length#() -> app#(uncurry(), app(app(fold(), add()), app(cons(), 1()))), length#() -> app#(cons(), 1()), length#() -> app#(fold(), add())} TRS: {app(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app(app(app(app(fold(), f_3), g_2), x), nil()) -> x, app(app(app(uncurry(), f_2), x), y) -> app(app(f_2, x), y), app(app(app(swap(), f_2), y), x) -> app(app(f_2, x), y), app(app(app(compose(), g_1), f_1), x) -> app(g_1, app(f_1, x)), app(app(apply(), f_1), x) -> app(f_1, x), app(app(uncurry(), app(app(fold(), cons()), id())), nil()) -> id(), app(app(const(), x), y) -> x, app(id(), x) -> x, app(listify(), x) -> app(app(cons(), x), nil()), app(sum(), l) -> app(app(app(app(fold(), add()), id()), 0()), l), append() -> app(app(compose(), app(app(swap(), fold()), cons())), id()), reverse() -> app(app(uncurry(), app(app(fold(), app(swap(), append())), listify())), nil()), length() -> app(app(uncurry(), app(app(fold(), add()), app(cons(), 1()))), 0())} EDG: { (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(sum(), l) -> app#(fold(), add())) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(sum(), l) -> app#(app(fold(), add()), id())) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(sum(), l) -> app#(app(app(fold(), add()), id()), 0())) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l)) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(listify(), x) -> app#(cons(), x)) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(listify(), x) -> app#(app(cons(), x), nil())) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(apply(), f_1), x) -> app#(f_1, x)) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x))) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x)) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y)) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x)) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y)) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x)) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t)) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t))) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z)) (app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z))) (app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t)) (app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t))) (app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z)) (app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z))) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(sum(), l) -> app#(fold(), add())) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(sum(), l) -> app#(app(fold(), add()), id())) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(sum(), l) -> app#(app(app(fold(), add()), id()), 0())) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(listify(), x) -> app#(cons(), x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(listify(), x) -> app#(app(cons(), x), nil())) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(apply(), f_1), x) -> app#(f_1, x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x))) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t))) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z))) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(sum(), l) -> app#(fold(), add())) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(sum(), l) -> app#(app(fold(), add()), id())) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(sum(), l) -> app#(app(app(fold(), add()), id()), 0())) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l)) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(listify(), x) -> app#(cons(), x)) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(listify(), x) -> app#(app(cons(), x), nil())) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(apply(), f_1), x) -> app#(f_1, x)) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x))) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x)) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y)) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x)) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y)) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x)) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t)) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t))) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z)) (app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z))) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(sum(), l) -> app#(fold(), add())) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(sum(), l) -> app#(app(fold(), add()), id())) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(sum(), l) -> app#(app(app(fold(), add()), id()), 0())) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l)) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(listify(), x) -> app#(cons(), x)) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(listify(), x) -> app#(app(cons(), x), nil())) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(app(apply(), f_1), x) -> app#(f_1, x)) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x))) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x)) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y)) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x)) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y)) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x)) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t)) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t))) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z)) (app#(app(apply(), f_1), x) -> app#(f_1, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z))) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t))) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z))) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z))) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t))) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x))) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(apply(), f_1), x) -> app#(f_1, x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(listify(), x) -> app#(app(cons(), x), nil())) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(listify(), x) -> app#(cons(), x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(sum(), l) -> app#(app(app(fold(), add()), id()), 0())) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(sum(), l) -> app#(app(fold(), add()), id())) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(sum(), l) -> app#(fold(), add())) (reverse#() -> append#(), append#() -> app#(app(swap(), fold()), cons())) (reverse#() -> append#(), append#() -> app#(app(compose(), app(app(swap(), fold()), cons())), id())) (reverse#() -> append#(), append#() -> app#(swap(), fold())) (reverse#() -> append#(), append#() -> app#(compose(), app(app(swap(), fold()), cons()))) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z))) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z)) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t))) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t)) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x)) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y)) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x)) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y)) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x)) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x))) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(apply(), f_1), x) -> app#(f_1, x)) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(listify(), x) -> app#(app(cons(), x), nil())) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(listify(), x) -> app#(cons(), x)) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l)) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(sum(), l) -> app#(app(app(fold(), add()), id()), 0())) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(sum(), l) -> app#(app(fold(), add()), id())) (app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(sum(), l) -> app#(fold(), add())) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z))) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z)) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t))) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t)) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x)) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y)) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x)) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y)) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x)) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x))) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(apply(), f_1), x) -> app#(f_1, x)) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(listify(), x) -> app#(app(cons(), x), nil())) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(listify(), x) -> app#(cons(), x)) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l)) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(sum(), l) -> app#(app(app(fold(), add()), id()), 0())) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(sum(), l) -> app#(app(fold(), add()), id())) (app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(sum(), l) -> app#(fold(), add())) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z))) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z)) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t))) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t)) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x)) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y)) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x)) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y)) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x)) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x))) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(apply(), f_1), x) -> app#(f_1, x)) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(listify(), x) -> app#(app(cons(), x), nil())) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(listify(), x) -> app#(cons(), x)) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l)) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(sum(), l) -> app#(app(app(fold(), add()), id()), 0())) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(sum(), l) -> app#(app(fold(), add()), id())) (app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(sum(), l) -> app#(fold(), add())) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z))) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t))) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x))) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(apply(), f_1), x) -> app#(f_1, x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(listify(), x) -> app#(app(cons(), x), nil())) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(listify(), x) -> app#(cons(), x)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l)) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(sum(), l) -> app#(app(app(fold(), add()), id()), 0())) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(sum(), l) -> app#(app(fold(), add()), id())) (app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(sum(), l) -> app#(fold(), add())) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z))) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z)) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t))) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t)) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x)) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y)) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x)) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y)) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x)) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x))) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(apply(), f_1), x) -> app#(f_1, x)) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(listify(), x) -> app#(app(cons(), x), nil())) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(listify(), x) -> app#(cons(), x)) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l)) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(sum(), l) -> app#(app(app(fold(), add()), id()), 0())) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(sum(), l) -> app#(app(fold(), add()), id())) (app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(sum(), l) -> app#(fold(), add())) } STATUS: arrows: 0.822266 SCCS (1): Scc: {app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(apply(), f_1), x) -> app#(f_1, x), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l)} SCC (12): Strict: {app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(f_3, app(g_2, z)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(g_2, z), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app#(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app#(app(app(app(fold(), f_3), g_2), x), t), app#(app(app(uncurry(), f_2), x), y) -> app#(f_2, x), app#(app(app(uncurry(), f_2), x), y) -> app#(app(f_2, x), y), app#(app(app(swap(), f_2), y), x) -> app#(f_2, x), app#(app(app(swap(), f_2), y), x) -> app#(app(f_2, x), y), app#(app(app(compose(), g_1), f_1), x) -> app#(f_1, x), app#(app(app(compose(), g_1), f_1), x) -> app#(g_1, app(f_1, x)), app#(app(apply(), f_1), x) -> app#(f_1, x), app#(sum(), l) -> app#(app(app(app(fold(), add()), id()), 0()), l)} Weak: {app(app(app(app(fold(), f_3), g_2), x), app(app(cons(), z), t)) -> app(app(f_3, app(g_2, z)), app(app(app(app(fold(), f_3), g_2), x), t)), app(app(app(app(fold(), f_3), g_2), x), nil()) -> x, app(app(app(uncurry(), f_2), x), y) -> app(app(f_2, x), y), app(app(app(swap(), f_2), y), x) -> app(app(f_2, x), y), app(app(app(compose(), g_1), f_1), x) -> app(g_1, app(f_1, x)), app(app(apply(), f_1), x) -> app(f_1, x), app(app(uncurry(), app(app(fold(), cons()), id())), nil()) -> id(), app(app(const(), x), y) -> x, app(id(), x) -> x, app(listify(), x) -> app(app(cons(), x), nil()), app(sum(), l) -> app(app(app(app(fold(), add()), id()), 0()), l), append() -> app(app(compose(), app(app(swap(), fold()), cons())), id()), reverse() -> app(app(uncurry(), app(app(fold(), app(swap(), append())), listify())), nil()), length() -> app(app(uncurry(), app(app(fold(), add()), app(cons(), 1()))), 0())} Open