YES Problem: a(f(),a(f(),x)) -> a(x,g()) a(x,g()) -> a(f(),a(g(),a(f(),x))) Proof: DP Processor: DPs: a#(f(),a(f(),x)) -> a#(x,g()) a#(x,g()) -> a#(f(),x) a#(x,g()) -> a#(g(),a(f(),x)) a#(x,g()) -> a#(f(),a(g(),a(f(),x))) TRS: a(f(),a(f(),x)) -> a(x,g()) a(x,g()) -> a(f(),a(g(),a(f(),x))) EDG Processor: DPs: a#(f(),a(f(),x)) -> a#(x,g()) a#(x,g()) -> a#(f(),x) a#(x,g()) -> a#(g(),a(f(),x)) a#(x,g()) -> a#(f(),a(g(),a(f(),x))) TRS: a(f(),a(f(),x)) -> a(x,g()) a(x,g()) -> a(f(),a(g(),a(f(),x))) graph: a#(f(),a(f(),x)) -> a#(x,g()) -> a#(x,g()) -> a#(f(),x) a#(f(),a(f(),x)) -> a#(x,g()) -> a#(x,g()) -> a#(g(),a(f(),x)) a#(f(),a(f(),x)) -> a#(x,g()) -> a#(x,g()) -> a#(f(),a(g(),a(f(),x))) a#(x,g()) -> a#(f(),a(g(),a(f(),x))) -> a#(f(),a(f(),x)) -> a#(x,g()) a#(x,g()) -> a#(f(),x) -> a#(f(),a(f(),x)) -> a#(x,g()) a#(x,g()) -> a#(f(),x) -> a#(x,g()) -> a#(f(),x) a#(x,g()) -> a#(f(),x) -> a#(x,g()) -> a#(g(),a(f(),x)) a#(x,g()) -> a#(f(),x) -> a#(x,g()) -> a#(f(),a(g(),a(f(),x))) CDG Processor: DPs: a#(f(),a(f(),x)) -> a#(x,g()) a#(x,g()) -> a#(f(),x) a#(x,g()) -> a#(g(),a(f(),x)) a#(x,g()) -> a#(f(),a(g(),a(f(),x))) TRS: a(f(),a(f(),x)) -> a(x,g()) a(x,g()) -> a(f(),a(g(),a(f(),x))) graph: a#(f(),a(f(),x)) -> a#(x,g()) -> a#(x,g()) -> a#(f(),a(g(),a(f(),x))) a#(f(),a(f(),x)) -> a#(x,g()) -> a#(x,g()) -> a#(g(),a(f(),x)) a#(f(),a(f(),x)) -> a#(x,g()) -> a#(x,g()) -> a#(f(),x) a#(x,g()) -> a#(f(),x) -> a#(x,g()) -> a#(f(),a(g(),a(f(),x))) a#(x,g()) -> a#(f(),x) -> a#(x,g()) -> a#(g(),a(f(),x)) a#(x,g()) -> a#(f(),x) -> a#(x,g()) -> a#(f(),x) SCC Processor: #sccs: 1 #rules: 1 #arcs: 6/16 DPs: a#(x,g()) -> a#(f(),x) TRS: a(f(),a(f(),x)) -> a(x,g()) a(x,g()) -> a(f(),a(g(),a(f(),x))) Matrix Interpretation Processor: dim=1 interpretation: [a#](x0, x1) = x0 + x1 + 7, [g] = 4, [a](x0, x1) = 0, [f] = 1 orientation: a#(x,g()) = x + 11 >= x + 8 = a#(f(),x) a(f(),a(f(),x)) = 0 >= 0 = a(x,g()) a(x,g()) = 0 >= 0 = a(f(),a(g(),a(f(),x))) problem: DPs: TRS: a(f(),a(f(),x)) -> a(x,g()) a(x,g()) -> a(f(),a(g(),a(f(),x))) Qed