YES We show the termination of the TRS R: .(.(x,y),z) -> .(x,.(y,z)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: .#(.(x,y),z) -> .#(x,.(y,z)) p2: .#(.(x,y),z) -> .#(y,z) and R consists of: r1: .(.(x,y),z) -> .(x,.(y,z)) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: .#(.(x,y),z) -> .#(x,.(y,z)) p2: .#(.(x,y),z) -> .#(y,z) and R consists of: r1: .(.(x,y),z) -> .(x,.(y,z)) The set of usable rules consists of r1 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: .#_A(x1,x2) = x1 + x2 + 2 ._A(x1,x2) = x1 + x2 + 1 base order 2: precedence: .# = . partial status: pi(.#) = [1] pi(.) = [1] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: .#(.(x,y),z) -> .#(y,z) and R consists of: r1: .(.(x,y),z) -> .(x,.(y,z)) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: .#(.(x,y),z) -> .#(y,z) and R consists of: r1: .(.(x,y),z) -> .(x,.(y,z)) The set of usable rules consists of (no rules) Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: .#_A(x1,x2) = x1 ._A(x1,x2) = x1 + x2 + 1 base order 2: precedence: . > .# partial status: pi(.#) = [] pi(.) = [1, 2] The following rules are removed: p1 Then no dependency pair remains.