Problem:
 f(s(x)) -> f(g(x,x))
 g(0(),1()) -> s(0())
 0() -> 1()

Proof:
 Unfolding Processor:
  loop length: 3
  terms:
   f(g(0(),0()))
   f(g(0(),1()))
   f(s(0()))
  context: []
  substitution:
   
  Qed