NO 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