YES Problem: g(x,a(),b()) -> g(b(),b(),a()) Proof: DP Processor: DPs: g#(x,a(),b()) -> g#(b(),b(),a()) TRS: g(x,a(),b()) -> g(b(),b(),a()) Usable Rule Processor: DPs: g#(x,a(),b()) -> g#(b(),b(),a()) TRS: Restore Modifier: DPs: g#(x,a(),b()) -> g#(b(),b(),a()) TRS: g(x,a(),b()) -> g(b(),b(),a()) SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/1 DPs: g#(x,a(),b()) -> g#(b(),b(),a()) TRS: g(x,a(),b()) -> g(b(),b(),a()) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0, x1, x2) = x1, [g](x0, x1, x2) = 0, [b] = 0, [a] = 1 orientation: g#(x,a(),b()) = 1 >= 0 = g#(b(),b(),a()) g(x,a(),b()) = 0 >= 0 = g(b(),b(),a()) problem: DPs: TRS: g(x,a(),b()) -> g(b(),b(),a()) Qed