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

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   
  critical peaks: 6
  f(c(),b()) <-0|0[]- f(a(),b()) -2|[]-> d()
  f(a(),c()) <-1|1[]- f(a(),b()) -2|[]-> d()
  f(c(),c()) <-3|[]- f(c(),c()) -4|[]-> f(c(),c())
  f(c(),c()) <-4|[]- f(c(),c()) -3|[]-> f(c(),c())
  f(a(),c()) <-5|[]- d() -6|[]-> f(c(),b())
  f(c(),b()) <-6|[]- d() -5|[]-> f(a(),c())
  Shift Processor lab=left (dd):
   
   strict:
    f(a(),b()) -> f(c(),b())
    f(a(),b()) -> d()
    d() -> f(c(),b())
    f(a(),b()) -> f(a(),c())
    f(a(),b()) -> d()
    d() -> f(a(),c())
    f(c(),c()) -> f(c(),c())
    f(c(),c()) -> f(c(),c())
    f(c(),c()) -> f(c(),c())
    f(c(),c()) -> f(c(),c())
    d() -> f(a(),c())
    d() -> f(c(),b())
    f(a(),c()) -> f(c(),c())
    f(c(),b()) -> f(c(),c())
    d() -> f(c(),b())
    d() -> f(a(),c())
    f(c(),b()) -> f(c(),c())
    f(a(),c()) -> f(c(),c())
   weak:
    a() -> c()
    b() -> c()
    f(a(),b()) -> d()
    f(x,c()) -> f(c(),c())
    f(c(),x) -> f(c(),c())
    d() -> f(a(),c())
    d() -> f(c(),b())
   Matrix Interpretation Processor: dim=3
    
    interpretation:
           [1]
     [d] = [1]
           [1],
     
                   [1 0 1]     [1 1 0]  
     [f](x0, x1) = [0 0 1]x0 + [0 0 0]x1
                   [0 1 0]     [0 0 0]  ,
     
           [0]
     [b] = [1]
           [0],
     
           [0]
     [c] = [0]
           [0],
     
           [0]
     [a] = [1]
           [1]
    orientation:
                  [2]    [1]             
     f(a(),b()) = [1] >= [0] = f(c(),b())
                  [1]    [0]             
     
                  [2]    [1]      
     f(a(),b()) = [1] >= [1] = d()
                  [1]    [1]      
     
           [1]    [1]             
     d() = [1] >= [0] = f(c(),b())
           [1]    [0]             
     
                  [2]    [1]             
     f(a(),b()) = [1] >= [1] = f(a(),c())
                  [1]    [1]             
     
                  [2]    [1]      
     f(a(),b()) = [1] >= [1] = d()
                  [1]    [1]      
     
           [1]    [1]             
     d() = [1] >= [1] = f(a(),c())
           [1]    [1]             
     
                  [0]    [0]             
     f(c(),c()) = [0] >= [0] = f(c(),c())
                  [0]    [0]             
     
                  [0]    [0]             
     f(c(),c()) = [0] >= [0] = f(c(),c())
                  [0]    [0]             
     
                  [0]    [0]             
     f(c(),c()) = [0] >= [0] = f(c(),c())
                  [0]    [0]             
     
                  [0]    [0]             
     f(c(),c()) = [0] >= [0] = f(c(),c())
                  [0]    [0]             
     
           [1]    [1]             
     d() = [1] >= [1] = f(a(),c())
           [1]    [1]             
     
           [1]    [1]             
     d() = [1] >= [0] = f(c(),b())
           [1]    [0]             
     
                  [1]    [0]             
     f(a(),c()) = [1] >= [0] = f(c(),c())
                  [1]    [0]             
     
                  [1]    [0]             
     f(c(),b()) = [0] >= [0] = f(c(),c())
                  [0]    [0]             
     
           [1]    [1]             
     d() = [1] >= [0] = f(c(),b())
           [1]    [0]             
     
           [1]    [1]             
     d() = [1] >= [1] = f(a(),c())
           [1]    [1]             
     
                  [1]    [0]             
     f(c(),b()) = [0] >= [0] = f(c(),c())
                  [0]    [0]             
     
                  [1]    [0]             
     f(a(),c()) = [1] >= [0] = f(c(),c())
                  [1]    [0]             
     
           [0]    [0]      
     a() = [1] >= [0] = c()
           [1]    [0]      
     
           [0]    [0]      
     b() = [1] >= [0] = c()
           [0]    [0]      
     
                [1 0 1]     [0]             
     f(x,c()) = [0 0 1]x >= [0] = f(c(),c())
                [0 1 0]     [0]             
     
                [1 1 0]     [0]             
     f(c(),x) = [0 0 0]x >= [0] = f(c(),c())
                [0 0 0]     [0]             
    problem:
     
     strict:
      d() -> f(c(),b())
      d() -> f(a(),c())
      f(c(),c()) -> f(c(),c())
      f(c(),c()) -> f(c(),c())
      f(c(),c()) -> f(c(),c())
      f(c(),c()) -> f(c(),c())
      d() -> f(a(),c())
      d() -> f(c(),b())
      d() -> f(c(),b())
      d() -> f(a(),c())
     weak:
      a() -> c()
      b() -> c()
      f(x,c()) -> f(c(),c())
      f(c(),x) -> f(c(),c())
      d() -> f(a(),c())
      d() -> f(c(),b())
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [d] = 5,
      
      [f](x0, x1) = x0 + x1 + 4,
      
      [b] = 0,
      
      [c] = 0,
      
      [a] = 1
     orientation:
      d() = 5 >= 4 = f(c(),b())
      
      d() = 5 >= 5 = f(a(),c())
      
      f(c(),c()) = 4 >= 4 = f(c(),c())
      
      f(c(),c()) = 4 >= 4 = f(c(),c())
      
      f(c(),c()) = 4 >= 4 = f(c(),c())
      
      f(c(),c()) = 4 >= 4 = f(c(),c())
      
      d() = 5 >= 5 = f(a(),c())
      
      d() = 5 >= 4 = f(c(),b())
      
      d() = 5 >= 4 = f(c(),b())
      
      d() = 5 >= 5 = f(a(),c())
      
      a() = 1 >= 0 = c()
      
      b() = 0 >= 0 = c()
      
      f(x,c()) = x + 4 >= 4 = f(c(),c())
      
      f(c(),x) = x + 4 >= 4 = f(c(),c())
     problem:
      
      strict:
       d() -> f(a(),c())
       f(c(),c()) -> f(c(),c())
       f(c(),c()) -> f(c(),c())
       f(c(),c()) -> f(c(),c())
       f(c(),c()) -> f(c(),c())
       d() -> f(a(),c())
       d() -> f(a(),c())
      weak:
       b() -> c()
       f(x,c()) -> f(c(),c())
       f(c(),x) -> f(c(),c())
       d() -> f(a(),c())
     Matrix Interpretation Processor: dim=2
      
      interpretation:
             [2]
       [d] = [3],
       
                     [2 1]     [2 0]  
       [f](x0, x1) = [0 2]x0 + [0 0]x1,
       
             [0]
       [b] = [1],
       
             [0]
       [c] = [0],
       
             [0]
       [a] = [1]
      orientation:
             [2]    [1]             
       d() = [3] >= [2] = f(a(),c())
       
                    [0]    [0]             
       f(c(),c()) = [0] >= [0] = f(c(),c())
       
                    [0]    [0]             
       f(c(),c()) = [0] >= [0] = f(c(),c())
       
                    [0]    [0]             
       f(c(),c()) = [0] >= [0] = f(c(),c())
       
                    [0]    [0]             
       f(c(),c()) = [0] >= [0] = f(c(),c())
       
             [2]    [1]             
       d() = [3] >= [2] = f(a(),c())
       
             [2]    [1]             
       d() = [3] >= [2] = f(a(),c())
       
             [0]    [0]      
       b() = [1] >= [0] = c()
       
                  [2 1]     [0]             
       f(x,c()) = [0 2]x >= [0] = f(c(),c())
       
                  [2 0]     [0]             
       f(c(),x) = [0 0]x >= [0] = f(c(),c())
      problem:
       
       strict:
        f(c(),c()) -> f(c(),c())
        f(c(),c()) -> f(c(),c())
        f(c(),c()) -> f(c(),c())
        f(c(),c()) -> f(c(),c())
       weak:
        b() -> c()
        f(x,c()) -> f(c(),c())
        f(c(),x) -> f(c(),c())
      Matrix Interpretation Processor: dim=3
       
       interpretation:
                      [1 0 0]     [1 0 0]  
        [f](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                      [0 0 0]     [0 0 0]  ,
        
              [1]
        [b] = [0]
              [0],
        
              [0]
        [c] = [0]
              [0]
       orientation:
                     [0]    [0]             
        f(c(),c()) = [0] >= [0] = f(c(),c())
                     [0]    [0]             
        
                     [0]    [0]             
        f(c(),c()) = [0] >= [0] = f(c(),c())
                     [0]    [0]             
        
                     [0]    [0]             
        f(c(),c()) = [0] >= [0] = f(c(),c())
                     [0]    [0]             
        
                     [0]    [0]             
        f(c(),c()) = [0] >= [0] = f(c(),c())
                     [0]    [0]             
        
              [1]    [0]      
        b() = [0] >= [0] = c()
              [0]    [0]      
        
                   [1 0 0]     [0]             
        f(x,c()) = [0 0 0]x >= [0] = f(c(),c())
                   [0 0 0]     [0]             
        
                   [1 0 0]     [0]             
        f(c(),x) = [0 0 0]x >= [0] = f(c(),c())
                   [0 0 0]     [0]             
       problem:
        
        strict:
         f(c(),c()) -> f(c(),c())
         f(c(),c()) -> f(c(),c())
         f(c(),c()) -> f(c(),c())
         f(c(),c()) -> f(c(),c())
        weak:
         f(x,c()) -> f(c(),c())
         f(c(),x) -> f(c(),c())
       Shift Processor (ldh) lab=left (force):
        
        strict:
         
        weak:
         
        Decreasing Processor:
         The following diagrams are decreasing:
         peak:
          f(c(),b()) <-0|0[1]- f(a(),b()) -2|[1]-> d()
         joins:
          
          d() -6|[0]-> f(c(),b())
         peak:
          f(a(),c()) <-1|1[1]- f(a(),b()) -2|[1]-> d()
         joins:
          
          d() -5|[0]-> f(a(),c())
         peak:
          f(c(),c()) <-3|[1]- f(c(),c()) -4|[1]-> f(c(),c())
         joins:
          
          
         peak:
          f(c(),c()) <-4|[1]- f(c(),c()) -3|[1]-> f(c(),c())
         joins:
          
          
         peak:
          f(a(),c()) <-5|[1]- d() -6|[1]-> f(c(),b())
         joins:
          f(a(),c()) -3|[0]-> f(c(),c())
          f(c(),b()) -4|[0]-> f(c(),c())
         peak:
          f(c(),b()) <-6|[1]- d() -5|[1]-> f(a(),c())
         joins:
          f(c(),b()) -4|[0]-> f(c(),c())
          f(a(),c()) -3|[0]-> f(c(),c())
         Qed