MAYBE Time: 2.280887 TRS: { h(e x, y) -> h(d(x, y), s y), d(g(x, y), z) -> g(d(x, z), e y), d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)), d(g(g(0(), x), y), 0()) -> e y, d(g(0(), x), y) -> e x, g(e x, e y) -> e g(x, y)} DP: DP: { h#(e x, y) -> h#(d(x, y), s y), h#(e x, y) -> d#(x, y), d#(g(x, y), z) -> d#(x, z), d#(g(x, y), z) -> g#(d(x, z), e y), d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z), d#(g(g(0(), x), y), s z) -> g#(e x, d(g(g(0(), x), y), z)), g#(e x, e y) -> g#(x, y)} TRS: { h(e x, y) -> h(d(x, y), s y), d(g(x, y), z) -> g(d(x, z), e y), d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)), d(g(g(0(), x), y), 0()) -> e y, d(g(0(), x), y) -> e x, g(e x, e y) -> e g(x, y)} UR: { d(g(x, y), z) -> g(d(x, z), e y), d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)), d(g(g(0(), x), y), 0()) -> e y, d(g(0(), x), y) -> e x, g(e x, e y) -> e g(x, y), a(w, v) -> w, a(w, v) -> v} EDG: {(h#(e x, y) -> h#(d(x, y), s y), h#(e x, y) -> d#(x, y)) (h#(e x, y) -> h#(d(x, y), s y), h#(e x, y) -> h#(d(x, y), s y)) (d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z), d#(g(g(0(), x), y), s z) -> g#(e x, d(g(g(0(), x), y), z))) (d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z), d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z)) (d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z), d#(g(x, y), z) -> g#(d(x, z), e y)) (d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z), d#(g(x, y), z) -> d#(x, z)) (g#(e x, e y) -> g#(x, y), g#(e x, e y) -> g#(x, y)) (d#(g(x, y), z) -> d#(x, z), d#(g(x, y), z) -> d#(x, z)) (d#(g(x, y), z) -> d#(x, z), d#(g(x, y), z) -> g#(d(x, z), e y)) (d#(g(x, y), z) -> d#(x, z), d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z)) (d#(g(x, y), z) -> d#(x, z), d#(g(g(0(), x), y), s z) -> g#(e x, d(g(g(0(), x), y), z))) (h#(e x, y) -> d#(x, y), d#(g(x, y), z) -> d#(x, z)) (h#(e x, y) -> d#(x, y), d#(g(x, y), z) -> g#(d(x, z), e y)) (h#(e x, y) -> d#(x, y), d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z)) (h#(e x, y) -> d#(x, y), d#(g(g(0(), x), y), s z) -> g#(e x, d(g(g(0(), x), y), z))) (d#(g(x, y), z) -> g#(d(x, z), e y), g#(e x, e y) -> g#(x, y)) (d#(g(g(0(), x), y), s z) -> g#(e x, d(g(g(0(), x), y), z)), g#(e x, e y) -> g#(x, y))} STATUS: arrows: 0.653061 SCCS (3): Scc: {h#(e x, y) -> h#(d(x, y), s y)} Scc: { d#(g(x, y), z) -> d#(x, z), d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z)} Scc: {g#(e x, e y) -> g#(x, y)} SCC (1): Strict: {h#(e x, y) -> h#(d(x, y), s y)} Weak: { h(e x, y) -> h(d(x, y), s y), d(g(x, y), z) -> g(d(x, z), e y), d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)), d(g(g(0(), x), y), 0()) -> e y, d(g(0(), x), y) -> e x, g(e x, e y) -> e g(x, y)} Fail SCC (2): Strict: { d#(g(x, y), z) -> d#(x, z), d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z)} Weak: { h(e x, y) -> h(d(x, y), s y), d(g(x, y), z) -> g(d(x, z), e y), d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)), d(g(g(0(), x), y), 0()) -> e y, d(g(0(), x), y) -> e x, g(e x, e y) -> e g(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [h](x0, x1) = 0, [d](x0, x1) = 0, [g](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [e](x0) = 0, [0] = 1, [d#](x0, x1) = x0 Strict: d#(g(g(0(), x), y), s z) -> d#(g(g(0(), x), y), z) 1 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z d#(g(x, y), z) -> d#(x, z) 0 + 0x + 0y + 1z >= 0 + 0x + 1z Weak: g(e x, e y) -> e g(x, y) 1 + 0x + 0y >= 0 + 0x + 0y d(g(0(), x), y) -> e x 0 + 0x + 0y >= 0 + 0x d(g(g(0(), x), y), 0()) -> e y 0 + 0x + 0y >= 0 + 0y d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)) 0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z d(g(x, y), z) -> g(d(x, z), e y) 0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z h(e x, y) -> h(d(x, y), s y) 0 + 0x + 0y >= 0 + 0x + 0y SCCS (1): Scc: {d#(g(x, y), z) -> d#(x, z)} SCC (1): Strict: {d#(g(x, y), z) -> d#(x, z)} Weak: { h(e x, y) -> h(d(x, y), s y), d(g(x, y), z) -> g(d(x, z), e y), d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)), d(g(g(0(), x), y), 0()) -> e y, d(g(0(), x), y) -> e x, g(e x, e y) -> e g(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [h](x0, x1) = x0 + x1 + 1, [d](x0, x1) = x0, [g](x0, x1) = x0 + 1, [s](x0) = x0, [e](x0) = 1, [0] = 0, [d#](x0, x1) = x0 Strict: d#(g(x, y), z) -> d#(x, z) 1 + 1x + 0y + 0z >= 0 + 1x + 0z Weak: g(e x, e y) -> e g(x, y) 2 + 0x + 0y >= 1 + 0x + 0y d(g(0(), x), y) -> e x 0 + 0x + 1y >= 1 + 0x d(g(g(0(), x), y), 0()) -> e y 0 + 0x + 0y >= 1 + 0y d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)) 0 + 0x + 0y + 1z >= 2 + 0x + 0y + 0z d(g(x, y), z) -> g(d(x, z), e y) 0 + 0x + 0y + 1z >= 1 + 0x + 0y + 1z h(e x, y) -> h(d(x, y), s y) 2 + 0x + 1y >= 1 + 0x + 2y Qed SCC (1): Strict: {g#(e x, e y) -> g#(x, y)} Weak: { h(e x, y) -> h(d(x, y), s y), d(g(x, y), z) -> g(d(x, z), e y), d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)), d(g(g(0(), x), y), 0()) -> e y, d(g(0(), x), y) -> e x, g(e x, e y) -> e g(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [h](x0, x1) = x0 + x1 + 1, [d](x0, x1) = x0 + x1, [g](x0, x1) = x0, [s](x0) = x0, [e](x0) = x0 + 1, [0] = 1, [g#](x0, x1) = x0 + 1 Strict: g#(e x, e y) -> g#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y Weak: g(e x, e y) -> e g(x, y) 1 + 1x + 0y >= 1 + 1x + 0y d(g(0(), x), y) -> e x 1 + 0x + 1y >= 1 + 1x d(g(g(0(), x), y), 0()) -> e y 2 + 0x + 0y >= 1 + 1y d(g(g(0(), x), y), s z) -> g(e x, d(g(g(0(), x), y), z)) 1 + 0x + 0y + 1z >= 1 + 1x + 0y + 0z d(g(x, y), z) -> g(d(x, z), e y) 0 + 1x + 0y + 1z >= 0 + 1x + 0y + 1z h(e x, y) -> h(d(x, y), s y) 2 + 1x + 1y >= 1 + 1x + 2y Qed