NO Problem: ap(f(),x) -> x ap(ap(ap(g(),x),y),ap(s(),z)) -> ap(ap(ap(g(),x),y),ap(ap(x,y),0())) Proof: Uncurry Processor: f1(x) -> x g3(x,y,s1(z)) -> g3(x,y,ap(ap(x,y),0())) ap(f(),x5) -> f1(x5) ap(g2(x4,x3),x5) -> g3(x4,x3,x5) ap(g1(x4),x5) -> g2(x4,x5) ap(g(),x5) -> g1(x5) ap(s(),x5) -> s1(x5) Unfolding Processor: loop length: 4 terms: g3(f(),s(),s1(z)) g3(f(),s(),ap(ap(f(),s()),0())) g3(f(),s(),ap(f1(s()),0())) g3(f(),s(),ap(s(),0())) context: [] substitution: z -> 0() Qed