MAYBE

Problem:
 g(tt(),x) -> g(h(f(x,x)),s(x))
 h(f(0(),y)) -> tt()
 f(s(x),y) -> f(x,s(y))

Proof:
 DP Processor:
  DPs:
   g#(tt(),x) -> f#(x,x)
   g#(tt(),x) -> h#(f(x,x))
   g#(tt(),x) -> g#(h(f(x,x)),s(x))
   f#(s(x),y) -> f#(x,s(y))
  TRS:
   g(tt(),x) -> g(h(f(x,x)),s(x))
   h(f(0(),y)) -> tt()
   f(s(x),y) -> f(x,s(y))
  TDG Processor:
   DPs:
    g#(tt(),x) -> f#(x,x)
    g#(tt(),x) -> h#(f(x,x))
    g#(tt(),x) -> g#(h(f(x,x)),s(x))
    f#(s(x),y) -> f#(x,s(y))
   TRS:
    g(tt(),x) -> g(h(f(x,x)),s(x))
    h(f(0(),y)) -> tt()
    f(s(x),y) -> f(x,s(y))
   graph:
    f#(s(x),y) -> f#(x,s(y)) -> f#(s(x),y) -> f#(x,s(y))
    g#(tt(),x) -> f#(x,x) -> f#(s(x),y) -> f#(x,s(y))
    g#(tt(),x) -> g#(h(f(x,x)),s(x)) ->
    g#(tt(),x) -> g#(h(f(x,x)),s(x))
    g#(tt(),x) -> g#(h(f(x,x)),s(x)) -> g#(tt(),x) -> h#(f(x,x))
    g#(tt(),x) -> g#(h(f(x,x)),s(x)) -> g#(tt(),x) -> f#(x,x)
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 5/16
    DPs:
     g#(tt(),x) -> g#(h(f(x,x)),s(x))
    TRS:
     g(tt(),x) -> g(h(f(x,x)),s(x))
     h(f(0(),y)) -> tt()
     f(s(x),y) -> f(x,s(y))
    Open
    
    DPs:
     f#(s(x),y) -> f#(x,s(y))
    TRS:
     g(tt(),x) -> g(h(f(x,x)),s(x))
     h(f(0(),y)) -> tt()
     f(s(x),y) -> f(x,s(y))
    Subterm Criterion Processor:
     simple projection:
      pi(f#) = 0
     problem:
      DPs:
       
      TRS:
       g(tt(),x) -> g(h(f(x,x)),s(x))
       h(f(0(),y)) -> tt()
       f(s(x),y) -> f(x,s(y))
     Qed