YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { rec[append_0][2](Nil(), Cons(x6, Nil())) -> Cons(x6, Nil()) , rec[append_0][2](Cons(x14, x10), Cons(x6, Nil())) -> Cons(x14, rec[append_0][2](x10, Cons(x6, Nil()))) , rec[rev_0][1](Nil()) -> Nil() , rec[rev_0][1](Cons(x5, x3)) -> rec[append_0][2](rec[rev_0][1](x3), Cons(x5, Nil())) , main(x1) -> rec[rev_0][1](x1) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(Cons) = {2}, Uargs(rec[append_0][2]) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [Nil] = [0] [Cons](x1, x2) = [1] x2 + [0] [rec[append_0][2]](x1, x2) = [1] x1 + [0] [rec[rev_0][1]](x1) = [0] [main](x1) = [1] x1 + [7] The following symbols are considered usable {rec[append_0][2], rec[rev_0][1], main} The order satisfies the following ordering constraints: [rec[append_0][2](Nil(), Cons(x6, Nil()))] = [0] >= [0] = [Cons(x6, Nil())] [rec[append_0][2](Cons(x14, x10), Cons(x6, Nil()))] = [1] x10 + [0] >= [1] x10 + [0] = [Cons(x14, rec[append_0][2](x10, Cons(x6, Nil())))] [rec[rev_0][1](Nil())] = [0] >= [0] = [Nil()] [rec[rev_0][1](Cons(x5, x3))] = [0] >= [0] = [rec[append_0][2](rec[rev_0][1](x3), Cons(x5, Nil()))] [main(x1)] = [1] x1 + [7] > [0] = [rec[rev_0][1](x1)] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { rec[append_0][2](Nil(), Cons(x6, Nil())) -> Cons(x6, Nil()) , rec[append_0][2](Cons(x14, x10), Cons(x6, Nil())) -> Cons(x14, rec[append_0][2](x10, Cons(x6, Nil()))) , rec[rev_0][1](Nil()) -> Nil() , rec[rev_0][1](Cons(x5, x3)) -> rec[append_0][2](rec[rev_0][1](x3), Cons(x5, Nil())) } Weak Trs: { main(x1) -> rec[rev_0][1](x1) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(Cons) = {2}, Uargs(rec[append_0][2]) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [Nil] = [0] [Cons](x1, x2) = [1] x2 + [0] [rec[append_0][2]](x1, x2) = [1] x1 + [0] [rec[rev_0][1]](x1) = [1] [main](x1) = [1] x1 + [7] The following symbols are considered usable {rec[append_0][2], rec[rev_0][1], main} The order satisfies the following ordering constraints: [rec[append_0][2](Nil(), Cons(x6, Nil()))] = [0] >= [0] = [Cons(x6, Nil())] [rec[append_0][2](Cons(x14, x10), Cons(x6, Nil()))] = [1] x10 + [0] >= [1] x10 + [0] = [Cons(x14, rec[append_0][2](x10, Cons(x6, Nil())))] [rec[rev_0][1](Nil())] = [1] > [0] = [Nil()] [rec[rev_0][1](Cons(x5, x3))] = [1] >= [1] = [rec[append_0][2](rec[rev_0][1](x3), Cons(x5, Nil()))] [main(x1)] = [1] x1 + [7] > [1] = [rec[rev_0][1](x1)] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { rec[append_0][2](Nil(), Cons(x6, Nil())) -> Cons(x6, Nil()) , rec[append_0][2](Cons(x14, x10), Cons(x6, Nil())) -> Cons(x14, rec[append_0][2](x10, Cons(x6, Nil()))) , rec[rev_0][1](Cons(x5, x3)) -> rec[append_0][2](rec[rev_0][1](x3), Cons(x5, Nil())) } Weak Trs: { rec[rev_0][1](Nil()) -> Nil() , main(x1) -> rec[rev_0][1](x1) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(Cons) = {2}, Uargs(rec[append_0][2]) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [Nil] = [0] [Cons](x1, x2) = [1] x2 + [0] [rec[append_0][2]](x1, x2) = [1] x1 + [1] [rec[rev_0][1]](x1) = [0] [main](x1) = [1] x1 + [7] The following symbols are considered usable {rec[append_0][2], rec[rev_0][1], main} The order satisfies the following ordering constraints: [rec[append_0][2](Nil(), Cons(x6, Nil()))] = [1] > [0] = [Cons(x6, Nil())] [rec[append_0][2](Cons(x14, x10), Cons(x6, Nil()))] = [1] x10 + [1] >= [1] x10 + [1] = [Cons(x14, rec[append_0][2](x10, Cons(x6, Nil())))] [rec[rev_0][1](Nil())] = [0] >= [0] = [Nil()] [rec[rev_0][1](Cons(x5, x3))] = [0] ? [1] = [rec[append_0][2](rec[rev_0][1](x3), Cons(x5, Nil()))] [main(x1)] = [1] x1 + [7] > [0] = [rec[rev_0][1](x1)] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { rec[append_0][2](Cons(x14, x10), Cons(x6, Nil())) -> Cons(x14, rec[append_0][2](x10, Cons(x6, Nil()))) , rec[rev_0][1](Cons(x5, x3)) -> rec[append_0][2](rec[rev_0][1](x3), Cons(x5, Nil())) } Weak Trs: { rec[append_0][2](Nil(), Cons(x6, Nil())) -> Cons(x6, Nil()) , rec[rev_0][1](Nil()) -> Nil() , main(x1) -> rec[rev_0][1](x1) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { rec[rev_0][1](Cons(x5, x3)) -> rec[append_0][2](rec[rev_0][1](x3), Cons(x5, Nil())) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(Cons) = {2}, Uargs(rec[append_0][2]) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [Nil] = [4] [Cons](x1, x2) = [1] x2 + [4] [rec[append_0][2]](x1, x2) = [1] x1 + [4] [rec[rev_0][1]](x1) = [2] x1 + [0] [main](x1) = [7] x1 + [7] The following symbols are considered usable {rec[append_0][2], rec[rev_0][1], main} The order satisfies the following ordering constraints: [rec[append_0][2](Nil(), Cons(x6, Nil()))] = [8] >= [8] = [Cons(x6, Nil())] [rec[append_0][2](Cons(x14, x10), Cons(x6, Nil()))] = [1] x10 + [8] >= [1] x10 + [8] = [Cons(x14, rec[append_0][2](x10, Cons(x6, Nil())))] [rec[rev_0][1](Nil())] = [8] > [4] = [Nil()] [rec[rev_0][1](Cons(x5, x3))] = [2] x3 + [8] > [2] x3 + [4] = [rec[append_0][2](rec[rev_0][1](x3), Cons(x5, Nil()))] [main(x1)] = [7] x1 + [7] > [2] x1 + [0] = [rec[rev_0][1](x1)] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { rec[append_0][2](Cons(x14, x10), Cons(x6, Nil())) -> Cons(x14, rec[append_0][2](x10, Cons(x6, Nil()))) } Weak Trs: { rec[append_0][2](Nil(), Cons(x6, Nil())) -> Cons(x6, Nil()) , rec[rev_0][1](Nil()) -> Nil() , rec[rev_0][1](Cons(x5, x3)) -> rec[append_0][2](rec[rev_0][1](x3), Cons(x5, Nil())) , main(x1) -> rec[rev_0][1](x1) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { rec[append_0][2](Cons(x14, x10), Cons(x6, Nil())) -> Cons(x14, rec[append_0][2](x10, Cons(x6, Nil()))) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(Cons) = {2}, Uargs(rec[append_0][2]) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [Nil] = [0] [1] [Cons](x1, x2) = [1 1] x2 + [0] [0 1] [6] [rec[append_0][2]](x1, x2) = [1 2] x1 + [0 0] x2 + [0] [0 1] [0 1] [0] [rec[rev_0][1]](x1) = [4 0] x1 + [0] [0 2] [0] [main](x1) = [7 7] x1 + [7] [7 7] [7] The following symbols are considered usable {rec[append_0][2], rec[rev_0][1], main} The order satisfies the following ordering constraints: [rec[append_0][2](Nil(), Cons(x6, Nil()))] = [2] [8] > [1] [7] = [Cons(x6, Nil())] [rec[append_0][2](Cons(x14, x10), Cons(x6, Nil()))] = [1 3] x10 + [12] [0 1] [13] > [1 3] x10 + [7] [0 1] [13] = [Cons(x14, rec[append_0][2](x10, Cons(x6, Nil())))] [rec[rev_0][1](Nil())] = [0] [2] >= [0] [1] = [Nil()] [rec[rev_0][1](Cons(x5, x3))] = [4 4] x3 + [0] [0 2] [12] >= [4 4] x3 + [0] [0 2] [7] = [rec[append_0][2](rec[rev_0][1](x3), Cons(x5, Nil()))] [main(x1)] = [7 7] x1 + [7] [7 7] [7] > [4 0] x1 + [0] [0 2] [0] = [rec[rev_0][1](x1)] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { rec[append_0][2](Nil(), Cons(x6, Nil())) -> Cons(x6, Nil()) , rec[append_0][2](Cons(x14, x10), Cons(x6, Nil())) -> Cons(x14, rec[append_0][2](x10, Cons(x6, Nil()))) , rec[rev_0][1](Nil()) -> Nil() , rec[rev_0][1](Cons(x5, x3)) -> rec[append_0][2](rec[rev_0][1](x3), Cons(x5, Nil())) , main(x1) -> rec[rev_0][1](x1) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))