MAYBE Problem: h(e(x),y) -> h(d(x,y),s(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) d(g(x,y),z) -> g(d(x,z),e(y)) g(e(x),e(y)) -> e(g(x,y)) Proof: DP Processor: DPs: h#(e(x),y) -> d#(x,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(x,y),z) -> d#(x,z) d#(g(x,y),z) -> g#(d(x,z),e(y)) g#(e(x),e(y)) -> g#(x,y) TRS: h(e(x),y) -> h(d(x,y),s(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) d(g(x,y),z) -> g(d(x,z),e(y)) g(e(x),e(y)) -> e(g(x,y)) Usable Rule Processor: DPs: h#(e(x),y) -> d#(x,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(x,y),z) -> d#(x,z) d#(g(x,y),z) -> g#(d(x,z),e(y)) g#(e(x),e(y)) -> g#(x,y) TRS: f9(x,y) -> x f9(x,y) -> 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) d(g(x,y),z) -> g(d(x,z),e(y)) g(e(x),e(y)) -> e(g(x,y)) TDG Processor: DPs: h#(e(x),y) -> d#(x,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(x,y),z) -> d#(x,z) d#(g(x,y),z) -> g#(d(x,z),e(y)) g#(e(x),e(y)) -> g#(x,y) TRS: f9(x,y) -> x f9(x,y) -> 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) d(g(x,y),z) -> g(d(x,z),e(y)) g(e(x),e(y)) -> e(g(x,y)) graph: g#(e(x),e(y)) -> g#(x,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) 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) 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(x,y),z) -> g#(d(x,z),e(y)) -> g#(e(x),e(y)) -> g#(x,y) 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(x,y),z) -> d#(x,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)) d#(g(x,y),z) -> d#(x,z) -> d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),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(x,y),z) -> d#(x,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)) 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) -> h#(d(x,y),s(y)) -> h#(e(x),y) -> h#(d(x,y),s(y)) h#(e(x),y) -> h#(d(x,y),s(y)) -> h#(e(x),y) -> d#(x,y) Restore Modifier: DPs: h#(e(x),y) -> d#(x,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(x,y),z) -> d#(x,z) d#(g(x,y),z) -> g#(d(x,z),e(y)) g#(e(x),e(y)) -> g#(x,y) TRS: h(e(x),y) -> h(d(x,y),s(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) d(g(x,y),z) -> g(d(x,z),e(y)) g(e(x),e(y)) -> e(g(x,y)) SCC Processor: #sccs: 3 #rules: 4 #arcs: 17/49 DPs: h#(e(x),y) -> h#(d(x,y),s(y)) TRS: h(e(x),y) -> h(d(x,y),s(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) d(g(x,y),z) -> g(d(x,z),e(y)) g(e(x),e(y)) -> e(g(x,y)) Open DPs: d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z) d#(g(x,y),z) -> d#(x,z) TRS: h(e(x),y) -> h(d(x,y),s(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) d(g(x,y),z) -> g(d(x,z),e(y)) g(e(x),e(y)) -> e(g(x,y)) Matrix Interpretation Processor: dimension: 1 interpretation: [d#](x0, x1) = x0 + 1, [g](x0, x1) = x0 + 1, [0] = 0, [s](x0) = 0, [d](x0, x1) = x0, [h](x0, x1) = 0, [e](x0) = 1 orientation: d#(g(g(0(),x),y),s(z)) = 3 >= 3 = d#(g(g(0(),x),y),z) d#(g(x,y),z) = x + 2 >= x + 1 = d#(x,z) h(e(x),y) = 0 >= 0 = h(d(x,y),s(y)) d(g(g(0(),x),y),s(z)) = 2 >= 2 = g(e(x),d(g(g(0(),x),y),z)) d(g(g(0(),x),y),0()) = 2 >= 1 = e(y) d(g(0(),x),y) = 1 >= 1 = e(x) d(g(x,y),z) = x + 1 >= x + 1 = g(d(x,z),e(y)) g(e(x),e(y)) = 2 >= 1 = e(g(x,y)) problem: DPs: d#(g(g(0(),x),y),s(z)) -> d#(g(g(0(),x),y),z) TRS: h(e(x),y) -> h(d(x,y),s(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) d(g(x,y),z) -> g(d(x,z),e(y)) g(e(x),e(y)) -> e(g(x,y)) Matrix Interpretation Processor: dimension: 1 interpretation: [d#](x0, x1) = x0 + x1 + 1, [g](x0, x1) = x0, [0] = 1, [s](x0) = x0 + 1, [d](x0, x1) = 0, [h](x0, x1) = 0, [e](x0) = 0 orientation: d#(g(g(0(),x),y),s(z)) = z + 3 >= z + 2 = d#(g(g(0(),x),y),z) h(e(x),y) = 0 >= 0 = h(d(x,y),s(y)) d(g(g(0(),x),y),s(z)) = 0 >= 0 = g(e(x),d(g(g(0(),x),y),z)) d(g(g(0(),x),y),0()) = 0 >= 0 = e(y) d(g(0(),x),y) = 0 >= 0 = e(x) d(g(x,y),z) = 0 >= 0 = g(d(x,z),e(y)) g(e(x),e(y)) = 0 >= 0 = e(g(x,y)) problem: DPs: TRS: h(e(x),y) -> h(d(x,y),s(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) d(g(x,y),z) -> g(d(x,z),e(y)) g(e(x),e(y)) -> e(g(x,y)) Qed DPs: g#(e(x),e(y)) -> g#(x,y) TRS: h(e(x),y) -> h(d(x,y),s(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) d(g(x,y),z) -> g(d(x,z),e(y)) g(e(x),e(y)) -> e(g(x,y)) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0, x1) = x1 + 1, [g](x0, x1) = x1, [0] = 0, [s](x0) = 0, [d](x0, x1) = x0 + 1, [h](x0, x1) = 0, [e](x0) = x0 + 1 orientation: g#(e(x),e(y)) = y + 2 >= y + 1 = g#(x,y) h(e(x),y) = 0 >= 0 = h(d(x,y),s(y)) d(g(g(0(),x),y),s(z)) = y + 1 >= y + 1 = g(e(x),d(g(g(0(),x),y),z)) d(g(g(0(),x),y),0()) = y + 1 >= y + 1 = e(y) d(g(0(),x),y) = x + 1 >= x + 1 = e(x) d(g(x,y),z) = y + 1 >= y + 1 = g(d(x,z),e(y)) g(e(x),e(y)) = y + 1 >= y + 1 = e(g(x,y)) problem: DPs: TRS: h(e(x),y) -> h(d(x,y),s(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) d(g(x,y),z) -> g(d(x,z),e(y)) g(e(x),e(y)) -> e(g(x,y)) Qed