YES Time: 0.100298 TRS: { f(x, 0(), 0()) -> s x, f(s x, s y, s z) -> f(x, y, f(s x, s y, z)), f(s x, s y, 0()) -> f(x, y, s 0()), f(s x, 0(), s z) -> f(x, s 0(), z), f(s 0(), y, z) -> f(0(), s y, s z), f(0(), y, 0()) -> s y, f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)), f(0(), s s y, s 0()) -> f(0(), y, s 0()), f(0(), s 0(), s s z) -> f(0(), s 0(), z), f(0(), s 0(), s 0()) -> s s 0(), f(0(), 0(), z) -> s z} DP: DP: { f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, s y, s z) -> f#(s x, s y, z), f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s s y, s s z) -> f#(0(), s s y, s z), f#(0(), s s y, s 0()) -> f#(0(), y, s 0()), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)} TRS: { f(x, 0(), 0()) -> s x, f(s x, s y, s z) -> f(x, y, f(s x, s y, z)), f(s x, s y, 0()) -> f(x, y, s 0()), f(s x, 0(), s z) -> f(x, s 0(), z), f(s 0(), y, z) -> f(0(), s y, s z), f(0(), y, 0()) -> s y, f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)), f(0(), s s y, s 0()) -> f(0(), y, s 0()), f(0(), s 0(), s s z) -> f(0(), s 0(), z), f(0(), s 0(), s 0()) -> s s 0(), f(0(), 0(), z) -> s z} UR: { f(x, 0(), 0()) -> s x, f(s x, s y, s z) -> f(x, y, f(s x, s y, z)), f(s x, s y, 0()) -> f(x, y, s 0()), f(s x, 0(), s z) -> f(x, s 0(), z), f(s 0(), y, z) -> f(0(), s y, s z), f(0(), y, 0()) -> s y, f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)), f(0(), s s y, s 0()) -> f(0(), y, s 0()), f(0(), s 0(), s s z) -> f(0(), s 0(), z), f(0(), s 0(), s 0()) -> s s 0(), f(0(), 0(), z) -> s z, a(w, v) -> w, a(w, v) -> v} EDG: {(f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)) (f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s 0(), y, z) -> f#(0(), s y, s z)) (f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s x, s y, 0()) -> f#(x, y, s 0())) (f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s x, s y, s z) -> f#(s x, s y, z)) (f#(s x, 0(), s z) -> f#(x, s 0(), z), f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z))) (f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(0(), s s y, s 0()) -> f#(0(), y, s 0())) (f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s 0(), y, z) -> f#(0(), s y, s z)) (f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s x, 0(), s z) -> f#(x, s 0(), z)) (f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s x, s y, s z) -> f#(s x, s y, z)) (f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z))) (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)) (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(0(), s s y, s 0()) -> f#(0(), y, s 0())) (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(0(), s s y, s s z) -> f#(0(), s s y, s z)) (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z))) (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s 0(), y, z) -> f#(0(), s y, s z)) (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, 0(), s z) -> f#(x, s 0(), z)) (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, s y, 0()) -> f#(x, y, s 0())) (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, s y, s z) -> f#(s x, s y, z)) (f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z))) (f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)) (f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s s y, s 0()) -> f#(0(), y, s 0())) (f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s s y, s s z) -> f#(0(), s s y, s z)) (f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z))) (f#(0(), s s y, s s z) -> f#(0(), s s y, s z), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z))) (f#(0(), s s y, s s z) -> f#(0(), s s y, s z), f#(0(), s s y, s s z) -> f#(0(), s s y, s z)) (f#(0(), s s y, s s z) -> f#(0(), s s y, s z), f#(0(), s s y, s 0()) -> f#(0(), y, s 0())) (f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z))) (f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s s y, s s z) -> f#(0(), s s y, s z)) (f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s s y, s 0()) -> f#(0(), y, s 0())) (f#(s 0(), y, z) -> f#(0(), s y, s z), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)) (f#(0(), s s y, s 0()) -> f#(0(), y, s 0()), f#(0(), s s y, s 0()) -> f#(0(), y, s 0())) (f#(0(), s 0(), s s z) -> f#(0(), s 0(), z), f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)) (f#(s x, s y, s z) -> f#(s x, s y, z), f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z))) (f#(s x, s y, s z) -> f#(s x, s y, z), f#(s x, s y, s z) -> f#(s x, s y, z)) (f#(s x, s y, s z) -> f#(s x, s y, z), f#(s x, s y, 0()) -> f#(x, y, s 0())) (f#(s x, s y, s z) -> f#(s x, s y, z), f#(s 0(), y, z) -> f#(0(), s y, s z))} STATUS: arrows: 0.555556 SCCS (4): Scc: {f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, s y, s z) -> f#(s x, s y, z), f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s x, 0(), s z) -> f#(x, s 0(), z)} Scc: {f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s s y, s s z) -> f#(0(), s s y, s z)} Scc: {f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)} Scc: {f#(0(), s s y, s 0()) -> f#(0(), y, s 0())} SCC (4): Strict: {f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)), f#(s x, s y, s z) -> f#(s x, s y, z), f#(s x, s y, 0()) -> f#(x, y, s 0()), f#(s x, 0(), s z) -> f#(x, s 0(), z)} Weak: { f(x, 0(), 0()) -> s x, f(s x, s y, s z) -> f(x, y, f(s x, s y, z)), f(s x, s y, 0()) -> f(x, y, s 0()), f(s x, 0(), s z) -> f(x, s 0(), z), f(s 0(), y, z) -> f(0(), s y, s z), f(0(), y, 0()) -> s y, f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)), f(0(), s s y, s 0()) -> f(0(), y, s 0()), f(0(), s 0(), s s z) -> f(0(), s 0(), z), f(0(), s 0(), s 0()) -> s s 0(), f(0(), 0(), z) -> s z} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = 0, [s](x0) = x0 + 1, [0] = 0, [f#](x0, x1, x2) = x0 + 1 Strict: f#(s x, 0(), s z) -> f#(x, s 0(), z) 2 + 1x + 0z >= 1 + 1x + 0z f#(s x, s y, 0()) -> f#(x, y, s 0()) 2 + 1x + 0y >= 1 + 1x + 0y f#(s x, s y, s z) -> f#(s x, s y, z) 2 + 1x + 0y + 0z >= 2 + 1x + 0y + 0z f#(s x, s y, s z) -> f#(x, y, f(s x, s y, z)) 2 + 1x + 0y + 0z >= 1 + 1x + 0y + 0z Weak: f(0(), 0(), z) -> s z 0 + 0z >= 1 + 1z f(0(), s 0(), s 0()) -> s s 0() 0 >= 2 f(0(), s 0(), s s z) -> f(0(), s 0(), z) 0 + 0z >= 0 + 0z f(0(), s s y, s 0()) -> f(0(), y, s 0()) 0 + 0y >= 0 + 0y f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)) 0 + 0y + 0z >= 0 + 0y + 0z f(0(), y, 0()) -> s y 0 + 0y >= 1 + 1y f(s 0(), y, z) -> f(0(), s y, s z) 0 + 0y + 0z >= 0 + 0y + 0z f(s x, 0(), s z) -> f(x, s 0(), z) 0 + 0x + 0z >= 0 + 0x + 0z f(s x, s y, 0()) -> f(x, y, s 0()) 0 + 0x + 0y >= 0 + 0x + 0y f(s x, s y, s z) -> f(x, y, f(s x, s y, z)) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z f(x, 0(), 0()) -> s x 0 + 0x >= 1 + 1x SCCS (1): Scc: {f#(s x, s y, s z) -> f#(s x, s y, z)} SCC (1): Strict: {f#(s x, s y, s z) -> f#(s x, s y, z)} Weak: { f(x, 0(), 0()) -> s x, f(s x, s y, s z) -> f(x, y, f(s x, s y, z)), f(s x, s y, 0()) -> f(x, y, s 0()), f(s x, 0(), s z) -> f(x, s 0(), z), f(s 0(), y, z) -> f(0(), s y, s z), f(0(), y, 0()) -> s y, f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)), f(0(), s s y, s 0()) -> f(0(), y, s 0()), f(0(), s 0(), s s z) -> f(0(), s 0(), z), f(0(), s 0(), s 0()) -> s s 0(), f(0(), 0(), z) -> s z} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + x1 + 1, [s](x0) = x0 + 1, [0] = 1, [f#](x0, x1, x2) = x0 + 1 Strict: f#(s x, s y, s z) -> f#(s x, s y, z) 2 + 0x + 0y + 1z >= 1 + 0x + 0y + 1z Weak: f(0(), 0(), z) -> s z 2 + 1z >= 1 + 1z f(0(), s 0(), s 0()) -> s s 0() 4 >= 3 f(0(), s 0(), s s z) -> f(0(), s 0(), z) 4 + 1z >= 2 + 1z f(0(), s s y, s 0()) -> f(0(), y, s 0()) 4 + 0y >= 4 + 0y f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)) 4 + 0y + 1z >= 5 + 0y + 1z f(0(), y, 0()) -> s y 3 + 0y >= 1 + 1y f(s 0(), y, z) -> f(0(), s y, s z) 3 + 0y + 1z >= 3 + 0y + 1z f(s x, 0(), s z) -> f(x, s 0(), z) 3 + 1x + 1z >= 1 + 1x + 1z f(s x, s y, 0()) -> f(x, y, s 0()) 3 + 1x + 0y >= 3 + 1x + 0y f(s x, s y, s z) -> f(x, y, f(s x, s y, z)) 3 + 1x + 0y + 1z >= 3 + 2x + 0y + 1z f(x, 0(), 0()) -> s x 2 + 1x >= 1 + 1x Qed SCC (2): Strict: {f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)), f#(0(), s s y, s s z) -> f#(0(), s s y, s z)} Weak: { f(x, 0(), 0()) -> s x, f(s x, s y, s z) -> f(x, y, f(s x, s y, z)), f(s x, s y, 0()) -> f(x, y, s 0()), f(s x, 0(), s z) -> f(x, s 0(), z), f(s 0(), y, z) -> f(0(), s y, s z), f(0(), y, 0()) -> s y, f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)), f(0(), s s y, s 0()) -> f(0(), y, s 0()), f(0(), s 0(), s s z) -> f(0(), s 0(), z), f(0(), s 0(), s 0()) -> s s 0(), f(0(), 0(), z) -> s z} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = 0, [s](x0) = x0 + 1, [0] = 0, [f#](x0, x1, x2) = x0 Strict: f#(0(), s s y, s s z) -> f#(0(), s s y, s z) 2 + 1y + 0z >= 2 + 1y + 0z f#(0(), s s y, s s z) -> f#(0(), y, f(0(), s s y, s z)) 2 + 1y + 0z >= 0 + 1y + 0z Weak: f(0(), 0(), z) -> s z 0 + 0z >= 1 + 1z f(0(), s 0(), s 0()) -> s s 0() 0 >= 2 f(0(), s 0(), s s z) -> f(0(), s 0(), z) 0 + 0z >= 0 + 0z f(0(), s s y, s 0()) -> f(0(), y, s 0()) 0 + 0y >= 0 + 0y f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)) 0 + 0y + 0z >= 0 + 0y + 0z f(0(), y, 0()) -> s y 0 + 0y >= 1 + 1y f(s 0(), y, z) -> f(0(), s y, s z) 0 + 0y + 0z >= 0 + 0y + 0z f(s x, 0(), s z) -> f(x, s 0(), z) 0 + 0x + 0z >= 0 + 0x + 0z f(s x, s y, 0()) -> f(x, y, s 0()) 0 + 0x + 0y >= 0 + 0x + 0y f(s x, s y, s z) -> f(x, y, f(s x, s y, z)) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z f(x, 0(), 0()) -> s x 0 + 0x >= 1 + 1x SCCS (1): Scc: {f#(0(), s s y, s s z) -> f#(0(), s s y, s z)} SCC (1): Strict: {f#(0(), s s y, s s z) -> f#(0(), s s y, s z)} Weak: { f(x, 0(), 0()) -> s x, f(s x, s y, s z) -> f(x, y, f(s x, s y, z)), f(s x, s y, 0()) -> f(x, y, s 0()), f(s x, 0(), s z) -> f(x, s 0(), z), f(s 0(), y, z) -> f(0(), s y, s z), f(0(), y, 0()) -> s y, f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)), f(0(), s s y, s 0()) -> f(0(), y, s 0()), f(0(), s 0(), s s z) -> f(0(), s 0(), z), f(0(), s 0(), s 0()) -> s s 0(), f(0(), 0(), z) -> s z} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + x1, [s](x0) = x0 + 1, [0] = 1, [f#](x0, x1, x2) = x0 + x1 + x2 + 1 Strict: f#(0(), s s y, s s z) -> f#(0(), s s y, s z) 6 + 1y + 1z >= 5 + 1y + 1z Weak: f(0(), 0(), z) -> s z 1 + 1z >= 1 + 1z f(0(), s 0(), s 0()) -> s s 0() 3 >= 3 f(0(), s 0(), s s z) -> f(0(), s 0(), z) 3 + 1z >= 1 + 1z f(0(), s s y, s 0()) -> f(0(), y, s 0()) 3 + 0y >= 3 + 0y f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)) 3 + 0y + 1z >= 3 + 0y + 1z f(0(), y, 0()) -> s y 2 + 0y >= 1 + 1y f(s 0(), y, z) -> f(0(), s y, s z) 2 + 0y + 1z >= 2 + 0y + 1z f(s x, 0(), s z) -> f(x, s 0(), z) 2 + 1x + 1z >= 0 + 1x + 1z f(s x, s y, 0()) -> f(x, y, s 0()) 2 + 1x + 0y >= 2 + 1x + 0y f(s x, s y, s z) -> f(x, y, f(s x, s y, z)) 2 + 1x + 0y + 1z >= 1 + 2x + 0y + 1z f(x, 0(), 0()) -> s x 1 + 1x >= 1 + 1x Qed SCC (1): Strict: {f#(0(), s 0(), s s z) -> f#(0(), s 0(), z)} Weak: { f(x, 0(), 0()) -> s x, f(s x, s y, s z) -> f(x, y, f(s x, s y, z)), f(s x, s y, 0()) -> f(x, y, s 0()), f(s x, 0(), s z) -> f(x, s 0(), z), f(s 0(), y, z) -> f(0(), s y, s z), f(0(), y, 0()) -> s y, f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)), f(0(), s s y, s 0()) -> f(0(), y, s 0()), f(0(), s 0(), s s z) -> f(0(), s 0(), z), f(0(), s 0(), s 0()) -> s s 0(), f(0(), 0(), z) -> s z} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + x1 + 1, [s](x0) = x0 + 1, [0] = 1, [f#](x0, x1, x2) = x0 + x1 Strict: f#(0(), s 0(), s s z) -> f#(0(), s 0(), z) 3 + 1z >= 1 + 1z Weak: f(0(), 0(), z) -> s z 2 + 1z >= 1 + 1z f(0(), s 0(), s 0()) -> s s 0() 4 >= 3 f(0(), s 0(), s s z) -> f(0(), s 0(), z) 4 + 1z >= 2 + 1z f(0(), s s y, s 0()) -> f(0(), y, s 0()) 4 + 0y >= 4 + 0y f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)) 4 + 0y + 1z >= 5 + 0y + 1z f(0(), y, 0()) -> s y 3 + 0y >= 1 + 1y f(s 0(), y, z) -> f(0(), s y, s z) 3 + 0y + 1z >= 3 + 0y + 1z f(s x, 0(), s z) -> f(x, s 0(), z) 3 + 1x + 1z >= 1 + 1x + 1z f(s x, s y, 0()) -> f(x, y, s 0()) 3 + 1x + 0y >= 3 + 1x + 0y f(s x, s y, s z) -> f(x, y, f(s x, s y, z)) 3 + 1x + 0y + 1z >= 3 + 2x + 0y + 1z f(x, 0(), 0()) -> s x 2 + 1x >= 1 + 1x Qed SCC (1): Strict: {f#(0(), s s y, s 0()) -> f#(0(), y, s 0())} Weak: { f(x, 0(), 0()) -> s x, f(s x, s y, s z) -> f(x, y, f(s x, s y, z)), f(s x, s y, 0()) -> f(x, y, s 0()), f(s x, 0(), s z) -> f(x, s 0(), z), f(s 0(), y, z) -> f(0(), s y, s z), f(0(), y, 0()) -> s y, f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)), f(0(), s s y, s 0()) -> f(0(), y, s 0()), f(0(), s 0(), s s z) -> f(0(), s 0(), z), f(0(), s 0(), s 0()) -> s s 0(), f(0(), 0(), z) -> s z} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + x1 + x2 + 1, [s](x0) = x0 + 1, [0] = 1, [f#](x0, x1, x2) = x0 Strict: f#(0(), s s y, s 0()) -> f#(0(), y, s 0()) 2 + 1y >= 0 + 1y Weak: f(0(), 0(), z) -> s z 3 + 1z >= 1 + 1z f(0(), s 0(), s 0()) -> s s 0() 6 >= 3 f(0(), s 0(), s s z) -> f(0(), s 0(), z) 6 + 1z >= 4 + 1z f(0(), s s y, s 0()) -> f(0(), y, s 0()) 6 + 1y >= 4 + 1y f(0(), s s y, s s z) -> f(0(), y, f(0(), s s y, s z)) 6 + 1y + 1z >= 7 + 2y + 1z f(0(), y, 0()) -> s y 3 + 1y >= 1 + 1y f(s 0(), y, z) -> f(0(), s y, s z) 3 + 1y + 1z >= 4 + 1y + 1z f(s x, 0(), s z) -> f(x, s 0(), z) 4 + 1x + 1z >= 3 + 1x + 1z f(s x, s y, 0()) -> f(x, y, s 0()) 4 + 1x + 1y >= 3 + 1x + 1y f(s x, s y, s z) -> f(x, y, f(s x, s y, z)) 4 + 1x + 1y + 1z >= 4 + 2x + 2y + 1z f(x, 0(), 0()) -> s x 3 + 1x >= 1 + 1x Qed