Problem:
 f(h(x,d()),y) -> f(h(y,d()),x)
 h(c(),x) -> h(x,x)

Proof:
 Church Rosser Transformation Processor (no redundant rules):
  strict:
   
  weak:
   
  critical peaks: 1
   f(h(d(),d()),y) <-0|0[]- f(h(c(),d()),y) -1|[]-> f(h(y,d()),c())
  Redundant Rules Transformation:
   h(c(),x) -> h(x,x)
   f(h(x,d()),y) -> f(h(y,d()),x)
   f(h(y,d()),c()) -> f(h(d(),d()),y)
   Church Rosser Transformation Processor:
    strict:
     
    weak:
     
    critical peaks: 4
     f(h(d(),d()),y) <-0|0[]- f(h(c(),d()),y) -1|[]-> f(h(y,d()),c())
     f(h(d(),d()),c()) <-0|0[]- f(h(c(),d()),c()) -2|[]-> f(h(d(),d()),c())
     f(h(c(),d()),y) <-1|[]- f(h(y,d()),c()) -2|[]-> f(h(d(),d()),y)
     f(h(d(),d()),x) <-2|[]- f(h(x,d()),c()) -1|[]-> f(h(c(),d()),x)
    Shift Processor lab=left (dd) (force):
     strict:
      f(h(c(),d()),y) -> f(h(d(),d()),y)
      f(h(c(),d()),y) -> f(h(y,d()),c())
      f(h(y,d()),c()) -> f(h(d(),d()),y)
      f(h(c(),d()),c()) -> f(h(d(),d()),c())
      f(h(c(),d()),c()) -> f(h(d(),d()),c())
      f(h(y,d()),c()) -> f(h(c(),d()),y)
      f(h(y,d()),c()) -> f(h(d(),d()),y)
      f(h(c(),d()),y) -> f(h(d(),d()),y)
      f(h(x,d()),c()) -> f(h(d(),d()),x)
      f(h(x,d()),c()) -> f(h(c(),d()),x)
      f(h(c(),d()),x) -> f(h(d(),d()),x)
     weak:
      h(c(),x) -> h(x,x)
      f(h(x,d()),y) -> f(h(y,d()),x)
      f(h(y,d()),c()) -> f(h(d(),d()),y)
     Shift Processor (ldh) lab=left (force):
      strict:
       
      weak:
       
      Rule Labeling Processor:
       strict:
        
       weak:
        
       rule labeling (right):
        h(c(),x) -> h(x,x): 1
        f(h(x,d()),y) -> f(h(y,d()),x): 2
        f(h(y,d()),c()) -> f(h(d(),d()),y): 0
       Rule Labeling Processor:
        strict:
         
        weak:
         
        rule labeling (left):
         h(c(),x) -> h(x,x): 0
         f(h(x,d()),y) -> f(h(y,d()),x): 0
         f(h(y,d()),c()) -> f(h(d(),d()),y): 0
        Decreasing Processor:
         The following diagrams are decreasing:
         peak:
          f(h(d(),d()),y) <-0|0[==0,==1,=>1]- f(h(c(),d()),y) -1|[==0,==1,?=2]-> f(h(y,d()),c())
         joins (1):
          
          f(h(y,d()),c()) -2|[==0,==1,>>0]-> f(h(d(),d()),y)
         peak:
          f(h(d(),d()),c()) <-0|0[==0,==1,=?1]- f(h(c(),d()),c()) -2|
                                                [==0,==1,>=0]-> f(h(d(),d()),c())
         joins (1):
          
          
         peak:
          f(h(c(),d()),y) <-1|[==0,==1,=?2]- f(h(y,d()),c()) -2|[==0,==1,>=0]-> f(h(d(),d()),y)
         joins (1):
          f(h(c(),d()),y) -0|0[==0,==1,>?1]-> f(h(d(),d()),y)
          
         peak:
          f(h(d(),d()),x) <-2|[==0,==1,=>0]- f(h(x,d()),c()) -1|[==0,==1,?=2]-> f(h(c(),d()),x)
         joins (1):
          
          f(h(c(),d()),x) -0|0[==0,==1,?>1]-> f(h(d(),d()),x)
         Qed