MAYBE Problem: ap(ap(g(),x),y) -> y ap(f(),x) -> ap(f(),app(g(),x)) Proof: DP Processor: DPs: ap#(f(),x) -> ap#(f(),app(g(),x)) TRS: ap(ap(g(),x),y) -> y ap(f(),x) -> ap(f(),app(g(),x)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/1 DPs: ap#(f(),x) -> ap#(f(),app(g(),x)) TRS: ap(ap(g(),x),y) -> y ap(f(),x) -> ap(f(),app(g(),x)) Open