Problem:
 d(x,x) -> 0()
 f(x) -> d(x,f(x))
 c() -> f(c())

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 0
  Redundant Rules Transformation:
   d(x,x) -> 0()
   f(x) -> d(x,f(x))
   c() -> f(c())
   f(c()) -> d(f(c()),f(c()))
   f(c()) -> d(c(),f(f(c())))
   c() -> d(c(),f(c()))
   c() -> f(f(c()))
   d(d(x,x),0()) -> 0()
   d(0(),d(x,x)) -> 0()
   d(c(),f(c())) -> 0()
   d(f(c()),c()) -> 0()
   Nonconfluence Processor:
    terms: f(0()) *<- f(c()) ->* 0()
    Qed
    
    first automaton:
     final states: {1028}
     transitions:
      d(1029,1028) -> 1028*
      0() -> 1029*
      f(1029) -> 1028*
    
    second automaton:
     final states: {7}
     transitions:
      0() -> 7*