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

Proof:
 Uncurry Processor:
  a1(X) -> f(X,X)
  c() -> a()
  c() -> b()
  f(a(),x1) -> a1(x1)
  Unfolding Processor:
   loop length: 2
   terms:
    f(a(),a())
    a1(a())
   context: []
   substitution:
    
   Qed