MAYBE

Problem:
 h(z,e(x)) -> h(c(z),d(z,x))
 d(z,g(0(),0())) -> e(0())
 d(z,g(x,y)) -> g(e(x),d(z,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)) -> e(g(x,y))

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