YES(?,O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { revconsapp(C(x1, x2), r) -> revconsapp(x2, C(x1, r)) , revconsapp(V(n), r) -> r , revconsapp(N(), r) -> r , deeprevapp(C(x1, x2), rest) -> deeprevapp(x2, C(x1, rest)) , deeprevapp(V(n), rest) -> revconsapp(rest, V(n)) , deeprevapp(N(), rest) -> rest , deeprev(C(x1, x2)) -> deeprevapp(C(x1, x2), N()) , deeprev(V(n)) -> V(n) , deeprev(N()) -> N() , second(C(x1, x2)) -> x2 , second(V(n)) -> N() , isVal(C(x1, x2)) -> False() , isVal(V(n)) -> True() , isVal(N()) -> False() , isNotEmptyT(C(x1, x2)) -> True() , isNotEmptyT(V(n)) -> False() , isNotEmptyT(N()) -> False() , isEmptyT(C(x1, x2)) -> False() , isEmptyT(V(n)) -> False() , isEmptyT(N()) -> True() , first(C(x1, x2)) -> x1 , first(V(n)) -> N() , goal(x) -> deeprev(x) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) The problem is match-bounded by 3. The enriched problem is compatible with the following automaton. { revconsapp_0(2, 2) -> 1 , revconsapp_0(2, 4) -> 1 , revconsapp_0(2, 5) -> 1 , revconsapp_0(2, 9) -> 1 , revconsapp_0(2, 10) -> 1 , revconsapp_0(4, 2) -> 1 , revconsapp_0(4, 4) -> 1 , revconsapp_0(4, 5) -> 1 , revconsapp_0(4, 9) -> 1 , revconsapp_0(4, 10) -> 1 , revconsapp_0(5, 2) -> 1 , revconsapp_0(5, 4) -> 1 , revconsapp_0(5, 5) -> 1 , revconsapp_0(5, 9) -> 1 , revconsapp_0(5, 10) -> 1 , revconsapp_0(9, 2) -> 1 , revconsapp_0(9, 4) -> 1 , revconsapp_0(9, 5) -> 1 , revconsapp_0(9, 9) -> 1 , revconsapp_0(9, 10) -> 1 , revconsapp_0(10, 2) -> 1 , revconsapp_0(10, 4) -> 1 , revconsapp_0(10, 5) -> 1 , revconsapp_0(10, 9) -> 1 , revconsapp_0(10, 10) -> 1 , revconsapp_1(2, 15) -> 1 , revconsapp_1(2, 16) -> 3 , revconsapp_1(4, 15) -> 1 , revconsapp_1(4, 16) -> 3 , revconsapp_1(5, 15) -> 1 , revconsapp_1(5, 16) -> 3 , revconsapp_1(9, 15) -> 1 , revconsapp_1(9, 16) -> 3 , revconsapp_1(10, 15) -> 1 , revconsapp_1(10, 16) -> 3 , revconsapp_1(15, 16) -> 3 , revconsapp_1(19, 16) -> 6 , revconsapp_1(19, 16) -> 14 , revconsapp_1(20, 16) -> 6 , revconsapp_1(20, 16) -> 14 , revconsapp_2(2, 18) -> 3 , revconsapp_2(4, 18) -> 3 , revconsapp_2(5, 18) -> 3 , revconsapp_2(9, 18) -> 3 , revconsapp_2(10, 18) -> 3 , revconsapp_2(15, 18) -> 3 , revconsapp_2(17, 18) -> 6 , revconsapp_2(17, 18) -> 14 , revconsapp_2(19, 18) -> 6 , revconsapp_2(19, 18) -> 14 , revconsapp_2(20, 18) -> 6 , revconsapp_2(20, 18) -> 14 , revconsapp_3(17, 21) -> 6 , revconsapp_3(17, 21) -> 14 , revconsapp_3(19, 21) -> 6 , revconsapp_3(19, 21) -> 14 , C_0(2, 2) -> 1 , C_0(2, 2) -> 2 , C_0(2, 2) -> 3 , C_0(2, 2) -> 7 , C_0(2, 2) -> 13 , C_0(2, 4) -> 1 , C_0(2, 4) -> 2 , C_0(2, 4) -> 3 , C_0(2, 4) -> 7 , C_0(2, 4) -> 13 , C_0(2, 5) -> 1 , C_0(2, 5) -> 2 , C_0(2, 5) -> 3 , C_0(2, 5) -> 7 , C_0(2, 5) -> 13 , C_0(2, 9) -> 1 , C_0(2, 9) -> 2 , C_0(2, 9) -> 3 , C_0(2, 9) -> 7 , C_0(2, 9) -> 13 , C_0(2, 10) -> 1 , C_0(2, 10) -> 2 , C_0(2, 10) -> 3 , C_0(2, 10) -> 7 , C_0(2, 10) -> 13 , C_0(4, 2) -> 1 , C_0(4, 2) -> 2 , C_0(4, 2) -> 3 , C_0(4, 2) -> 7 , C_0(4, 2) -> 13 , C_0(4, 4) -> 1 , C_0(4, 4) -> 2 , C_0(4, 4) -> 3 , C_0(4, 4) -> 7 , C_0(4, 4) -> 13 , C_0(4, 5) -> 1 , C_0(4, 5) -> 2 , C_0(4, 5) -> 3 , C_0(4, 5) -> 7 , C_0(4, 5) -> 13 , C_0(4, 9) -> 1 , C_0(4, 9) -> 2 , C_0(4, 9) -> 3 , C_0(4, 9) -> 7 , C_0(4, 9) -> 13 , C_0(4, 10) -> 1 , C_0(4, 10) -> 2 , C_0(4, 10) -> 3 , C_0(4, 10) -> 7 , C_0(4, 10) -> 13 , C_0(5, 2) -> 1 , C_0(5, 2) -> 2 , C_0(5, 2) -> 3 , C_0(5, 2) -> 7 , C_0(5, 2) -> 13 , C_0(5, 4) -> 1 , C_0(5, 4) -> 2 , C_0(5, 4) -> 3 , C_0(5, 4) -> 7 , C_0(5, 4) -> 13 , C_0(5, 5) -> 1 , C_0(5, 5) -> 2 , C_0(5, 5) -> 3 , C_0(5, 5) -> 7 , C_0(5, 5) -> 13 , C_0(5, 9) -> 1 , C_0(5, 9) -> 2 , C_0(5, 9) -> 3 , C_0(5, 9) -> 7 , C_0(5, 9) -> 13 , C_0(5, 10) -> 1 , C_0(5, 10) -> 2 , C_0(5, 10) -> 3 , C_0(5, 10) -> 7 , C_0(5, 10) -> 13 , C_0(9, 2) -> 1 , C_0(9, 2) -> 2 , C_0(9, 2) -> 3 , C_0(9, 2) -> 7 , C_0(9, 2) -> 13 , C_0(9, 4) -> 1 , C_0(9, 4) -> 2 , C_0(9, 4) -> 3 , C_0(9, 4) -> 7 , C_0(9, 4) -> 13 , C_0(9, 5) -> 1 , C_0(9, 5) -> 2 , C_0(9, 5) -> 3 , C_0(9, 5) -> 7 , C_0(9, 5) -> 13 , C_0(9, 9) -> 1 , C_0(9, 9) -> 2 , C_0(9, 9) -> 3 , C_0(9, 9) -> 7 , C_0(9, 9) -> 13 , C_0(9, 10) -> 1 , C_0(9, 10) -> 2 , C_0(9, 10) -> 3 , C_0(9, 10) -> 7 , C_0(9, 10) -> 13 , C_0(10, 2) -> 1 , C_0(10, 2) -> 2 , C_0(10, 2) -> 3 , C_0(10, 2) -> 7 , C_0(10, 2) -> 13 , C_0(10, 4) -> 1 , C_0(10, 4) -> 2 , C_0(10, 4) -> 3 , C_0(10, 4) -> 7 , C_0(10, 4) -> 13 , C_0(10, 5) -> 1 , C_0(10, 5) -> 2 , C_0(10, 5) -> 3 , C_0(10, 5) -> 7 , C_0(10, 5) -> 13 , C_0(10, 9) -> 1 , C_0(10, 9) -> 2 , C_0(10, 9) -> 3 , C_0(10, 9) -> 7 , C_0(10, 9) -> 13 , C_0(10, 10) -> 1 , C_0(10, 10) -> 2 , C_0(10, 10) -> 3 , C_0(10, 10) -> 7 , C_0(10, 10) -> 13 , C_1(2, 2) -> 1 , C_1(2, 2) -> 3 , C_1(2, 2) -> 15 , C_1(2, 4) -> 1 , C_1(2, 4) -> 3 , C_1(2, 4) -> 15 , C_1(2, 5) -> 1 , C_1(2, 5) -> 3 , C_1(2, 5) -> 15 , C_1(2, 9) -> 1 , C_1(2, 9) -> 3 , C_1(2, 9) -> 15 , C_1(2, 10) -> 1 , C_1(2, 10) -> 3 , C_1(2, 10) -> 15 , C_1(2, 15) -> 1 , C_1(2, 15) -> 3 , C_1(2, 15) -> 15 , C_1(2, 16) -> 3 , C_1(2, 16) -> 16 , C_1(2, 18) -> 3 , C_1(2, 18) -> 16 , C_1(2, 19) -> 6 , C_1(2, 19) -> 14 , C_1(2, 19) -> 20 , C_1(2, 20) -> 6 , C_1(2, 20) -> 14 , C_1(2, 20) -> 20 , C_1(4, 2) -> 1 , C_1(4, 2) -> 3 , C_1(4, 2) -> 15 , C_1(4, 4) -> 1 , C_1(4, 4) -> 3 , C_1(4, 4) -> 15 , C_1(4, 5) -> 1 , C_1(4, 5) -> 3 , C_1(4, 5) -> 15 , C_1(4, 9) -> 1 , C_1(4, 9) -> 3 , C_1(4, 9) -> 15 , C_1(4, 10) -> 1 , C_1(4, 10) -> 3 , C_1(4, 10) -> 15 , C_1(4, 15) -> 1 , C_1(4, 15) -> 3 , C_1(4, 15) -> 15 , C_1(4, 16) -> 3 , C_1(4, 16) -> 16 , C_1(4, 18) -> 3 , C_1(4, 18) -> 16 , C_1(4, 19) -> 6 , C_1(4, 19) -> 14 , C_1(4, 19) -> 20 , C_1(4, 20) -> 6 , C_1(4, 20) -> 14 , C_1(4, 20) -> 20 , C_1(5, 2) -> 1 , C_1(5, 2) -> 3 , C_1(5, 2) -> 15 , C_1(5, 4) -> 1 , C_1(5, 4) -> 3 , C_1(5, 4) -> 15 , C_1(5, 5) -> 1 , C_1(5, 5) -> 3 , C_1(5, 5) -> 15 , C_1(5, 9) -> 1 , C_1(5, 9) -> 3 , C_1(5, 9) -> 15 , C_1(5, 10) -> 1 , C_1(5, 10) -> 3 , C_1(5, 10) -> 15 , C_1(5, 15) -> 1 , C_1(5, 15) -> 3 , C_1(5, 15) -> 15 , C_1(5, 16) -> 3 , C_1(5, 16) -> 16 , C_1(5, 18) -> 3 , C_1(5, 18) -> 16 , C_1(5, 19) -> 6 , C_1(5, 19) -> 14 , C_1(5, 19) -> 20 , C_1(5, 20) -> 6 , C_1(5, 20) -> 14 , C_1(5, 20) -> 20 , C_1(9, 2) -> 1 , C_1(9, 2) -> 3 , C_1(9, 2) -> 15 , C_1(9, 4) -> 1 , C_1(9, 4) -> 3 , C_1(9, 4) -> 15 , C_1(9, 5) -> 1 , C_1(9, 5) -> 3 , C_1(9, 5) -> 15 , C_1(9, 9) -> 1 , C_1(9, 9) -> 3 , C_1(9, 9) -> 15 , C_1(9, 10) -> 1 , C_1(9, 10) -> 3 , C_1(9, 10) -> 15 , C_1(9, 15) -> 1 , C_1(9, 15) -> 3 , C_1(9, 15) -> 15 , C_1(9, 16) -> 3 , C_1(9, 16) -> 16 , C_1(9, 18) -> 3 , C_1(9, 18) -> 16 , C_1(9, 19) -> 6 , C_1(9, 19) -> 14 , C_1(9, 19) -> 20 , C_1(9, 20) -> 6 , C_1(9, 20) -> 14 , C_1(9, 20) -> 20 , C_1(10, 2) -> 1 , C_1(10, 2) -> 3 , C_1(10, 2) -> 15 , C_1(10, 4) -> 1 , C_1(10, 4) -> 3 , C_1(10, 4) -> 15 , C_1(10, 5) -> 1 , C_1(10, 5) -> 3 , C_1(10, 5) -> 15 , C_1(10, 9) -> 1 , C_1(10, 9) -> 3 , C_1(10, 9) -> 15 , C_1(10, 10) -> 1 , C_1(10, 10) -> 3 , C_1(10, 10) -> 15 , C_1(10, 15) -> 1 , C_1(10, 15) -> 3 , C_1(10, 15) -> 15 , C_1(10, 16) -> 3 , C_1(10, 16) -> 16 , C_1(10, 18) -> 3 , C_1(10, 18) -> 16 , C_1(10, 19) -> 6 , C_1(10, 19) -> 14 , C_1(10, 19) -> 20 , C_1(10, 20) -> 6 , C_1(10, 20) -> 14 , C_1(10, 20) -> 20 , C_2(2, 16) -> 3 , C_2(2, 16) -> 6 , C_2(2, 16) -> 14 , C_2(2, 16) -> 18 , C_2(2, 17) -> 6 , C_2(2, 17) -> 14 , C_2(2, 17) -> 19 , C_2(2, 18) -> 3 , C_2(2, 18) -> 6 , C_2(2, 18) -> 14 , C_2(2, 18) -> 18 , C_2(2, 19) -> 6 , C_2(2, 19) -> 14 , C_2(2, 19) -> 19 , C_2(4, 16) -> 3 , C_2(4, 16) -> 6 , C_2(4, 16) -> 14 , C_2(4, 16) -> 18 , C_2(4, 17) -> 6 , C_2(4, 17) -> 14 , C_2(4, 17) -> 19 , C_2(4, 18) -> 3 , C_2(4, 18) -> 6 , C_2(4, 18) -> 14 , C_2(4, 18) -> 18 , C_2(4, 19) -> 6 , C_2(4, 19) -> 14 , C_2(4, 19) -> 19 , C_2(5, 16) -> 3 , C_2(5, 16) -> 6 , C_2(5, 16) -> 14 , C_2(5, 16) -> 18 , C_2(5, 17) -> 6 , C_2(5, 17) -> 14 , C_2(5, 17) -> 19 , C_2(5, 18) -> 3 , C_2(5, 18) -> 6 , C_2(5, 18) -> 14 , C_2(5, 18) -> 18 , C_2(5, 19) -> 6 , C_2(5, 19) -> 14 , C_2(5, 19) -> 19 , C_2(9, 16) -> 3 , C_2(9, 16) -> 6 , C_2(9, 16) -> 14 , C_2(9, 16) -> 18 , C_2(9, 17) -> 6 , C_2(9, 17) -> 14 , C_2(9, 17) -> 19 , C_2(9, 18) -> 3 , C_2(9, 18) -> 6 , C_2(9, 18) -> 14 , C_2(9, 18) -> 18 , C_2(9, 19) -> 6 , C_2(9, 19) -> 14 , C_2(9, 19) -> 19 , C_2(10, 16) -> 3 , C_2(10, 16) -> 6 , C_2(10, 16) -> 14 , C_2(10, 16) -> 18 , C_2(10, 17) -> 6 , C_2(10, 17) -> 14 , C_2(10, 17) -> 19 , C_2(10, 18) -> 3 , C_2(10, 18) -> 6 , C_2(10, 18) -> 14 , C_2(10, 18) -> 18 , C_2(10, 19) -> 6 , C_2(10, 19) -> 14 , C_2(10, 19) -> 19 , C_3(2, 18) -> 6 , C_3(2, 18) -> 14 , C_3(2, 18) -> 21 , C_3(2, 21) -> 6 , C_3(2, 21) -> 14 , C_3(2, 21) -> 21 , C_3(4, 18) -> 6 , C_3(4, 18) -> 14 , C_3(4, 18) -> 21 , C_3(4, 21) -> 6 , C_3(4, 21) -> 14 , C_3(4, 21) -> 21 , C_3(5, 18) -> 6 , C_3(5, 18) -> 14 , C_3(5, 18) -> 21 , C_3(5, 21) -> 6 , C_3(5, 21) -> 14 , C_3(5, 21) -> 21 , C_3(9, 18) -> 6 , C_3(9, 18) -> 14 , C_3(9, 18) -> 21 , C_3(9, 21) -> 6 , C_3(9, 21) -> 14 , C_3(9, 21) -> 21 , C_3(10, 18) -> 6 , C_3(10, 18) -> 14 , C_3(10, 18) -> 21 , C_3(10, 21) -> 6 , C_3(10, 21) -> 14 , C_3(10, 21) -> 21 , deeprevapp_0(2, 2) -> 3 , deeprevapp_0(2, 4) -> 3 , deeprevapp_0(2, 5) -> 3 , deeprevapp_0(2, 9) -> 3 , deeprevapp_0(2, 10) -> 3 , deeprevapp_0(4, 2) -> 3 , deeprevapp_0(4, 4) -> 3 , deeprevapp_0(4, 5) -> 3 , deeprevapp_0(4, 9) -> 3 , deeprevapp_0(4, 10) -> 3 , deeprevapp_0(5, 2) -> 3 , deeprevapp_0(5, 4) -> 3 , deeprevapp_0(5, 5) -> 3 , deeprevapp_0(5, 9) -> 3 , deeprevapp_0(5, 10) -> 3 , deeprevapp_0(9, 2) -> 3 , deeprevapp_0(9, 4) -> 3 , deeprevapp_0(9, 5) -> 3 , deeprevapp_0(9, 9) -> 3 , deeprevapp_0(9, 10) -> 3 , deeprevapp_0(10, 2) -> 3 , deeprevapp_0(10, 4) -> 3 , deeprevapp_0(10, 5) -> 3 , deeprevapp_0(10, 9) -> 3 , deeprevapp_0(10, 10) -> 3 , deeprevapp_1(2, 15) -> 3 , deeprevapp_1(2, 20) -> 6 , deeprevapp_1(2, 20) -> 14 , deeprevapp_1(4, 15) -> 3 , deeprevapp_1(4, 20) -> 6 , deeprevapp_1(4, 20) -> 14 , deeprevapp_1(5, 15) -> 3 , deeprevapp_1(5, 20) -> 6 , deeprevapp_1(5, 20) -> 14 , deeprevapp_1(9, 15) -> 3 , deeprevapp_1(9, 20) -> 6 , deeprevapp_1(9, 20) -> 14 , deeprevapp_1(10, 15) -> 3 , deeprevapp_1(10, 20) -> 6 , deeprevapp_1(10, 20) -> 14 , deeprevapp_1(15, 17) -> 6 , deeprevapp_1(15, 17) -> 14 , deeprevapp_2(2, 19) -> 6 , deeprevapp_2(2, 19) -> 14 , deeprevapp_2(4, 19) -> 6 , deeprevapp_2(4, 19) -> 14 , deeprevapp_2(5, 19) -> 6 , deeprevapp_2(5, 19) -> 14 , deeprevapp_2(9, 19) -> 6 , deeprevapp_2(9, 19) -> 14 , deeprevapp_2(10, 19) -> 6 , deeprevapp_2(10, 19) -> 14 , deeprevapp_2(15, 19) -> 6 , deeprevapp_2(15, 19) -> 14 , V_0(2) -> 1 , V_0(2) -> 3 , V_0(2) -> 4 , V_0(2) -> 7 , V_0(2) -> 13 , V_0(4) -> 1 , V_0(4) -> 3 , V_0(4) -> 4 , V_0(4) -> 7 , V_0(4) -> 13 , V_0(5) -> 1 , V_0(5) -> 3 , V_0(5) -> 4 , V_0(5) -> 7 , V_0(5) -> 13 , V_0(9) -> 1 , V_0(9) -> 3 , V_0(9) -> 4 , V_0(9) -> 7 , V_0(9) -> 13 , V_0(10) -> 1 , V_0(10) -> 3 , V_0(10) -> 4 , V_0(10) -> 7 , V_0(10) -> 13 , V_1(2) -> 3 , V_1(2) -> 6 , V_1(2) -> 14 , V_1(2) -> 16 , V_1(4) -> 3 , V_1(4) -> 6 , V_1(4) -> 14 , V_1(4) -> 16 , V_1(5) -> 3 , V_1(5) -> 6 , V_1(5) -> 14 , V_1(5) -> 16 , V_1(9) -> 3 , V_1(9) -> 6 , V_1(9) -> 14 , V_1(9) -> 16 , V_1(10) -> 3 , V_1(10) -> 6 , V_1(10) -> 14 , V_1(10) -> 16 , N_0() -> 1 , N_0() -> 3 , N_0() -> 5 , N_0() -> 7 , N_0() -> 13 , N_1() -> 6 , N_1() -> 7 , N_1() -> 13 , N_1() -> 14 , N_1() -> 17 , deeprev_0(2) -> 6 , deeprev_0(4) -> 6 , deeprev_0(5) -> 6 , deeprev_0(9) -> 6 , deeprev_0(10) -> 6 , deeprev_1(2) -> 14 , deeprev_1(4) -> 14 , deeprev_1(5) -> 14 , deeprev_1(9) -> 14 , deeprev_1(10) -> 14 , second_0(2) -> 7 , second_0(4) -> 7 , second_0(5) -> 7 , second_0(9) -> 7 , second_0(10) -> 7 , isVal_0(2) -> 8 , isVal_0(4) -> 8 , isVal_0(5) -> 8 , isVal_0(9) -> 8 , isVal_0(10) -> 8 , False_0() -> 1 , False_0() -> 3 , False_0() -> 7 , False_0() -> 9 , False_0() -> 13 , False_1() -> 8 , False_1() -> 11 , False_1() -> 12 , True_0() -> 1 , True_0() -> 3 , True_0() -> 7 , True_0() -> 10 , True_0() -> 13 , True_1() -> 8 , True_1() -> 11 , True_1() -> 12 , isNotEmptyT_0(2) -> 11 , isNotEmptyT_0(4) -> 11 , isNotEmptyT_0(5) -> 11 , isNotEmptyT_0(9) -> 11 , isNotEmptyT_0(10) -> 11 , isEmptyT_0(2) -> 12 , isEmptyT_0(4) -> 12 , isEmptyT_0(5) -> 12 , isEmptyT_0(9) -> 12 , isEmptyT_0(10) -> 12 , first_0(2) -> 13 , first_0(4) -> 13 , first_0(5) -> 13 , first_0(9) -> 13 , first_0(10) -> 13 , goal_0(2) -> 14 , goal_0(4) -> 14 , goal_0(5) -> 14 , goal_0(9) -> 14 , goal_0(10) -> 14 , 2 -> 1 , 2 -> 3 , 2 -> 7 , 2 -> 13 , 4 -> 1 , 4 -> 3 , 4 -> 7 , 4 -> 13 , 5 -> 1 , 5 -> 3 , 5 -> 7 , 5 -> 13 , 9 -> 1 , 9 -> 3 , 9 -> 7 , 9 -> 13 , 10 -> 1 , 10 -> 3 , 10 -> 7 , 10 -> 13 , 15 -> 1 , 15 -> 3 , 16 -> 3 , 18 -> 3 , 18 -> 6 , 18 -> 14 , 19 -> 6 , 19 -> 14 , 20 -> 6 , 20 -> 14 , 21 -> 6 , 21 -> 14 } Hurray, we answered YES(?,O(n^1))