YES Time: 0.059269 TRS: { +(p2(), +(p2(), p2())) -> +(p1(), p5()), +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)), +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)), +(p2(), p1()) -> +(p1(), p2()), +(+(x, y), z) -> +(x, +(y, z)), +(p1(), +(p2(), p2())) -> p5(), +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x), +(p1(), +(p1(), x)) -> +(p2(), x), +(p1(), p1()) -> p2(), +(p5(), p2()) -> +(p2(), p5()), +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)), +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)), +(p5(), +(p5(), x)) -> +(p10(), x), +(p5(), p1()) -> +(p1(), p5()), +(p5(), p5()) -> p10(), +(p10(), p2()) -> +(p2(), p10()), +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)), +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)), +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)), +(p10(), p1()) -> +(p1(), p10()), +(p10(), p5()) -> +(p5(), p10())} DP: DP: { +#(p2(), +(p2(), p2())) -> +#(p1(), p5()), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)), +#(p2(), p1()) -> +#(p1(), p2()), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p5(), p2()) -> +#(p2(), p5()), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)), +#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p5(), p1()) -> +#(p1(), p5()), +#(p10(), p2()) -> +#(p2(), p10()), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)), +#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10()), +#(p10(), p5()) -> +#(p5(), p10())} TRS: { +(p2(), +(p2(), p2())) -> +(p1(), p5()), +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)), +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)), +(p2(), p1()) -> +(p1(), p2()), +(+(x, y), z) -> +(x, +(y, z)), +(p1(), +(p2(), p2())) -> p5(), +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x), +(p1(), +(p1(), x)) -> +(p2(), x), +(p1(), p1()) -> p2(), +(p5(), p2()) -> +(p2(), p5()), +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)), +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)), +(p5(), +(p5(), x)) -> +(p10(), x), +(p5(), p1()) -> +(p1(), p5()), +(p5(), p5()) -> p10(), +(p10(), p2()) -> +(p2(), p10()), +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)), +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)), +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)), +(p10(), p1()) -> +(p1(), p10()), +(p10(), p5()) -> +(p5(), p10())} EDG: { (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), p1()) -> +#(p1(), p5())) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), p2()) -> +#(p2(), p5())) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), p1()) -> +#(p1(), p5())) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), p2()) -> +#(p2(), p5())) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), p1()) -> +#(p1(), p5())) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), p2()) -> +#(p2(), p5())) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p5()) -> +#(p5(), p10())) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10())) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p10(), x)) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p10(), x)) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x))) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p10(), x)) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x))) (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p2()) -> +#(p2(), p10())) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), p5()) -> +#(p5(), p10())) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10())) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p10(), x)) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p10(), x)) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x))) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p10(), x)) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x))) (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), p2()) -> +#(p2(), p10())) (+#(+(x, y), z) -> +#(y, z), +#(p10(), p5()) -> +#(p5(), p10())) (+#(+(x, y), z) -> +#(y, z), +#(p10(), p1()) -> +#(p1(), p10())) (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p5(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p1(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p2(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p10(), p2()) -> +#(p2(), p10())) (+#(+(x, y), z) -> +#(y, z), +#(p5(), p1()) -> +#(p1(), p5())) (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p5(), p2()) -> +#(p2(), p5())) (+#(+(x, y), z) -> +#(y, z), +#(p1(), +(p1(), x)) -> +#(p2(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(p2(), p1()) -> +#(p1(), p2())) (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p1(), x)) -> +#(p2(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x))) (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p2(), p2())) -> +#(p1(), p5())) (+#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)), +#(p1(), +(p1(), x)) -> +#(p2(), x)) (+#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p1(), x)) -> +#(p2(), x)) (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x))) (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p2(), p2())) -> +#(p1(), p5())) (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p1(), x)) -> +#(p2(), x)) (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x))) (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p2(), p2())) -> +#(p1(), p5())) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), p2()) -> +#(p2(), p5())) (+#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)), +#(p1(), +(p1(), x)) -> +#(p2(), x)) (+#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)), +#(p1(), +(p1(), x)) -> +#(p2(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p2(), p2())) -> +#(p1(), p5())) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p1(), x)) -> +#(p2(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p1(), +(p1(), x)) -> +#(p2(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), p2()) -> +#(p2(), p5())) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), p2()) -> +#(p2(), p10())) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p2(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p1(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p5(), x)) -> +#(p10(), x)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), p5()) -> +#(p5(), p10())) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)), +#(p1(), +(p1(), x)) -> +#(p2(), x)) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p2()) -> +#(p2(), p10())) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x))) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p10(), x)) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x))) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p10(), x)) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p10(), x)) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10())) (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p5()) -> +#(p5(), p10())) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), p2()) -> +#(p2(), p10())) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x))) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p10(), x)) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x))) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p10(), x)) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p10(), x)) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10())) (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), p5()) -> +#(p5(), p10())) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), p2()) -> +#(p2(), p5())) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x))) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p5(), x)) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p5(), x)) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x)) (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), p1()) -> +#(p1(), p5())) (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), p2())) -> +#(p1(), p5())) (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x))) (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p2(), x)) (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), p1()) -> +#(p1(), p2())) (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), p2())) -> +#(p1(), p5())) (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x))) (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x)) (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p2(), x)) (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), p1()) -> +#(p1(), p2())) } SCCS (2): Scc: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Scc: {+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)), +#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)), +#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p10(), +(p5(), x)) -> +#(p10(), x)} SCC (2): Strict: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Weak: { +(p2(), +(p2(), p2())) -> +(p1(), p5()), +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)), +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)), +(p2(), p1()) -> +(p1(), p2()), +(+(x, y), z) -> +(x, +(y, z)), +(p1(), +(p2(), p2())) -> p5(), +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x), +(p1(), +(p1(), x)) -> +(p2(), x), +(p1(), p1()) -> p2(), +(p5(), p2()) -> +(p2(), p5()), +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)), +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)), +(p5(), +(p5(), x)) -> +(p10(), x), +(p5(), p1()) -> +(p1(), p5()), +(p5(), p5()) -> p10(), +(p10(), p2()) -> +(p2(), p10()), +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)), +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)), +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)), +(p10(), p1()) -> +(p1(), p10()), +(p10(), p5()) -> +(p5(), p10())} SPSC: Simple Projection: pi(+#) = 0 Strict: {+#(+(x, y), z) -> +#(y, z)} EDG: {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))} SCCS (1): Scc: {+#(+(x, y), z) -> +#(y, z)} SCC (1): Strict: {+#(+(x, y), z) -> +#(y, z)} Weak: { +(p2(), +(p2(), p2())) -> +(p1(), p5()), +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)), +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)), +(p2(), p1()) -> +(p1(), p2()), +(+(x, y), z) -> +(x, +(y, z)), +(p1(), +(p2(), p2())) -> p5(), +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x), +(p1(), +(p1(), x)) -> +(p2(), x), +(p1(), p1()) -> p2(), +(p5(), p2()) -> +(p2(), p5()), +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)), +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)), +(p5(), +(p5(), x)) -> +(p10(), x), +(p5(), p1()) -> +(p1(), p5()), +(p5(), p5()) -> p10(), +(p10(), p2()) -> +(p2(), p10()), +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)), +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)), +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)), +(p10(), p1()) -> +(p1(), p10()), +(p10(), p5()) -> +(p5(), p10())} SPSC: Simple Projection: pi(+#) = 0 Strict: {} Qed SCC (17): Strict: {+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)), +#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)), +#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p10(), +(p5(), x)) -> +#(p10(), x)} Weak: { +(p2(), +(p2(), p2())) -> +(p1(), p5()), +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)), +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)), +(p2(), p1()) -> +(p1(), p2()), +(+(x, y), z) -> +(x, +(y, z)), +(p1(), +(p2(), p2())) -> p5(), +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x), +(p1(), +(p1(), x)) -> +(p2(), x), +(p1(), p1()) -> p2(), +(p5(), p2()) -> +(p2(), p5()), +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)), +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)), +(p5(), +(p5(), x)) -> +(p10(), x), +(p5(), p1()) -> +(p1(), p5()), +(p5(), p5()) -> p10(), +(p10(), p2()) -> +(p2(), p10()), +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)), +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)), +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)), +(p10(), p1()) -> +(p1(), p10()), +(p10(), p5()) -> +(p5(), p10())} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1, [p2] = 1, [p1] = 1, [p5] = 1, [p10] = 1, [+#](x0, x1) = x0 Strict: +#(p10(), +(p5(), x)) -> +#(p10(), x) 1 + 1x >= 0 + 1x +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)) 1 + 1x >= 1 + 1x +#(p10(), +(p1(), x)) -> +#(p10(), x) 1 + 1x >= 0 + 1x +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)) 1 + 1x >= 1 + 1x +#(p10(), +(p2(), x)) -> +#(p10(), x) 1 + 1x >= 0 + 1x +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)) 1 + 1x >= 1 + 1x +#(p5(), +(p5(), x)) -> +#(p10(), x) 1 + 1x >= 0 + 1x +#(p5(), +(p1(), x)) -> +#(p5(), x) 1 + 1x >= 0 + 1x +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)) 1 + 1x >= 1 + 1x +#(p5(), +(p2(), x)) -> +#(p5(), x) 1 + 1x >= 0 + 1x +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)) 1 + 1x >= 1 + 1x +#(p1(), +(p1(), x)) -> +#(p2(), x) 1 + 1x >= 0 + 1x +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x) 2 + 1x >= 0 + 1x +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)) 1 + 1x >= 1 + 1x +#(p2(), +(p1(), x)) -> +#(p2(), x) 1 + 1x >= 0 + 1x +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x) 2 + 1x >= 0 + 1x +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)) 2 + 1x >= 1 + 1x Weak: EDG: {(+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x))) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x))) (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)))} SCCS (0): Qed