YES Problem: .(.(x,y),z) -> .(x,.(y,z)) Proof: DP Processor: DPs: .#(.(x,y),z) -> .#(y,z) .#(.(x,y),z) -> .#(x,.(y,z)) TRS: .(.(x,y),z) -> .(x,.(y,z)) Restore Modifier: DPs: .#(.(x,y),z) -> .#(y,z) .#(.(x,y),z) -> .#(x,.(y,z)) TRS: .(.(x,y),z) -> .(x,.(y,z)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 DPs: .#(.(x,y),z) -> .#(y,z) .#(.(x,y),z) -> .#(x,.(y,z)) TRS: .(.(x,y),z) -> .(x,.(y,z)) Matrix Interpretation Processor: dimension: 1 interpretation: [.#](x0, x1) = x0 + x1, [.](x0, x1) = x0 + x1 + 1 orientation: .#(.(x,y),z) = x + y + z + 1 >= y + z = .#(y,z) .#(.(x,y),z) = x + y + z + 1 >= x + y + z + 1 = .#(x,.(y,z)) .(.(x,y),z) = x + y + z + 2 >= x + y + z + 2 = .(x,.(y,z)) problem: DPs: .#(.(x,y),z) -> .#(x,.(y,z)) TRS: .(.(x,y),z) -> .(x,.(y,z)) Matrix Interpretation Processor: dimension: 1 interpretation: [.#](x0, x1) = x0, [.](x0, x1) = x0 + 1 orientation: .#(.(x,y),z) = x + 1 >= x = .#(x,.(y,z)) .(.(x,y),z) = x + 2 >= x + 1 = .(x,.(y,z)) problem: DPs: TRS: .(.(x,y),z) -> .(x,.(y,z)) Qed