Problem:
 f(a(),b()) -> c()
 a() -> a'()
 b() -> b'()
 c() -> f(a'(),b())
 c() -> f(a(),b'())
 c() -> f(a(),b())

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