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

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   
  weak:
   
  critical peaks: 12
  f(b(),a(),b(),b()) <-1|0[]- f(a(),a(),b(),b()) -0|[]-> f(c(),c(),c(),c())
  f(a(),b(),b(),b()) <-1|1[]- f(a(),a(),b(),b()) -0|[]-> f(c(),c(),c(),c())
  b() <-1|[]- a() -2|[]-> c()
  f(c(),a(),b(),b()) <-2|0[]- f(a(),a(),b(),b()) -0|[]-> f(c(),c(),c(),c())
  f(a(),c(),b(),b()) <-2|1[]- f(a(),a(),b(),b()) -0|[]-> f(c(),c(),c(),c())
  c() <-2|[]- a() -1|[]-> b()
  f(a(),a(),a(),b()) <-3|2[]- f(a(),a(),b(),b()) -0|[]-> f(c(),c(),c(),c())
  f(a(),a(),b(),a()) <-3|3[]- f(a(),a(),b(),b()) -0|[]-> f(c(),c(),c(),c())
  a() <-3|[]- b() -4|[]-> c()
  f(a(),a(),c(),b()) <-4|2[]- f(a(),a(),b(),b()) -0|[]-> f(c(),c(),c(),c())
  f(a(),a(),b(),c()) <-4|3[]- f(a(),a(),b(),b()) -0|[]-> f(c(),c(),c(),c())
  c() <-4|[]- b() -3|[]-> a()
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed