NO Problem: app(app(const(),x),y) -> x app(app(app(subst(),f),g),x) -> app(app(f,x),app(g,x)) app(app(fix(),f),x) -> app(app(f,app(fix(),f)),x) Proof: Uncurry Processor: const2(x,y) -> x subst3(f,g,x) -> app(app(f,x),app(g,x)) fix2(f,x) -> app(app(f,fix1(f)),x) app(const1(x5),x6) -> const2(x5,x6) app(const(),x6) -> const1(x6) app(subst2(x5,x4),x6) -> subst3(x5,x4,x6) app(subst1(x5),x6) -> subst2(x5,x6) app(subst(),x6) -> subst1(x6) app(fix1(x5),x6) -> fix2(x5,x6) app(fix(),x6) -> fix1(x6) Unfolding Processor: loop length: 5 terms: fix2(subst1(x85456),x86194) app(app(subst1(x85456),fix1(subst1(x85456))),x86194) app(subst2(x85456,fix1(subst1(x85456))),x86194) subst3(x85456,fix1(subst1(x85456)),x86194) app(app(x85456,x86194),app(fix1(subst1(x85456)),x86194)) context: app(app(x85456,x86194),[]) substitution: x85456 -> x85456 x86194 -> x86194 Qed