YES(?,O(n^1)) 919.84/297.02 YES(?,O(n^1)) 919.84/297.02 919.84/297.02 We are left with following problem, upon which TcT provides the 919.84/297.02 certificate YES(?,O(n^1)). 919.84/297.02 919.84/297.02 Strict Trs: 919.84/297.02 { 0(x1) -> 1(x1) 919.84/297.02 , 4(5(4(5(x1)))) -> 4(4(5(5(x1)))) 919.84/297.02 , 5(5(5(5(5(5(4(4(4(4(4(4(x1)))))))))))) -> 2(x1) } 919.84/297.02 Obligation: 919.84/297.02 derivational complexity 919.84/297.02 Answer: 919.84/297.02 YES(?,O(n^1)) 919.84/297.02 919.84/297.02 The problem is match-bounded by 1. The enriched problem is 919.84/297.02 compatible with the following automaton. 919.84/297.02 { 0_0(1) -> 1 919.84/297.02 , 1_0(1) -> 1 919.84/297.02 , 1_1(1) -> 1 919.84/297.02 , 4_0(1) -> 1 919.84/297.02 , 4_1(2) -> 1 919.84/297.02 , 4_1(3) -> 2 919.84/297.02 , 5_0(1) -> 1 919.84/297.02 , 5_1(1) -> 4 919.84/297.02 , 5_1(4) -> 3 919.84/297.02 , 2_0(1) -> 1 919.84/297.02 , 2_1(1) -> 1 919.84/297.02 , 2_1(1) -> 3 919.84/297.02 , 2_1(1) -> 4 919.84/297.02 , 2_1(2) -> 1 919.84/297.02 , 2_1(2) -> 3 919.84/297.02 , 2_1(2) -> 4 919.84/297.02 , 2_1(3) -> 1 919.84/297.02 , 2_1(3) -> 3 919.84/297.02 , 2_1(3) -> 4 } 919.84/297.02 919.84/297.02 Hurray, we answered YES(?,O(n^1)) 920.16/297.38 EOF