YES We show the termination of the TRS R: w(r(x)) -> r(w(x)) b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: w#(r(x)) -> w#(x) p2: b#(r(x)) -> b#(x) p3: b#(w(x)) -> w#(b(x)) p4: b#(w(x)) -> b#(x) and R consists of: r1: w(r(x)) -> r(w(x)) r2: b(r(x)) -> r(b(x)) r3: b(w(x)) -> w(b(x)) The estimated dependency graph contains the following SCCs: {p2, p4} {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: b#(w(x)) -> b#(x) p2: b#(r(x)) -> b#(x) and R consists of: r1: w(r(x)) -> r(w(x)) r2: b(r(x)) -> r(b(x)) r3: b(w(x)) -> w(b(x)) The set of usable rules consists of r1, r2, r3 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: model-based reduction triple (=A, >=A!, >A!): finite algebra: carrier: {0,1} interpretations: b#_A(0) = 0 b#_A(1) = 0 w_A(0) = 0 w_A(1) = 1 r_A(0) = 0 r_A(1) = 1 b_A(0) = 0 b_A(1) = 0 b#!_A(0) = 0 b#!_A(1) = 0 w!_A(0) = 0 w!_A(1) = 1 r!_A(0) = 0 r!_A(1) = 1 b!_A(0) = 1 b!_A(1) = 1 partial status: pi(b#) = [1] pi(w) = [1] pi(r) = [1] pi(b) = [1] The following rules are removed: p1, p2 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: w#(r(x)) -> w#(x) and R consists of: r1: w(r(x)) -> r(w(x)) r2: b(r(x)) -> r(b(x)) r3: b(w(x)) -> w(b(x)) The set of usable rules consists of r1, r2, r3 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: model-based reduction triple (=A, >=A!, >A!): finite algebra: carrier: {0,1} interpretations: w#_A(0) = 0 w#_A(1) = 0 r_A(0) = 0 r_A(1) = 0 w_A(0) = 0 w_A(1) = 0 b_A(0) = 0 b_A(1) = 1 w#!_A(0) = 0 w#!_A(1) = 0 r!_A(0) = 0 r!_A(1) = 0 w!_A(0) = 0 w!_A(1) = 0 b!_A(0) = 0 b!_A(1) = 0 partial status: pi(w#) = [1] pi(r) = [1] pi(w) = [1] pi(b) = [1] The following rules are removed: p1 Then no dependency pair remains.