MAYBE Time: 0.041824 TRS: { h(z, e x) -> h(c z, d(z, x)), d(z, g(x, y)) -> g(e x, d(z, y)), d(z, g(0(), 0())) -> e 0(), d(c z, g(g(x, y), 0())) -> g(d(c z, g(x, y)), d(z, g(x, y))), g(e x, e y) -> e g(x, y)} DP: DP: { h#(z, e x) -> h#(c z, d(z, x)), h#(z, e x) -> d#(z, x), d#(z, g(x, y)) -> d#(z, y), d#(z, g(x, y)) -> g#(e x, d(z, y)), d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y)), d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y)), d#(c z, g(g(x, y), 0())) -> g#(d(c z, g(x, y)), d(z, g(x, y))), g#(e x, e y) -> g#(x, y)} TRS: { h(z, e x) -> h(c z, d(z, x)), d(z, g(x, y)) -> g(e x, d(z, y)), d(z, g(0(), 0())) -> e 0(), d(c z, g(g(x, y), 0())) -> g(d(c z, g(x, y)), d(z, g(x, y))), g(e x, e y) -> e g(x, y)} UR: { d(z, g(x, y)) -> g(e x, d(z, y)), d(z, g(0(), 0())) -> e 0(), d(c z, g(g(x, y), 0())) -> g(d(c z, g(x, y)), d(z, g(x, y))), g(e x, e y) -> e g(x, y), a(w, v) -> w, a(w, v) -> v} EDG: {(h#(z, e x) -> h#(c z, d(z, x)), h#(z, e x) -> d#(z, x)) (h#(z, e x) -> h#(c z, d(z, x)), h#(z, e x) -> h#(c z, d(z, x))) (d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y)), d#(c z, g(g(x, y), 0())) -> g#(d(c z, g(x, y)), d(z, g(x, y)))) (d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y)), d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y))) (d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y)), d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y))) (d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y)), d#(z, g(x, y)) -> g#(e x, d(z, y))) (d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y)), d#(z, g(x, y)) -> d#(z, y)) (h#(z, e x) -> d#(z, x), d#(c z, g(g(x, y), 0())) -> g#(d(c z, g(x, y)), d(z, g(x, y)))) (h#(z, e x) -> d#(z, x), d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y))) (h#(z, e x) -> d#(z, x), d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y))) (h#(z, e x) -> d#(z, x), d#(z, g(x, y)) -> g#(e x, d(z, y))) (h#(z, e x) -> d#(z, x), d#(z, g(x, y)) -> d#(z, y)) (g#(e x, e y) -> g#(x, y), g#(e x, e y) -> g#(x, y)) (d#(z, g(x, y)) -> d#(z, y), d#(z, g(x, y)) -> d#(z, y)) (d#(z, g(x, y)) -> d#(z, y), d#(z, g(x, y)) -> g#(e x, d(z, y))) (d#(z, g(x, y)) -> d#(z, y), d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y))) (d#(z, g(x, y)) -> d#(z, y), d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y))) (d#(z, g(x, y)) -> d#(z, y), d#(c z, g(g(x, y), 0())) -> g#(d(c z, g(x, y)), d(z, g(x, y)))) (d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y)), d#(z, g(x, y)) -> d#(z, y)) (d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y)), d#(z, g(x, y)) -> g#(e x, d(z, y))) (d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y)), d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y))) (d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y)), d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y))) (d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y)), d#(c z, g(g(x, y), 0())) -> g#(d(c z, g(x, y)), d(z, g(x, y)))) (d#(z, g(x, y)) -> g#(e x, d(z, y)), g#(e x, e y) -> g#(x, y)) (d#(c z, g(g(x, y), 0())) -> g#(d(c z, g(x, y)), d(z, g(x, y))), g#(e x, e y) -> g#(x, y))} STATUS: arrows: 0.609375 SCCS (3): Scc: {h#(z, e x) -> h#(c z, d(z, x))} Scc: { d#(z, g(x, y)) -> d#(z, y), d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y)), d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y))} Scc: {g#(e x, e y) -> g#(x, y)} SCC (1): Strict: {h#(z, e x) -> h#(c z, d(z, x))} Weak: { h(z, e x) -> h(c z, d(z, x)), d(z, g(x, y)) -> g(e x, d(z, y)), d(z, g(0(), 0())) -> e 0(), d(c z, g(g(x, y), 0())) -> g(d(c z, g(x, y)), d(z, g(x, y))), g(e x, e y) -> e g(x, y)} Fail SCC (3): Strict: { d#(z, g(x, y)) -> d#(z, y), d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y)), d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y))} Weak: { h(z, e x) -> h(c z, d(z, x)), d(z, g(x, y)) -> g(e x, d(z, y)), d(z, g(0(), 0())) -> e 0(), d(c z, g(g(x, y), 0())) -> g(d(c z, g(x, y)), d(z, g(x, y))), 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, [d](x0, x1) = x0 + x1, [g](x0, x1) = x0 + x1, [c](x0) = x0, [e](x0) = 0, [0] = 1, [d#](x0, x1) = x0 Strict: d#(c z, g(g(x, y), 0())) -> d#(c z, g(x, y)) 1 + 0z + 1x + 1y >= 0 + 0z + 1x + 1y d#(c z, g(g(x, y), 0())) -> d#(z, g(x, y)) 1 + 0z + 1x + 1y >= 0 + 0z + 1x + 1y d#(z, g(x, y)) -> d#(z, y) 0 + 0z + 1x + 1y >= 0 + 0z + 1y Weak: g(e x, e y) -> e g(x, y) 0 + 0x + 0y >= 0 + 0x + 0y d(c z, g(g(x, y), 0())) -> g(d(c z, g(x, y)), d(z, g(x, y))) 1 + 1z + 1x + 1y >= 0 + 2z + 2x + 2y d(z, g(0(), 0())) -> e 0() 2 + 1z >= 0 d(z, g(x, y)) -> g(e x, d(z, y)) 0 + 1z + 1x + 1y >= 0 + 1z + 0x + 1y h(z, e x) -> h(c z, d(z, x)) 0 + 1z + 0x >= 0 + 2z + 1x SCCS (1): Scc: {d#(z, g(x, y)) -> d#(z, y)} SCC (1): Strict: {d#(z, g(x, y)) -> d#(z, y)} Weak: { h(z, e x) -> h(c z, d(z, x)), d(z, g(x, y)) -> g(e x, d(z, y)), d(z, g(0(), 0())) -> e 0(), d(c z, g(g(x, y), 0())) -> g(d(c z, g(x, y)), d(z, g(x, y))), 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, [c](x0) = x0, [e](x0) = 1, [0] = 1, [d#](x0, x1) = x0 Strict: d#(z, g(x, y)) -> d#(z, y) 1 + 0z + 0x + 1y >= 0 + 0z + 1y Weak: g(e x, e y) -> e g(x, y) 2 + 0x + 0y >= 1 + 0x + 0y d(c z, g(g(x, y), 0())) -> g(d(c z, g(x, y)), d(z, g(x, y))) 0 + 1z + 0x + 0y >= 1 + 1z + 0x + 0y d(z, g(0(), 0())) -> e 0() 0 + 1z >= 1 d(z, g(x, y)) -> g(e x, d(z, y)) 0 + 1z + 0x + 0y >= 1 + 1z + 0x + 0y h(z, e x) -> h(c z, d(z, x)) 2 + 1z + 0x >= 1 + 2z + 0x Qed SCC (1): Strict: {g#(e x, e y) -> g#(x, y)} Weak: { h(z, e x) -> h(c z, d(z, x)), d(z, g(x, y)) -> g(e x, d(z, y)), d(z, g(0(), 0())) -> e 0(), d(c z, g(g(x, y), 0())) -> g(d(c z, g(x, y)), d(z, g(x, y))), 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) = 0, [c](x0) = x0, [e](x0) = x0 + 1, [0] = 1, [g#](x0, x1) = x0 Strict: g#(e x, e y) -> g#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: g(e x, e y) -> e g(x, y) 0 + 0x + 0y >= 1 + 0x + 0y d(c z, g(g(x, y), 0())) -> g(d(c z, g(x, y)), d(z, g(x, y))) 0 + 1z + 0x + 0y >= 0 + 0z + 0x + 0y d(z, g(0(), 0())) -> e 0() 0 + 1z >= 2 d(z, g(x, y)) -> g(e x, d(z, y)) 0 + 1z + 0x + 0y >= 0 + 0z + 0x + 0y h(z, e x) -> h(c z, d(z, x)) 2 + 1z + 1x >= 1 + 2z + 0x Qed