YES(O(1),O(n^6)) 227.99/60.05 YES(O(1),O(n^6)) 227.99/60.05 227.99/60.05 We are left with following problem, upon which TcT provides the 227.99/60.05 certificate YES(O(1),O(n^6)). 227.99/60.05 227.99/60.05 Strict Trs: 227.99/60.05 { app(app(app(compose(), f), g), x) -> app(g, app(f, x)) 227.99/60.05 , app(app(reverse2(), app(app(cons(), x), xs)), l) -> 227.99/60.05 app(app(reverse2(), xs), app(app(cons(), x), l)) 227.99/60.05 , app(app(reverse2(), nil()), l) -> l 227.99/60.05 , app(reverse(), l) -> app(app(reverse2(), l), nil()) 227.99/60.05 , app(hd(), app(app(cons(), x), xs)) -> x 227.99/60.05 , app(tl(), app(app(cons(), x), xs)) -> xs 227.99/60.05 , last() -> app(app(compose(), hd()), reverse()) 227.99/60.05 , init() -> 227.99/60.05 app(app(compose(), reverse()), 227.99/60.05 app(app(compose(), tl()), reverse())) } 227.99/60.05 Obligation: 227.99/60.05 derivational complexity 227.99/60.05 Answer: 227.99/60.05 YES(O(1),O(n^6)) 227.99/60.05 227.99/60.05 We uncurry the input using the following uncurry rules. 227.99/60.05 227.99/60.05 { app(compose_2(x_1, x_2), x_3) -> compose_3(x_1, x_2, x_3) 227.99/60.05 , app(hd(), x_1) -> hd_1(x_1) 227.99/60.05 , app(reverse(), x_1) -> reverse_1(x_1) 227.99/60.05 , app(tl(), x_1) -> tl_1(x_1) 227.99/60.05 , app(compose(), x_1) -> compose_1(x_1) 227.99/60.05 , app(compose_1(x_1), x_2) -> compose_2(x_1, x_2) 227.99/60.05 , app(reverse2(), x_1) -> reverse2_1(x_1) 227.99/60.05 , app(reverse2_1(x_1), x_2) -> reverse2_2(x_1, x_2) 227.99/60.05 , app(cons(), x_1) -> cons_1(x_1) 227.99/60.05 , app(cons_1(x_1), x_2) -> cons_2(x_1, x_2) } 227.99/60.05 227.99/60.05 We are left with following problem, upon which TcT provides the 227.99/60.05 certificate YES(O(1),O(n^6)). 227.99/60.05 227.99/60.05 Strict Trs: 227.99/60.05 { compose_3(f, g, x) -> app(g, app(f, x)) 227.99/60.05 , reverse2_2(cons_2(x, xs), l) -> reverse2_2(xs, cons_2(x, l)) 227.99/60.05 , reverse2_2(nil(), l) -> l 227.99/60.05 , reverse_1(l) -> reverse2_2(l, nil()) 227.99/60.05 , hd_1(cons_2(x, xs)) -> x 227.99/60.05 , tl_1(cons_2(x, xs)) -> xs 227.99/60.05 , last() -> compose_2(hd(), reverse()) 227.99/60.05 , init() -> compose_2(reverse(), compose_2(tl(), reverse())) } 227.99/60.05 Weak Trs: 227.99/60.05 { app(compose_2(x_1, x_2), x_3) -> compose_3(x_1, x_2, x_3) 227.99/60.05 , app(hd(), x_1) -> hd_1(x_1) 227.99/60.05 , app(reverse(), x_1) -> reverse_1(x_1) 227.99/60.05 , app(tl(), x_1) -> tl_1(x_1) 227.99/60.05 , app(compose(), x_1) -> compose_1(x_1) 227.99/60.05 , app(compose_1(x_1), x_2) -> compose_2(x_1, x_2) 227.99/60.05 , app(reverse2(), x_1) -> reverse2_1(x_1) 227.99/60.05 , app(reverse2_1(x_1), x_2) -> reverse2_2(x_1, x_2) 227.99/60.05 , app(cons(), x_1) -> cons_1(x_1) 227.99/60.05 , app(cons_1(x_1), x_2) -> cons_2(x_1, x_2) } 227.99/60.05 Obligation: 227.99/60.05 derivational complexity 227.99/60.05 Answer: 227.99/60.05 YES(O(1),O(n^6)) 227.99/60.05 227.99/60.05 We use the processor 'matrix interpretation of dimension 3' to 227.99/60.05 orient following rules strictly. 227.99/60.05 227.99/60.05 Trs: 227.99/60.05 { compose_3(f, g, x) -> app(g, app(f, x)) 227.99/60.05 , reverse2_2(nil(), l) -> l 227.99/60.05 , reverse_1(l) -> reverse2_2(l, nil()) 227.99/60.05 , hd_1(cons_2(x, xs)) -> x 227.99/60.05 , tl_1(cons_2(x, xs)) -> xs 227.99/60.05 , last() -> compose_2(hd(), reverse()) 227.99/60.05 , init() -> compose_2(reverse(), compose_2(tl(), reverse())) } 227.99/60.05 227.99/60.05 The induced complexity on above rules (modulo remaining rules) is 227.99/60.05 YES(?,O(n^3)) . These rules are removed from the problem. Note that 227.99/60.05 none of the weakly oriented rules is size-increasing. The overall 227.99/60.05 complexity is obtained by composition . 227.99/60.05 227.99/60.05 Sub-proof: 227.99/60.05 ---------- 227.99/60.05 TcT has computed the following triangular matrix interpretation. 227.99/60.05 227.99/60.05 [1 2 2] [1 0 0] [0] 227.99/60.05 [app](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [0] 227.99/60.05 [0 0 1] [0 0 1] [1] 227.99/60.05 227.99/60.05 [1 2 2] [1 2 2] [1 0 227.99/60.05 0] [1] 227.99/60.05 [compose_3](x1, x2, x3) = [0 1 0] x1 + [0 1 0] x2 + [0 1 227.99/60.05 0] x3 + [0] 227.99/60.05 [0 0 1] [0 0 1] [0 0 227.99/60.05 1] [2] 227.99/60.05 227.99/60.05 [1 0 0] [1 0 0] [0] 227.99/60.05 [reverse2_2](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [0] 227.99/60.05 [0 0 1] [0 0 1] [1] 227.99/60.05 227.99/60.05 [1 2 1] [1 0 0] [1] 227.99/60.05 [cons_2](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [0] 227.99/60.05 [0 0 1] [0 0 1] [2] 227.99/60.05 227.99/60.05 [1] 227.99/60.05 [nil] = [1] 227.99/60.05 [0] 227.99/60.05 227.99/60.05 [1 0 0] [2] 227.99/60.05 [reverse_1](x1) = [0 1 0] x1 + [1] 227.99/60.05 [0 0 1] [1] 227.99/60.05 227.99/60.05 [1 0 0] [1] 227.99/60.05 [hd_1](x1) = [0 1 0] x1 + [1] 227.99/60.05 [0 0 1] [1] 227.99/60.05 227.99/60.05 [1 0 0] [0] 227.99/60.05 [tl_1](x1) = [0 1 0] x1 + [0] 227.99/60.05 [0 0 1] [1] 227.99/60.05 227.99/60.05 [2] 227.99/60.05 [last] = [2] 227.99/60.05 [1] 227.99/60.05 227.99/60.05 [1 0 0] [1 0 0] [0] 227.99/60.05 [compose_2](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [0] 227.99/60.05 [0 0 1] [0 0 1] [1] 227.99/60.05 227.99/60.05 [0] 227.99/60.05 [hd] = [1] 227.99/60.05 [0] 227.99/60.05 227.99/60.05 [0] 227.99/60.05 [reverse] = [1] 227.99/60.05 [0] 227.99/60.05 227.99/60.05 [2] 227.99/60.05 [init] = [2] 227.99/60.05 [2] 227.99/60.05 227.99/60.05 [1] 227.99/60.05 [tl] = [0] 227.99/60.05 [0] 227.99/60.05 227.99/60.05 [2] 227.99/60.05 [compose] = [0] 227.99/60.05 [0] 227.99/60.05 227.99/60.05 [1 0 0] [1] 227.99/60.05 [compose_1](x1) = [0 1 0] x1 + [0] 227.99/60.05 [0 0 1] [0] 227.99/60.05 227.99/60.05 [2] 227.99/60.05 [reverse2] = [0] 227.99/60.05 [0] 227.99/60.05 227.99/60.05 [1 0 0] [1] 227.99/60.05 [reverse2_1](x1) = [0 1 0] x1 + [0] 227.99/60.05 [0 0 1] [0] 227.99/60.05 227.99/60.05 [2] 227.99/60.05 [cons] = [0] 227.99/60.05 [0] 227.99/60.05 227.99/60.05 [1 0 0] [1] 227.99/60.05 [cons_1](x1) = [0 1 0] x1 + [0] 227.99/60.05 [0 0 1] [1] 227.99/60.05 227.99/60.05 The order satisfies the following ordering constraints: 227.99/60.05 227.99/60.05 [app(compose_2(x_1, x_2), x_3)] = [1 2 2] [1 2 2] [1 0 0] [2] 227.99/60.05 [0 1 0] x_1 + [0 1 0] x_2 + [0 1 0] x_3 + [0] 227.99/60.05 [0 0 1] [0 0 1] [0 0 1] [2] 227.99/60.05 > [1 2 2] [1 2 2] [1 0 0] [1] 227.99/60.05 [0 1 0] x_1 + [0 1 0] x_2 + [0 1 0] x_3 + [0] 227.99/60.05 [0 0 1] [0 0 1] [0 0 1] [2] 227.99/60.05 = [compose_3(x_1, x_2, x_3)] 227.99/60.05 227.99/60.05 [app(hd(), x_1)] = [1 0 0] [2] 227.99/60.05 [0 1 0] x_1 + [1] 227.99/60.05 [0 0 1] [1] 227.99/60.05 > [1 0 0] [1] 227.99/60.05 [0 1 0] x_1 + [1] 227.99/60.05 [0 0 1] [1] 227.99/60.05 = [hd_1(x_1)] 227.99/60.05 227.99/60.05 [app(reverse(), x_1)] = [1 0 0] [2] 227.99/60.05 [0 1 0] x_1 + [1] 227.99/60.05 [0 0 1] [1] 227.99/60.05 >= [1 0 0] [2] 227.99/60.05 [0 1 0] x_1 + [1] 227.99/60.05 [0 0 1] [1] 227.99/60.05 = [reverse_1(x_1)] 227.99/60.05 227.99/60.05 [app(tl(), x_1)] = [1 0 0] [1] 227.99/60.05 [0 1 0] x_1 + [0] 227.99/60.05 [0 0 1] [1] 227.99/60.05 > [1 0 0] [0] 227.99/60.05 [0 1 0] x_1 + [0] 227.99/60.05 [0 0 1] [1] 227.99/60.05 = [tl_1(x_1)] 227.99/60.05 227.99/60.05 [app(compose(), x_1)] = [1 0 0] [2] 227.99/60.05 [0 1 0] x_1 + [0] 227.99/60.05 [0 0 1] [1] 227.99/60.05 > [1 0 0] [1] 227.99/60.05 [0 1 0] x_1 + [0] 227.99/60.05 [0 0 1] [0] 227.99/60.05 = [compose_1(x_1)] 227.99/60.05 227.99/60.05 [app(compose_1(x_1), x_2)] = [1 2 2] [1 0 0] [1] 227.99/60.05 [0 1 0] x_1 + [0 1 0] x_2 + [0] 227.99/60.05 [0 0 1] [0 0 1] [1] 227.99/60.05 > [1 0 0] [1 0 0] [0] 227.99/60.05 [0 1 0] x_1 + [0 1 0] x_2 + [0] 227.99/60.05 [0 0 1] [0 0 1] [1] 227.99/60.05 = [compose_2(x_1, x_2)] 227.99/60.05 227.99/60.05 [app(reverse2(), x_1)] = [1 0 0] [2] 227.99/60.05 [0 1 0] x_1 + [0] 227.99/60.05 [0 0 1] [1] 227.99/60.05 > [1 0 0] [1] 227.99/60.05 [0 1 0] x_1 + [0] 227.99/60.05 [0 0 1] [0] 227.99/60.05 = [reverse2_1(x_1)] 227.99/60.05 227.99/60.05 [app(reverse2_1(x_1), x_2)] = [1 2 2] [1 0 0] [1] 227.99/60.05 [0 1 0] x_1 + [0 1 0] x_2 + [0] 227.99/60.05 [0 0 1] [0 0 1] [1] 227.99/60.05 > [1 0 0] [1 0 0] [0] 227.99/60.05 [0 1 0] x_1 + [0 1 0] x_2 + [0] 227.99/60.05 [0 0 1] [0 0 1] [1] 227.99/60.05 = [reverse2_2(x_1, x_2)] 227.99/60.05 227.99/60.05 [app(cons(), x_1)] = [1 0 0] [2] 227.99/60.05 [0 1 0] x_1 + [0] 227.99/60.05 [0 0 1] [1] 227.99/60.05 > [1 0 0] [1] 227.99/60.05 [0 1 0] x_1 + [0] 227.99/60.05 [0 0 1] [1] 227.99/60.05 = [cons_1(x_1)] 227.99/60.05 227.99/60.05 [app(cons_1(x_1), x_2)] = [1 2 2] [1 0 0] [3] 227.99/60.05 [0 1 0] x_1 + [0 1 0] x_2 + [0] 227.99/60.05 [0 0 1] [0 0 1] [2] 227.99/60.05 > [1 2 1] [1 0 0] [1] 227.99/60.05 [0 1 0] x_1 + [0 1 0] x_2 + [0] 227.99/60.05 [0 0 1] [0 0 1] [2] 227.99/60.05 = [cons_2(x_1, x_2)] 227.99/60.05 227.99/60.05 [compose_3(f, g, x)] = [1 2 2] [1 2 2] [1 0 0] [1] 227.99/60.05 [0 1 0] f + [0 1 0] g + [0 1 0] x + [0] 227.99/60.05 [0 0 1] [0 0 1] [0 0 1] [2] 227.99/60.05 > [1 2 2] [1 2 2] [1 0 0] [0] 227.99/60.05 [0 1 0] f + [0 1 0] g + [0 1 0] x + [0] 227.99/60.05 [0 0 1] [0 0 1] [0 0 1] [2] 227.99/60.05 = [app(g, app(f, x))] 227.99/60.05 227.99/60.05 [reverse2_2(cons_2(x, xs), l)] = [1 2 1] [1 0 0] [1 0 0] [1] 227.99/60.05 [0 1 0] x + [0 1 0] l + [0 1 0] xs + [0] 227.99/60.05 [0 0 1] [0 0 1] [0 0 1] [3] 227.99/60.05 >= [1 2 1] [1 0 0] [1 0 0] [1] 227.99/60.05 [0 1 0] x + [0 1 0] l + [0 1 0] xs + [0] 227.99/60.05 [0 0 1] [0 0 1] [0 0 1] [3] 227.99/60.05 = [reverse2_2(xs, cons_2(x, l))] 227.99/60.05 227.99/60.05 [reverse2_2(nil(), l)] = [1 0 0] [1] 227.99/60.05 [0 1 0] l + [1] 227.99/60.05 [0 0 1] [1] 227.99/60.05 > [1 0 0] [0] 227.99/60.05 [0 1 0] l + [0] 227.99/60.05 [0 0 1] [0] 227.99/60.05 = [l] 227.99/60.05 227.99/60.05 [reverse_1(l)] = [1 0 0] [2] 227.99/60.05 [0 1 0] l + [1] 227.99/60.05 [0 0 1] [1] 227.99/60.05 > [1 0 0] [1] 227.99/60.05 [0 1 0] l + [1] 227.99/60.05 [0 0 1] [1] 227.99/60.05 = [reverse2_2(l, nil())] 227.99/60.05 227.99/60.05 [hd_1(cons_2(x, xs))] = [1 2 1] [1 0 0] [2] 227.99/60.05 [0 1 0] x + [0 1 0] xs + [1] 227.99/60.05 [0 0 1] [0 0 1] [3] 227.99/60.05 > [1 0 0] [0] 227.99/60.05 [0 1 0] x + [0] 227.99/60.05 [0 0 1] [0] 227.99/60.05 = [x] 227.99/60.05 227.99/60.05 [tl_1(cons_2(x, xs))] = [1 2 1] [1 0 0] [1] 227.99/60.05 [0 1 0] x + [0 1 0] xs + [0] 227.99/60.05 [0 0 1] [0 0 1] [3] 227.99/60.05 > [1 0 0] [0] 227.99/60.05 [0 1 0] xs + [0] 227.99/60.05 [0 0 1] [0] 227.99/60.05 = [xs] 227.99/60.05 227.99/60.05 [last()] = [2] 227.99/60.05 [2] 227.99/60.05 [1] 227.99/60.05 > [0] 227.99/60.05 [2] 227.99/60.05 [1] 227.99/60.05 = [compose_2(hd(), reverse())] 227.99/60.05 227.99/60.05 [init()] = [2] 227.99/60.05 [2] 227.99/60.05 [2] 227.99/60.05 > [1] 227.99/60.05 [2] 227.99/60.05 [2] 227.99/60.05 = [compose_2(reverse(), compose_2(tl(), reverse()))] 227.99/60.05 227.99/60.05 227.99/60.05 We return to the main proof. 227.99/60.05 227.99/60.05 We are left with following problem, upon which TcT provides the 227.99/60.05 certificate YES(?,O(n^1)). 227.99/60.05 227.99/60.05 Strict Trs: 227.99/60.05 { reverse2_2(cons_2(x, xs), l) -> reverse2_2(xs, cons_2(x, l)) } 227.99/60.05 Weak Trs: 227.99/60.05 { app(compose_2(x_1, x_2), x_3) -> compose_3(x_1, x_2, x_3) 227.99/60.05 , app(hd(), x_1) -> hd_1(x_1) 227.99/60.05 , app(reverse(), x_1) -> reverse_1(x_1) 227.99/60.05 , app(tl(), x_1) -> tl_1(x_1) 227.99/60.05 , app(compose(), x_1) -> compose_1(x_1) 227.99/60.05 , app(compose_1(x_1), x_2) -> compose_2(x_1, x_2) 227.99/60.05 , app(reverse2(), x_1) -> reverse2_1(x_1) 227.99/60.05 , app(reverse2_1(x_1), x_2) -> reverse2_2(x_1, x_2) 227.99/60.05 , app(cons(), x_1) -> cons_1(x_1) 227.99/60.05 , app(cons_1(x_1), x_2) -> cons_2(x_1, x_2) } 227.99/60.05 Obligation: 227.99/60.05 derivational complexity 227.99/60.05 Answer: 227.99/60.05 YES(?,O(n^1)) 227.99/60.05 227.99/60.05 The problem is match-bounded by 1. The enriched problem is 227.99/60.05 compatible with the following automaton. 227.99/60.05 { app_0(1, 1) -> 1 227.99/60.05 , compose_3_0(1, 1, 1) -> 1 227.99/60.05 , reverse2_2_0(1, 1) -> 1 227.99/60.05 , reverse2_2_1(1, 2) -> 1 227.99/60.05 , cons_2_0(1, 1) -> 1 227.99/60.05 , cons_2_1(1, 1) -> 2 227.99/60.05 , cons_2_1(1, 2) -> 2 227.99/60.05 , reverse_1_0(1) -> 1 227.99/60.05 , hd_1_0(1) -> 1 227.99/60.05 , tl_1_0(1) -> 1 227.99/60.05 , compose_2_0(1, 1) -> 1 227.99/60.05 , hd_0() -> 1 227.99/60.05 , reverse_0() -> 1 227.99/60.05 , tl_0() -> 1 227.99/60.05 , compose_0() -> 1 227.99/60.05 , compose_1_0(1) -> 1 227.99/60.05 , reverse2_0() -> 1 227.99/60.05 , reverse2_1_0(1) -> 1 227.99/60.05 , cons_0() -> 1 227.99/60.05 , cons_1_0(1) -> 1 } 227.99/60.05 227.99/60.05 Hurray, we answered YES(O(1),O(n^6)) 227.99/60.06 EOF