Problem:
 +(x,0()) -> x
 +(x,s(y)) -> s(+(x,y))
 d(0()) -> 0()
 d(s(x)) -> s(s(d(x)))
 f(0()) -> 0()
 f(s(x)) -> +(+(s(x),s(x)),s(x))
 f(g(0())) -> +(+(g(0()),g(0())),g(0()))
 g(x) -> s(d(x))

Proof:
 Church Rosser Transformation Processor (dup):
  
  strict:
   f(s(x)) -> +(+(s(x),s(x)),s(x))
  weak:
   +(x,0()) -> x
   +(x,s(y)) -> s(+(x,y))
   d(0()) -> 0()
   d(s(x)) -> s(s(d(x)))
   f(0()) -> 0()
   f(g(0())) -> +(+(g(0()),g(0())),g(0()))
   g(x) -> s(d(x))
  critical peaks: 1
  f(s(d(0()))) <-7|0[]- f(g(0())) -6|[]-> +(+(g(0()),g(0())),g(0()))
  LPO Processor:
   precedence:
    f > g ~ + > d > s ~ 0
   problem:
    
    strict:
     
    weak:
     
   Shift Processor (no label):
    
    strict:
     
    weak:
     
    Shift Processor lab=left (dd):
     
     strict:
      f(g(0())) -> f(s(d(0())))
      f(g(0())) -> +(+(g(0()),g(0())),g(0()))
      f(s(d(0()))) -> +(+(s(d(0())),s(d(0()))),s(d(0())))
      +(+(g(0()),g(0())),g(0())) -> +(+(g(0()),g(0())),s(d(0())))
      +(+(g(0()),g(0())),s(d(0()))) -> +(+(g(0()),s(d(0()))),s(d(0())))
      +(+(g(0()),s(d(0()))),s(d(0()))) -> +(+(s(d(0())),s(d(0()))),s(d(0())))
      f(s(d(0()))) -> +(+(s(d(0())),s(d(0()))),s(d(0())))
      +(+(g(0()),g(0())),g(0())) -> +(+(g(0()),s(d(0()))),g(0()))
      +(+(g(0()),s(d(0()))),g(0())) -> +(+(g(0()),s(d(0()))),s(d(0())))
      +(+(g(0()),s(d(0()))),s(d(0()))) -> +(+(s(d(0())),s(d(0()))),s(d(0())))
      f(s(d(0()))) -> +(+(s(d(0())),s(d(0()))),s(d(0())))
      +(+(g(0()),g(0())),g(0())) -> +(+(g(0()),g(0())),s(d(0())))
      +(+(g(0()),g(0())),s(d(0()))) -> +(+(s(d(0())),g(0())),s(d(0())))
      +(+(s(d(0())),g(0())),s(d(0()))) -> +(+(s(d(0())),s(d(0()))),s(d(0())))
      f(s(d(0()))) -> +(+(s(d(0())),s(d(0()))),s(d(0())))
      +(+(g(0()),g(0())),g(0())) -> +(+(s(d(0())),g(0())),g(0()))
      +(+(s(d(0())),g(0())),g(0())) -> +(+(s(d(0())),g(0())),s(d(0())))
      +(+(s(d(0())),g(0())),s(d(0()))) -> +(+(s(d(0())),s(d(0()))),s(d(0())))
      f(s(d(0()))) -> +(+(s(d(0())),s(d(0()))),s(d(0())))
      +(+(g(0()),g(0())),g(0())) -> +(+(g(0()),s(d(0()))),g(0()))
      +(+(g(0()),s(d(0()))),g(0())) -> +(+(s(d(0())),s(d(0()))),g(0()))
      +(+(s(d(0())),s(d(0()))),g(0())) -> +(+(s(d(0())),s(d(0()))),s(d(0())))
      f(s(d(0()))) -> +(+(s(d(0())),s(d(0()))),s(d(0())))
      +(+(g(0()),g(0())),g(0())) -> +(+(s(d(0())),g(0())),g(0()))
      +(+(s(d(0())),g(0())),g(0())) -> +(+(s(d(0())),s(d(0()))),g(0()))
      +(+(s(d(0())),s(d(0()))),g(0())) -> +(+(s(d(0())),s(d(0()))),s(d(0())))
     weak:
      +(x,0()) -> x
      +(x,s(y)) -> s(+(x,y))
      d(0()) -> 0()
      d(s(x)) -> s(s(d(x)))
      f(0()) -> 0()
      f(s(x)) -> +(+(s(x),s(x)),s(x))
      f(g(0())) -> +(+(g(0()),g(0())),g(0()))
      g(x) -> s(d(x))
     LPO Processor:
      precedence:
       g > f ~ d > + > s ~ 0
      problem:
       
       strict:
        
       weak:
        
      Shift Processor (ldh) lab=left (force):
       
       strict:
        
       weak:
        
       Decreasing Processor:
        The following diagrams are decreasing:
        peak:
         f(s(d(0()))) <-7|0[1]- f(g(0())) -6|[1]-> +(+(g(0()),g(0())),g(0()))
        joins:
         f(s(d(0()))) -5|[0]-> +(+(s(d(0())),s(d(0()))),s(d(0())))
         +(+(g(0()),g(0())),g(0())) -7|1[0]-> +(+(g(0()),g(0())),s(d(0()))) -7|0,1[0]-> 
          +(+(g(0()),s(d(0()))),s(d(0()))) -7|0,0[0]-> +(+(s(d(0())),s(d(0()))),s(d(0())))
        Qed