YES Problem: app(app(F(),app(app(F(),f),x)),x) -> app(app(F(),app(G(),app(app(F(),f),x))),app(f,x)) Proof: DP Processor: DPs: app#(app(F(),app(app(F(),f),x)),x) -> app#(f,x) app#(app(F(),app(app(F(),f),x)),x) -> app#(G(),app(app(F(),f),x)) app#(app(F(),app(app(F(),f),x)),x) -> app#(F(),app(G(),app(app(F(),f),x))) app#(app(F(),app(app(F(),f),x)),x) -> app#(app(F(),app(G(),app(app(F(),f),x))),app(f,x)) TRS: app(app(F(),app(app(F(),f),x)),x) -> app(app(F(),app(G(),app(app(F(),f),x))),app(f,x)) EDG Processor: DPs: app#(app(F(),app(app(F(),f),x)),x) -> app#(f,x) app#(app(F(),app(app(F(),f),x)),x) -> app#(G(),app(app(F(),f),x)) app#(app(F(),app(app(F(),f),x)),x) -> app#(F(),app(G(),app(app(F(),f),x))) app#(app(F(),app(app(F(),f),x)),x) -> app#(app(F(),app(G(),app(app(F(),f),x))),app(f,x)) TRS: app(app(F(),app(app(F(),f),x)),x) -> app(app(F(),app(G(),app(app(F(),f),x))),app(f,x)) graph: app#(app(F(),app(app(F(),f),x)),x) -> app#(f,x) -> app#(app(F(),app(app(F(),f),x)),x) -> app#(f,x) app#(app(F(),app(app(F(),f),x)),x) -> app#(f,x) -> app#(app(F(),app(app(F(),f),x)),x) -> app#(G(),app(app(F(),f),x)) app#(app(F(),app(app(F(),f),x)),x) -> app#(f,x) -> app#(app(F(),app(app(F(),f),x)),x) -> app#(F(),app(G(),app(app(F(),f),x))) app#(app(F(),app(app(F(),f),x)),x) -> app#(f,x) -> app#(app(F(),app(app(F(),f),x)),x) -> app#(app(F(),app(G(),app(app(F(),f),x))),app(f,x)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 4/16 DPs: app#(app(F(),app(app(F(),f),x)),x) -> app#(f,x) TRS: app(app(F(),app(app(F(),f),x)),x) -> app(app(F(),app(G(),app(app(F(),f),x))),app(f,x)) Subterm Criterion Processor: simple projection: pi(app#) = 0 problem: DPs: TRS: app(app(F(),app(app(F(),f),x)),x) -> app(app(F(),app(G(),app(app(F(),f),x))),app(f,x)) Qed