YES O(n) TRS: { c(c(b(c(y), 0()))) -> a(0(), c(c(a(y, 0())))), c(c(c(a(x, y)))) -> b(c(c(c(c(y)))), x), c(c(a(a(y, 0()), x))) -> c(y) } DUP: We consider a non-duplicating system. Trs: { c(c(b(c(y), 0()))) -> a(0(), c(c(a(y, 0())))), c(c(c(a(x, y)))) -> b(c(c(c(c(y)))), x), c(c(a(a(y, 0()), x))) -> c(y) } BOUND: Automaton: { 0_3() -> 79, 0_2() -> 25, 0_1() -> 5, 0_0() -> 4, a_3(79, 82) -> 71 | 70 | 69 | 47 | 46 | 45 | 16 | 15 | 14, a_3(46, 79) -> 80, a_2(46, 25) -> 26, a_2(39, 25) -> 26, a_2(25, 28) -> 71 | 70 | 69 | 68 | 47 | 46 | 45 | 44 | 40 | 39 | 38 | 37 | 28 | 16 | 15 | 14 | 13 | 12 | 11 | 10 | 9 | 8 | 4, a_2(15, 25) -> 26, a_2(11, 25) -> 26, a_2(4, 25) -> 26, a_1(62, 5) -> 98, a_1(58, 5) -> 95, a_1(46, 5) -> 6, a_1(39, 5) -> 6, a_1(23, 5) -> 41, a_1(15, 5) -> 6, a_1(11, 5) -> 6, a_1(5, 100) -> 70 | 46, a_1(5, 97) -> 39, a_1(5, 43) -> 15 | 11, a_1(5, 8) -> 71 | 70 | 69 | 68 | 47 | 46 | 45 | 44 | 40 | 39 | 38 | 37 | 28 | 16 | 15 | 14 | 13 | 12 | 11 | 10 | 9 | 8 | 4, a_1(4, 5) -> 6, a_0(4, 4) -> 4, c_3(81) -> 82, c_3(80) -> 81, c_3(70) -> 71, c_3(69) -> 70, c_3(68) -> 69, c_3(62) -> 63, c_3(61) -> 62, c_3(60) -> 61, c_3(28) -> 68, c_3(25) -> 60, c_2(58) -> 59, c_2(57) -> 58, c_2(56) -> 57, c_2(46) -> 47, c_2(45) -> 46, c_2(44) -> 45, c_2(28) -> 44, c_2(27) -> 28, c_2(26) -> 27, c_2(25) -> 56, c_2(23) -> 24, c_2(22) -> 23, c_2(21) -> 22, c_2(15) -> 16, c_2(14) -> 15, c_2(13) -> 14, c_2(8) -> 13, c_2(5) -> 21, c_1(99) -> 100, c_1(98) -> 99, c_1(96) -> 97, c_1(95) -> 96, c_1(42) -> 43, c_1(41) -> 42, c_1(39) -> 40, c_1(38) -> 39, c_1(37) -> 38, c_1(28) -> 37, c_1(11) -> 12, c_1(10) -> 11, c_1(9) -> 10, c_1(8) -> 9, c_1(7) -> 8, c_1(6) -> 7, c_1(4) -> 71 | 70 | 69 | 68 | 47 | 46 | 45 | 44 | 40 | 39 | 38 | 37 | 28 | 16 | 15 | 14 | 13 | 12 | 11 | 10 | 9 | 8 | 4, c_0(4) -> 4, b_3(71, 25) -> 71 | 70 | 47 | 46 | 16 | 15, b_3(63, 46) -> 68 | 44, b_3(63, 39) -> 68 | 44, b_3(63, 15) -> 68 | 44, b_3(63, 11) -> 68 | 44, b_3(63, 4) -> 68 | 44, b_2(59, 46) -> 37, b_2(59, 39) -> 37, b_2(59, 15) -> 37, b_2(59, 11) -> 37, b_2(59, 4) -> 37, b_2(47, 25) -> 71 | 70 | 69 | 68 | 47 | 46 | 45 | 44 | 40 | 39 | 38 | 37 | 28 | 16 | 15 | 14 | 13 | 12 | 11 | 10 | 9 | 8 | 4, b_2(24, 46) -> 13 | 9, b_2(24, 39) -> 13 | 9, b_2(24, 15) -> 13 | 9, b_2(24, 11) -> 13 | 9, b_2(24, 4) -> 13 | 9, b_2(16, 5) -> 71 | 70 | 69 | 68 | 47 | 46 | 45 | 44 | 40 | 39 | 38 | 37 | 28 | 16 | 15 | 14 | 13 | 12 | 11 | 10 | 9 | 8 | 4, b_1(40, 25) -> 71 | 70 | 69 | 68 | 47 | 46 | 45 | 44 | 40 | 39 | 38 | 37 | 28 | 16 | 15 | 14 | 13 | 12 | 11 | 10 | 9 | 8 | 4, b_1(12, 5) -> 71 | 70 | 69 | 68 | 47 | 46 | 45 | 44 | 40 | 39 | 38 | 37 | 28 | 16 | 15 | 14 | 13 | 12 | 11 | 10 | 9 | 8 | 4, b_1(4, 4) -> 71 | 70 | 69 | 68 | 47 | 46 | 45 | 44 | 40 | 39 | 38 | 37 | 28 | 16 | 15 | 14 | 13 | 12 | 11 | 10 | 9 | 8 | 4, b_0(4, 4) -> 4 } Strict: {} Qed