YES O(n) TRS: { a(X) -> e(), b(X) -> e(), c(X) -> e(), c(b(a(X))) -> a(a(b(b(c(c(X)))))) } DUP: We consider a non-duplicating system. Trs: { a(X) -> e(), b(X) -> e(), c(X) -> e(), c(b(a(X))) -> a(a(b(b(c(c(X)))))) } BOUND: Automaton: { e_2() -> 21, e_1() -> 5, e_0() -> 4, c_1(26) -> 27, c_1(8) -> 9, c_1(7) -> 8, c_0(4) -> 4, b_1(10) -> 11, b_1(9) -> 10, b_0(4) -> 4, a_1(12) -> 13, a_1(11) -> 12, a_0(4) -> 4, 27 -> 8, 21 -> 27 | 13 | 12 | 11 | 10 | 9, 13 -> 8 | 4, 12 -> 26, 5 -> 4, 4 -> 7 } Strict: {} Qed