Problem:
 f(a()) -> f(g(b(),b()))
 a() -> g(c(),c())
 c() -> d()
 d() -> b()
 b() -> d()

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   
  critical peaks: 1
  f(g(c(),c())) <-1|0[]- f(a()) -0|[]-> f(g(b(),b()))
  Shift Processor lab=left (dd):
   
   strict:
    f(a()) -> f(g(c(),c()))
    f(a()) -> f(g(b(),b()))
    f(g(c(),c())) -> f(g(c(),d()))
    f(g(c(),d())) -> f(g(d(),d()))
    f(g(b(),b())) -> f(g(b(),d()))
    f(g(b(),d())) -> f(g(d(),d()))
    f(g(c(),c())) -> f(g(c(),d()))
    f(g(c(),d())) -> f(g(d(),d()))
    f(g(b(),b())) -> f(g(d(),b()))
    f(g(d(),b())) -> f(g(d(),d()))
    f(g(c(),c())) -> f(g(d(),c()))
    f(g(d(),c())) -> f(g(d(),d()))
    f(g(b(),b())) -> f(g(b(),d()))
    f(g(b(),d())) -> f(g(d(),d()))
    f(g(c(),c())) -> f(g(d(),c()))
    f(g(d(),c())) -> f(g(d(),d()))
    f(g(b(),b())) -> f(g(d(),b()))
    f(g(d(),b())) -> f(g(d(),d()))
   weak:
    f(a()) -> f(g(b(),b()))
    a() -> g(c(),c())
    c() -> d()
    d() -> b()
    b() -> d()
   LPO Processor:
    precedence:
     a > d ~ c ~ g ~ b ~ f
    problem:
     
     strict:
      f(g(c(),c())) -> f(g(c(),d()))
      f(g(c(),d())) -> f(g(d(),d()))
      f(g(b(),b())) -> f(g(b(),d()))
      f(g(b(),d())) -> f(g(d(),d()))
      f(g(c(),c())) -> f(g(c(),d()))
      f(g(c(),d())) -> f(g(d(),d()))
      f(g(b(),b())) -> f(g(d(),b()))
      f(g(d(),b())) -> f(g(d(),d()))
      f(g(c(),c())) -> f(g(d(),c()))
      f(g(d(),c())) -> f(g(d(),d()))
      f(g(b(),b())) -> f(g(b(),d()))
      f(g(b(),d())) -> f(g(d(),d()))
      f(g(c(),c())) -> f(g(d(),c()))
      f(g(d(),c())) -> f(g(d(),d()))
      f(g(b(),b())) -> f(g(d(),b()))
      f(g(d(),b())) -> f(g(d(),d()))
     weak:
      c() -> d()
      d() -> b()
      b() -> d()
    LPO Processor:
     precedence:
      g > c > d ~ b ~ f
     problem:
      
      strict:
       f(g(b(),b())) -> f(g(b(),d()))
       f(g(b(),d())) -> f(g(d(),d()))
       f(g(b(),b())) -> f(g(d(),b()))
       f(g(d(),b())) -> f(g(d(),d()))
       f(g(b(),b())) -> f(g(b(),d()))
       f(g(b(),d())) -> f(g(d(),d()))
       f(g(b(),b())) -> f(g(d(),b()))
       f(g(d(),b())) -> f(g(d(),d()))
      weak:
       d() -> b()
       b() -> d()
     Shift Processor (ldh) lab=left (force):
      
      strict:
       
      weak:
       
      Decreasing Processor:
       The following diagrams are decreasing:
       peak:
        f(g(c(),c())) <-1|0[1]- f(a()) -0|[1]-> f(g(b(),b()))
       joins:
        f(g(c(),c())) -2|0,1[0]-> f(g(c(),d())) -2|0,0[0]-> f(g(d(),d()))
        f(g(b(),b())) -4|0,1[0]-> f(g(b(),d())) -4|0,0[0]-> f(g(d(),d()))
       Qed