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 (critical pair closing system, Thm 2.11):
  c() -> f(a'(),b())
  c() -> f(a(),b'())
  b() -> b'()
  a() -> a'()
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [b'] = 0,
    
    [a'] = 0,
    
    [c] = 2,
    
    [f](x0, x1) = x0 + x1 + 1,
    
    [b] = 1,
    
    [a] = 1
   orientation:
    c() = 2 >= 2 = f(a'(),b())
    
    c() = 2 >= 2 = f(a(),b'())
    
    b() = 1 >= 0 = b'()
    
    a() = 1 >= 0 = a'()
   problem:
    c() -> f(a'(),b())
    c() -> f(a(),b'())
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [b'] = 0,
     
     [a'] = 0,
     
     [c] = 1,
     
     [f](x0, x1) = x0 + x1,
     
     [b] = 1,
     
     [a] = 0
    orientation:
     c() = 1 >= 1 = f(a'(),b())
     
     c() = 1 >= 0 = f(a(),b'())
    problem:
     c() -> f(a'(),b())
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [a'] = 1,
      
      [c] = 3,
      
      [f](x0, x1) = x0 + 4x1 + 1,
      
      [b] = 0
     orientation:
      c() = 3 >= 2 = f(a'(),b())
     problem:
      
     Qed