Problem: f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) cons(x,y) -> x cons(x,y) -> y Proof: Unfolding Processor: loop length: 4 terms: g(f(s(cons(s(a()),s(b()))),s(cons(s(a()),s(b()))),s(cons(s(a()),s(b()))))) g(f(s(cons(s(a()),s(b()))),s(s(b())),s(cons(s(a()),s(b()))))) g(f(s(s(a())),s(s(b())),s(cons(s(a()),s(b()))))) g(f(s(a()),s(b()),s(cons(s(a()),s(b()))))) context: [] substitution: Qed