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] = [0]
           [0],
     
                   [1 0 0]     [1 0 0]  
     [f](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                   [0 0 0]     [0 0 0]  ,
     
           [0]
     [b] = [1]
           [0],
     
           [0]
     [c] = [0]
           [0],
     
           [1]
     [a] = [0]
           [0]
    orientation:
                  [1]    [0]             
     f(a(),b()) = [0] >= [0] = f(c(),b())
                  [0]    [0]             
     
                  [1]    [1]      
     f(a(),b()) = [0] >= [0] = d()
                  [0]    [0]      
     
           [1]    [0]             
     d() = [0] >= [0] = f(c(),b())
           [0]    [0]             
     
                  [1]    [1]             
     f(a(),b()) = [0] >= [0] = f(a(),c())
                  [0]    [0]             
     
                  [1]    [1]      
     f(a(),b()) = [0] >= [0] = d()
                  [0]    [0]      
     
           [1]    [1]             
     d() = [0] >= [0] = f(a(),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]             
     
                  [0]    [0]             
     f(c(),c()) = [0] >= [0] = f(c(),c())
                  [0]    [0]             
     
           [1]    [1]             
     d() = [0] >= [0] = f(a(),c())
           [0]    [0]             
     
           [1]    [0]             
     d() = [0] >= [0] = f(c(),b())
           [0]    [0]             
     
                  [1]    [0]             
     f(a(),c()) = [0] >= [0] = f(c(),c())
                  [0]    [0]             
     
                  [0]    [0]             
     f(c(),b()) = [0] >= [0] = f(c(),c())
                  [0]    [0]             
     
           [1]    [0]             
     d() = [0] >= [0] = f(c(),b())
           [0]    [0]             
     
           [1]    [1]             
     d() = [0] >= [0] = f(a(),c())
           [0]    [0]             
     
                  [0]    [0]             
     f(c(),b()) = [0] >= [0] = f(c(),c())
                  [0]    [0]             
     
                  [1]    [0]             
     f(a(),c()) = [0] >= [0] = f(c(),c())
                  [0]    [0]             
     
           [1]    [0]      
     a() = [0] >= [0] = c()
           [0]    [0]      
     
           [0]    [0]      
     b() = [1] >= [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(a(),b()) -> d()
      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())
      f(c(),b()) -> f(c(),c())
      d() -> f(a(),c())
      f(c(),b()) -> f(c(),c())
     weak:
      b() -> c()
      f(a(),b()) -> d()
      f(x,c()) -> f(c(),c())
      f(c(),x) -> f(c(),c())
      d() -> f(a(),c())
    Matrix Interpretation Processor: dim=3
     
     interpretation:
            [1]
      [d] = [1]
            [0],
      
                    [1 0 0]     [1 1 0]  
      [f](x0, x1) = [0 0 0]x0 + [1 1 0]x1
                    [0 0 0]     [0 0 0]  ,
      
            [1]
      [b] = [1]
            [0],
      
            [0]
      [c] = [0]
            [0],
      
            [0]
      [a] = [0]
            [0]
     orientation:
                   [2]    [1]      
      f(a(),b()) = [2] >= [1] = d()
                   [0]    [0]      
      
                   [2]    [0]             
      f(a(),b()) = [2] >= [0] = f(a(),c())
                   [0]    [0]             
      
                   [2]    [1]      
      f(a(),b()) = [2] >= [1] = d()
                   [0]    [0]      
      
            [1]    [0]             
      d() = [1] >= [0] = f(a(),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]             
      
                   [0]    [0]             
      f(c(),c()) = [0] >= [0] = f(c(),c())
                   [0]    [0]             
      
            [1]    [0]             
      d() = [1] >= [0] = f(a(),c())
            [0]    [0]             
      
                   [2]    [0]             
      f(c(),b()) = [2] >= [0] = f(c(),c())
                   [0]    [0]             
      
            [1]    [0]             
      d() = [1] >= [0] = f(a(),c())
            [0]    [0]             
      
                   [2]    [0]             
      f(c(),b()) = [2] >= [0] = f(c(),c())
                   [0]    [0]             
      
            [1]    [0]      
      b() = [1] >= [0] = c()
            [0]    [0]      
      
                 [1 0 0]     [0]             
      f(x,c()) = [0 0 0]x >= [0] = f(c(),c())
                 [0 0 0]     [0]             
      
                 [1 1 0]     [0]             
      f(c(),x) = [1 1 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