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))
  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:
    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))
   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)
   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))
    Subterm Criterion Processor:
     simple projection:
      pi(d#) = 1
     problem:
      DPs:
       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))
     Subterm Criterion Processor:
      simple projection:
       pi(d#) = 0
      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))
    Subterm Criterion Processor:
     simple projection:
      pi(g#) = 1
     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