YES(O(1),O(n^1)) 484.60/166.28 YES(O(1),O(n^1)) 484.60/166.28 484.60/166.28 We are left with following problem, upon which TcT provides the 484.60/166.28 certificate YES(O(1),O(n^1)). 484.60/166.28 484.60/166.28 Strict Trs: 484.60/166.28 { c(c(c(a(x, y)))) -> b(c(c(c(c(y)))), x) 484.60/166.28 , c(c(a(a(y, 0()), x))) -> c(y) 484.60/166.28 , c(c(b(c(y), 0()))) -> a(0(), c(c(a(y, 0())))) } 484.60/166.28 Obligation: 484.60/166.28 derivational complexity 484.60/166.28 Answer: 484.60/166.28 YES(O(1),O(n^1)) 484.60/166.28 484.60/166.28 The weightgap principle applies (using the following nonconstant 484.60/166.28 growth matrix-interpretation) 484.60/166.28 484.60/166.28 TcT has computed the following triangular matrix interpretation. 484.60/166.28 Note that the diagonal of the component-wise maxima of 484.60/166.28 interpretation-entries contains no more than 1 non-zero entries. 484.60/166.28 484.60/166.28 [c](x1) = [1] x1 + [0] 484.60/166.28 484.60/166.28 [a](x1, x2) = [1] x1 + [1] x2 + [1] 484.60/166.28 484.60/166.28 [b](x1, x2) = [1] x1 + [1] x2 + [0] 484.60/166.28 484.60/166.28 [0] = [0] 484.60/166.28 484.60/166.28 The order satisfies the following ordering constraints: 484.60/166.28 484.60/166.28 [c(c(c(a(x, y))))] = [1] x + [1] y + [1] 484.60/166.28 > [1] x + [1] y + [0] 484.60/166.28 = [b(c(c(c(c(y)))), x)] 484.60/166.28 484.60/166.28 [c(c(a(a(y, 0()), x)))] = [1] x + [1] y + [2] 484.60/166.28 > [1] y + [0] 484.60/166.28 = [c(y)] 484.60/166.28 484.60/166.28 [c(c(b(c(y), 0())))] = [1] y + [0] 484.60/166.28 ? [1] y + [2] 484.60/166.28 = [a(0(), c(c(a(y, 0()))))] 484.60/166.28 484.60/166.28 484.60/166.28 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 484.60/166.28 484.60/166.28 We are left with following problem, upon which TcT provides the 484.60/166.28 certificate YES(?,O(n^1)). 484.60/166.28 484.60/166.28 Strict Trs: { c(c(b(c(y), 0()))) -> a(0(), c(c(a(y, 0())))) } 484.60/166.28 Weak Trs: 484.60/166.28 { c(c(c(a(x, y)))) -> b(c(c(c(c(y)))), x) 484.60/166.28 , c(c(a(a(y, 0()), x))) -> c(y) } 484.60/166.28 Obligation: 484.60/166.28 derivational complexity 484.60/166.28 Answer: 484.60/166.28 YES(?,O(n^1)) 484.60/166.28 484.60/166.28 The problem is match-bounded by 2. The enriched problem is 484.60/166.28 compatible with the following automaton. 484.60/166.28 { c_0(1) -> 1 484.60/166.28 , c_1(1) -> 3 484.60/166.28 , c_1(1) -> 7 484.60/166.28 , c_1(1) -> 8 484.60/166.28 , c_1(1) -> 9 484.60/166.28 , c_1(1) -> 10 484.60/166.28 , c_1(1) -> 11 484.60/166.28 , c_1(1) -> 12 484.60/166.28 , c_1(1) -> 13 484.60/166.28 , c_1(1) -> 14 484.60/166.28 , c_1(1) -> 18 484.60/166.28 , c_1(1) -> 22 484.60/166.28 , c_1(1) -> 23 484.60/166.28 , c_1(1) -> 24 484.60/166.28 , c_1(1) -> 25 484.60/166.28 , c_1(1) -> 30 484.60/166.28 , c_1(1) -> 31 484.60/166.28 , c_1(1) -> 32 484.60/166.28 , c_1(1) -> 33 484.60/166.28 , c_1(3) -> 14 484.60/166.28 , c_1(4) -> 3 484.60/166.28 , c_1(5) -> 4 484.60/166.28 , c_1(8) -> 7 484.60/166.28 , c_1(9) -> 8 484.60/166.28 , c_1(10) -> 9 484.60/166.28 , c_1(12) -> 11 484.60/166.28 , c_1(13) -> 12 484.60/166.28 , c_1(14) -> 13 484.60/166.28 , c_1(44) -> 43 484.60/166.28 , c_1(45) -> 44 484.60/166.28 , c_2(3) -> 25 484.60/166.28 , c_2(6) -> 29 484.60/166.28 , c_2(18) -> 33 484.60/166.28 , c_2(19) -> 18 484.60/166.28 , c_2(20) -> 19 484.60/166.28 , c_2(21) -> 42 484.60/166.28 , c_2(23) -> 22 484.60/166.28 , c_2(24) -> 23 484.60/166.28 , c_2(25) -> 24 484.60/166.28 , c_2(27) -> 26 484.60/166.28 , c_2(28) -> 27 484.60/166.28 , c_2(29) -> 28 484.60/166.28 , c_2(31) -> 30 484.60/166.28 , c_2(32) -> 31 484.60/166.28 , c_2(33) -> 32 484.60/166.28 , c_2(37) -> 36 484.60/166.28 , c_2(38) -> 37 484.60/166.28 , c_2(40) -> 39 484.60/166.28 , c_2(41) -> 40 484.60/166.28 , c_2(42) -> 41 484.60/166.28 , a_0(1, 1) -> 1 484.60/166.28 , a_1(1, 6) -> 5 484.60/166.28 , a_1(2, 3) -> 1 484.60/166.28 , a_1(6, 3) -> 3 484.60/166.28 , a_1(6, 3) -> 7 484.60/166.28 , a_1(6, 3) -> 8 484.60/166.28 , a_1(6, 3) -> 9 484.60/166.28 , a_1(6, 3) -> 10 484.60/166.28 , a_1(6, 3) -> 11 484.60/166.28 , a_1(6, 3) -> 12 484.60/166.28 , a_1(6, 3) -> 13 484.60/166.28 , a_1(6, 3) -> 14 484.60/166.28 , a_1(6, 3) -> 18 484.60/166.28 , a_1(6, 3) -> 22 484.60/166.28 , a_1(6, 3) -> 23 484.60/166.28 , a_1(6, 3) -> 24 484.60/166.28 , a_1(6, 3) -> 25 484.60/166.28 , a_1(6, 3) -> 30 484.60/166.28 , a_1(6, 3) -> 31 484.60/166.28 , a_1(6, 3) -> 32 484.60/166.28 , a_1(6, 3) -> 33 484.60/166.28 , a_1(6, 43) -> 31 484.60/166.28 , a_1(8, 6) -> 5 484.60/166.28 , a_1(12, 6) -> 5 484.60/166.28 , a_1(13, 6) -> 5 484.60/166.28 , a_1(27, 6) -> 5 484.60/166.28 , a_1(40, 6) -> 45 484.60/166.28 , a_2(1, 21) -> 20 484.60/166.28 , a_2(12, 21) -> 20 484.60/166.28 , a_2(17, 18) -> 8 484.60/166.28 , a_2(21, 18) -> 7 484.60/166.28 , a_2(21, 18) -> 9 484.60/166.28 , a_2(21, 18) -> 11 484.60/166.28 , a_2(21, 18) -> 12 484.60/166.28 , a_2(21, 18) -> 13 484.60/166.28 , a_2(21, 18) -> 14 484.60/166.28 , a_2(21, 18) -> 22 484.60/166.28 , a_2(21, 18) -> 23 484.60/166.28 , a_2(21, 18) -> 24 484.60/166.28 , a_2(21, 18) -> 25 484.60/166.28 , a_2(21, 18) -> 30 484.60/166.28 , a_2(21, 18) -> 31 484.60/166.28 , a_2(21, 18) -> 32 484.60/166.28 , a_2(21, 18) -> 33 484.60/166.28 , a_2(21, 36) -> 11 484.60/166.28 , a_2(21, 36) -> 22 484.60/166.28 , a_2(21, 36) -> 30 484.60/166.28 , a_2(23, 21) -> 38 484.60/166.28 , b_0(1, 1) -> 1 484.60/166.28 , b_1(7, 1) -> 1 484.60/166.28 , b_1(11, 2) -> 1 484.60/166.28 , b_1(11, 2) -> 3 484.60/166.28 , b_1(11, 2) -> 7 484.60/166.28 , b_1(11, 2) -> 8 484.60/166.28 , b_1(11, 2) -> 9 484.60/166.28 , b_1(11, 2) -> 10 484.60/166.28 , b_1(11, 2) -> 11 484.60/166.28 , b_1(11, 2) -> 12 484.60/166.28 , b_1(11, 2) -> 13 484.60/166.28 , b_1(11, 2) -> 14 484.60/166.28 , b_1(11, 2) -> 18 484.60/166.28 , b_1(11, 2) -> 22 484.60/166.28 , b_1(11, 2) -> 23 484.60/166.28 , b_1(11, 2) -> 24 484.60/166.28 , b_1(11, 2) -> 25 484.60/166.28 , b_1(11, 2) -> 30 484.60/166.28 , b_1(11, 2) -> 31 484.60/166.28 , b_1(11, 2) -> 32 484.60/166.28 , b_1(11, 2) -> 33 484.60/166.28 , b_1(12, 1) -> 3 484.60/166.28 , b_1(12, 1) -> 7 484.60/166.28 , b_1(12, 1) -> 8 484.60/166.28 , b_1(12, 1) -> 9 484.60/166.28 , b_1(12, 1) -> 10 484.60/166.28 , b_1(12, 1) -> 11 484.60/166.28 , b_1(12, 1) -> 12 484.60/166.28 , b_1(12, 1) -> 13 484.60/166.28 , b_1(12, 1) -> 14 484.60/166.28 , b_1(12, 1) -> 18 484.60/166.28 , b_1(12, 1) -> 22 484.60/166.28 , b_1(12, 1) -> 23 484.60/166.28 , b_1(12, 1) -> 24 484.60/166.28 , b_1(12, 1) -> 25 484.60/166.28 , b_1(12, 1) -> 30 484.60/166.28 , b_1(12, 1) -> 31 484.60/166.28 , b_1(12, 1) -> 32 484.60/166.28 , b_1(12, 1) -> 33 484.60/166.28 , b_2(22, 2) -> 7 484.60/166.28 , b_2(22, 2) -> 8 484.60/166.28 , b_2(22, 2) -> 11 484.60/166.28 , b_2(22, 2) -> 12 484.60/166.28 , b_2(22, 2) -> 13 484.60/166.28 , b_2(22, 2) -> 22 484.60/166.28 , b_2(22, 2) -> 23 484.60/166.28 , b_2(22, 2) -> 24 484.60/166.28 , b_2(22, 2) -> 30 484.60/166.28 , b_2(22, 2) -> 31 484.60/166.28 , b_2(22, 2) -> 32 484.60/166.28 , b_2(22, 6) -> 7 484.60/166.28 , b_2(22, 6) -> 11 484.60/166.28 , b_2(22, 6) -> 12 484.60/166.28 , b_2(22, 6) -> 22 484.60/166.28 , b_2(22, 6) -> 23 484.60/166.28 , b_2(22, 6) -> 30 484.60/166.28 , b_2(22, 6) -> 31 484.60/166.28 , b_2(26, 1) -> 14 484.60/166.28 , b_2(26, 1) -> 25 484.60/166.28 , b_2(26, 8) -> 14 484.60/166.28 , b_2(26, 8) -> 25 484.60/166.28 , b_2(26, 12) -> 14 484.60/166.28 , b_2(26, 12) -> 25 484.60/166.28 , b_2(26, 13) -> 14 484.60/166.28 , b_2(26, 13) -> 25 484.60/166.28 , b_2(26, 27) -> 14 484.60/166.28 , b_2(26, 27) -> 25 484.60/166.28 , b_2(30, 21) -> 11 484.60/166.28 , b_2(30, 21) -> 22 484.60/166.28 , b_2(30, 21) -> 30 484.60/166.28 , b_2(39, 1) -> 33 484.60/166.28 , b_2(39, 12) -> 33 484.60/166.28 , 0_0() -> 1 484.60/166.28 , 0_1() -> 2 484.60/166.28 , 0_1() -> 6 484.60/166.28 , 0_2() -> 17 484.60/166.28 , 0_2() -> 21 } 484.60/166.28 484.60/166.28 Hurray, we answered YES(O(1),O(n^1)) 484.85/166.38 EOF