Problem:
 f(s(s(s(s(s(s(s(s(x)))))))),y,y) -> f(id(s(s(s(s(s(s(s(s(x))))))))),y,y)
 id(s(x)) -> s(id(x))
 id(0()) -> 0()

Proof:
 Unfolding Processor:
  loop length: 9
  terms:
   f(s(s(s(s(s(s(s(s(x1561)))))))),y,y)
   f(id(s(s(s(s(s(s(s(s(x1561))))))))),y,y)
   f(s(id(s(s(s(s(s(s(s(x1561))))))))),y,y)
   f(s(s(id(s(s(s(s(s(s(x1561))))))))),y,y)
   f(s(s(s(id(s(s(s(s(s(x1561))))))))),y,y)
   f(s(s(s(s(id(s(s(s(s(x1561))))))))),y,y)
   f(s(s(s(s(s(id(s(s(s(x1561))))))))),y,y)
   f(s(s(s(s(s(s(id(s(s(x1561))))))))),y,y)
   f(s(s(s(s(s(s(s(id(s(x1561))))))))),y,y)
  context: []
  substitution:
   y -> y
   x1561 -> id(x1561)
  Qed