YES Time: 0.069113 TRS: { +(+(x, y), z) -> +(x, +(y, z)), +(f x, +(f y, z)) -> +(f +(x, y), z), +(f x, f y) -> f +(x, y)} DP: DP: { +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(f x, +(f y, z)) -> +#(x, y), +#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, f y) -> +#(x, y)} TRS: { +(+(x, y), z) -> +(x, +(y, z)), +(f x, +(f y, z)) -> +(f +(x, y), z), +(f x, f y) -> f +(x, y)} EDG: {(+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, f y) -> +#(x, y)) (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, +(f y, z)) -> +#(f +(x, y), z)) (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, +(f y, z)) -> +#(x, y)) (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(+(x, y), z) -> +#(y, z)) (+#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, f y) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, +(f y, z)) -> +#(f +(x, y), z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, +(f y, z)) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(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))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(f x, +(f y, z)) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(f x, +(f y, z)) -> +#(f +(x, y), z)) (+#(+(x, y), z) -> +#(y, z), +#(f x, f y) -> +#(x, y)) (+#(f x, f y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(f x, f y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(f x, f y) -> +#(x, y), +#(f x, +(f y, z)) -> +#(x, y)) (+#(f x, f y) -> +#(x, y), +#(f x, +(f y, z)) -> +#(f +(x, y), z)) (+#(f x, f y) -> +#(x, y), +#(f x, f y) -> +#(x, y)) (+#(f x, +(f y, z)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(f x, +(f y, z)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(f x, +(f y, z)) -> +#(x, y), +#(f x, +(f y, z)) -> +#(x, y)) (+#(f x, +(f y, z)) -> +#(x, y), +#(f x, +(f y, z)) -> +#(f +(x, y), z)) (+#(f x, +(f y, z)) -> +#(x, y), +#(f x, f y) -> +#(x, y))} STATUS: arrows: 0.000000 SCCS (1): Scc: { +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(f x, +(f y, z)) -> +#(x, y), +#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, f y) -> +#(x, y)} SCC (5): Strict: { +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(f x, +(f y, z)) -> +#(x, y), +#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, f y) -> +#(x, y)} Weak: { +(+(x, y), z) -> +(x, +(y, z)), +(f x, +(f y, z)) -> +(f +(x, y), z), +(f x, f y) -> f +(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1 + 1, [f](x0) = x0, [+#](x0, x1) = x0 + x1 Strict: +#(f x, f y) -> +#(x, y) 0 + 1x + 1y >= 0 + 1x + 1y +#(f x, +(f y, z)) -> +#(f +(x, y), z) 1 + 1x + 1y + 1z >= 1 + 1x + 1y + 1z +#(f x, +(f y, z)) -> +#(x, y) 1 + 1x + 1y + 1z >= 0 + 1x + 1y +#(+(x, y), z) -> +#(y, z) 1 + 1x + 1y + 1z >= 0 + 1y + 1z +#(+(x, y), z) -> +#(x, +(y, z)) 1 + 1x + 1y + 1z >= 1 + 1x + 1y + 1z Weak: +(f x, f y) -> f +(x, y) 1 + 1x + 1y >= 1 + 1x + 1y +(f x, +(f y, z)) -> +(f +(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z SCCS (1): Scc: { +#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, f y) -> +#(x, y)} SCC (3): Strict: { +#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, +(f y, z)) -> +#(f +(x, y), z), +#(f x, f y) -> +#(x, y)} Weak: { +(+(x, y), z) -> +(x, +(y, z)), +(f x, +(f y, z)) -> +(f +(x, y), z), +(f x, f y) -> f +(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0, [f](x0) = x0 + 1, [+#](x0, x1) = x0 Strict: +#(f x, f y) -> +#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y +#(f x, +(f y, z)) -> +#(f +(x, y), z) 0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z +#(+(x, y), z) -> +#(x, +(y, z)) 0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z Weak: +(f x, f y) -> f +(x, y) 1 + 0x + 1y >= 1 + 0x + 1y +(f x, +(f y, z)) -> +(f +(x, y), z) 0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z +(+(x, y), z) -> +(x, +(y, z)) 0 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z SCCS (1): Scc: { +#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, +(f y, z)) -> +#(f +(x, y), z)} SCC (2): Strict: { +#(+(x, y), z) -> +#(x, +(y, z)), +#(f x, +(f y, z)) -> +#(f +(x, y), z)} Weak: { +(+(x, y), z) -> +(x, +(y, z)), +(f x, +(f y, z)) -> +(f +(x, y), z), +(f x, f y) -> f +(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1 + 1, [f](x0) = 0, [+#](x0, x1) = x0 + x1 Strict: +#(f x, +(f y, z)) -> +#(f +(x, y), z) 1 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z +#(+(x, y), z) -> +#(x, +(y, z)) 1 + 1x + 1y + 1z >= 1 + 1x + 1y + 1z Weak: +(f x, f y) -> f +(x, y) 1 + 0x + 0y >= 0 + 0x + 0y +(f x, +(f y, z)) -> +(f +(x, y), z) 2 + 0x + 0y + 1z >= 1 + 0x + 0y + 1z +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z SCCS (1): Scc: {+#(+(x, y), z) -> +#(x, +(y, z))} SCC (1): Strict: {+#(+(x, y), z) -> +#(x, +(y, z))} Weak: { +(+(x, y), z) -> +(x, +(y, z)), +(f x, +(f y, z)) -> +(f +(x, y), z), +(f x, f y) -> f +(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [+](x0, x1) = x0 + x1 + 1, [f](x0) = 0, [+#](x0, x1) = x0 + 1 Strict: +#(+(x, y), z) -> +#(x, +(y, z)) 2 + 1x + 1y + 0z >= 1 + 1x + 0y + 0z Weak: +(f x, f y) -> f +(x, y) 1 + 0x + 0y >= 0 + 0x + 0y +(f x, +(f y, z)) -> +(f +(x, y), z) 2 + 0x + 0y + 1z >= 1 + 0x + 0y + 1z +(+(x, y), z) -> +(x, +(y, z)) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z Qed