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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) , Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) , Concat(Id(), s) -> s , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) } 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 considered usable: Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, Uargs(Frozen) = {2}, Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, Uargs(Concat) = {2} TcT has computed the following constructor-restricted polynomial interpretation. [Term_sub](x1, x2) = x1 + x1*x2 + x2 [Case](x1, x2, x3) = 1 + x1 + x3 [Frozen](x1, x2, x3, x4) = x1 + x1*x4 + x2 + x2*x4 + x3 + x3*x4 + x4 [Sum_sub](x1, x2) = 1 [Sum_constant](x1) = 0 [Left]() = 0 [Right]() = 0 [Sum_term_var](x1) = 1 [Term_app](x1, x2) = 1 + x1 + x2 [Term_pair](x1, x2) = 1 + x1 + x2 [Term_inl](x1) = x1 [Term_inr](x1) = x1 [Term_var](x1) = 0 [Id]() = 0 [Cons_usual](x1, x2, x3) = 2 + x2 + x3 [Cons_sum](x1, x2, x3) = x3 [Concat](x1, x2) = x1 + x1*x2 + x2 The following symbols are considered usable {Term_sub, Frozen, Sum_sub, Concat} This order satisfies the following ordering constraints. [Term_sub(Term_sub(m, s), t)] = m + m*s + s + m*t + m*s*t + s*t + t >= m + m*s + m*s*t + m*t + s + s*t + t = [Term_sub(m, Concat(s, t))] [Term_sub(Case(m, xi, n), s)] = 1 + m + n + 2*s + m*s + n*s >= m + m*s + 1 + 2*s + n + n*s = [Frozen(m, Sum_sub(xi, s), n, s)] [Term_sub(Term_app(m, n), s)] = 1 + m + n + 2*s + m*s + n*s >= 1 + m + m*s + 2*s + n + n*s = [Term_app(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_pair(m, n), s)] = 1 + m + n + 2*s + m*s + n*s >= 1 + m + m*s + 2*s + n + n*s = [Term_pair(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_inl(m), s)] = m + m*s + s >= m + m*s + s = [Term_inl(Term_sub(m, s))] [Term_sub(Term_inr(m), s)] = m + m*s + s >= m + m*s + s = [Term_inr(Term_sub(m, s))] [Term_sub(Term_var(x), Id())] = >= = [Term_var(x)] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s > m = [m] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s > s = [Term_sub(Term_var(x), s)] [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = s >= s = [Term_sub(Term_var(x), s)] [Frozen(m, Sum_constant(Left()), n, s)] = m + m*s + n + n*s + s >= m + m*s + s = [Term_sub(m, s)] [Frozen(m, Sum_constant(Right()), n, s)] = m + m*s + n + n*s + s >= n + n*s + s = [Term_sub(n, s)] [Frozen(m, Sum_term_var(xi), n, s)] = m + m*s + 1 + 2*s + n + n*s >= 1 + m + m*s + 2*s + n + n*s = [Case(Term_sub(m, s), xi, Term_sub(n, s))] [Sum_sub(xi, Id())] = 1 >= 1 = [Sum_term_var(xi)] [Sum_sub(xi, Cons_usual(y, m, s))] = 1 >= 1 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 >= 1 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 > = [Sum_constant(k)] [Concat(Id(), s)] = s >= s = [s] [Concat(Cons_usual(x, m, s), t)] = 2 + m + s + 3*t + m*t + s*t >= 2 + m + m*t + 2*t + s + s*t = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] [Concat(Cons_sum(xi, k, s), t)] = s + s*t + t >= s + s*t + t = [Cons_sum(xi, k, Concat(s, t))] [Concat(Concat(s, t), u)] = s + s*t + t + s*u + s*t*u + t*u + u >= s + s*t + s*t*u + s*u + t + t*u + u = [Concat(s, Concat(t, u))] 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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) , Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Concat(Id(), s) -> s , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Weak Trs: { Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { Term_sub(Term_var(x), Id()) -> Term_var(x) , Concat(Id(), s) -> s } 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 considered usable: Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, Uargs(Frozen) = {2}, Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, Uargs(Concat) = {2} TcT has computed the following constructor-restricted polynomial interpretation. [Term_sub](x1, x2) = x1 + x1*x2 + x2 [Case](x1, x2, x3) = 1 + x1 + x3 [Frozen](x1, x2, x3, x4) = x1 + x1*x4 + x2 + x2*x4 + x3 + x3*x4 + x4 [Sum_sub](x1, x2) = 1 [Sum_constant](x1) = 0 [Left]() = 0 [Right]() = 0 [Sum_term_var](x1) = 1 [Term_app](x1, x2) = 1 + x1 + x2 [Term_pair](x1, x2) = 2 + x1 + x2 [Term_inl](x1) = x1 [Term_inr](x1) = x1 [Term_var](x1) = 0 [Id]() = 2 [Cons_usual](x1, x2, x3) = 2 + x2 + x3 [Cons_sum](x1, x2, x3) = x3 [Concat](x1, x2) = x1 + x1*x2 + x2 The following symbols are considered usable {Term_sub, Frozen, Sum_sub, Concat} This order satisfies the following ordering constraints. [Term_sub(Term_sub(m, s), t)] = m + m*s + s + m*t + m*s*t + s*t + t >= m + m*s + m*s*t + m*t + s + s*t + t = [Term_sub(m, Concat(s, t))] [Term_sub(Case(m, xi, n), s)] = 1 + m + n + 2*s + m*s + n*s >= m + m*s + 1 + 2*s + n + n*s = [Frozen(m, Sum_sub(xi, s), n, s)] [Term_sub(Term_app(m, n), s)] = 1 + m + n + 2*s + m*s + n*s >= 1 + m + m*s + 2*s + n + n*s = [Term_app(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_pair(m, n), s)] = 2 + m + n + 3*s + m*s + n*s >= 2 + m + m*s + 2*s + n + n*s = [Term_pair(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_inl(m), s)] = m + m*s + s >= m + m*s + s = [Term_inl(Term_sub(m, s))] [Term_sub(Term_inr(m), s)] = m + m*s + s >= m + m*s + s = [Term_inr(Term_sub(m, s))] [Term_sub(Term_var(x), Id())] = 2 > = [Term_var(x)] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s > m = [m] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s > s = [Term_sub(Term_var(x), s)] [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = s >= s = [Term_sub(Term_var(x), s)] [Frozen(m, Sum_constant(Left()), n, s)] = m + m*s + n + n*s + s >= m + m*s + s = [Term_sub(m, s)] [Frozen(m, Sum_constant(Right()), n, s)] = m + m*s + n + n*s + s >= n + n*s + s = [Term_sub(n, s)] [Frozen(m, Sum_term_var(xi), n, s)] = m + m*s + 1 + 2*s + n + n*s >= 1 + m + m*s + 2*s + n + n*s = [Case(Term_sub(m, s), xi, Term_sub(n, s))] [Sum_sub(xi, Id())] = 1 >= 1 = [Sum_term_var(xi)] [Sum_sub(xi, Cons_usual(y, m, s))] = 1 >= 1 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 >= 1 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 > = [Sum_constant(k)] [Concat(Id(), s)] = 2 + 3*s > s = [s] [Concat(Cons_usual(x, m, s), t)] = 2 + m + s + 3*t + m*t + s*t >= 2 + m + m*t + 2*t + s + s*t = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] [Concat(Cons_sum(xi, k, s), t)] = s + s*t + t >= s + s*t + t = [Cons_sum(xi, k, Concat(s, t))] [Concat(Concat(s, t), u)] = s + s*t + t + s*u + s*t*u + t*u + u >= s + s*t + s*t*u + s*u + t + t*u + u = [Concat(s, Concat(t, u))] 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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) , Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Weak Trs: { Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) , Concat(Id(), s) -> s } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) } 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 considered usable: Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, Uargs(Frozen) = {2}, Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, Uargs(Concat) = {2} TcT has computed the following constructor-restricted polynomial interpretation. [Term_sub](x1, x2) = 2*x1 + 2*x1*x2 + x2 [Case](x1, x2, x3) = 2 + x1 + x3 [Frozen](x1, x2, x3, x4) = 2 + 2*x1 + 2*x1*x4 + x2 + 2*x3 + 2*x3*x4 + 2*x4 [Sum_sub](x1, x2) = 2*x2 [Sum_constant](x1) = 0 [Left]() = 0 [Right]() = 0 [Sum_term_var](x1) = 0 [Term_app](x1, x2) = 2 + x1 + x2 [Term_pair](x1, x2) = 1 + x1 + x2 [Term_inl](x1) = x1 [Term_inr](x1) = x1 [Term_var](x1) = 0 [Id]() = 0 [Cons_usual](x1, x2, x3) = 1 + x2 + x3 [Cons_sum](x1, x2, x3) = x3 [Concat](x1, x2) = 2*x1 + 2*x1*x2 + x2 The following symbols are considered usable {Term_sub, Frozen, Sum_sub, Concat} This order satisfies the following ordering constraints. [Term_sub(Term_sub(m, s), t)] = 4*m + 4*m*s + 2*s + 4*m*t + 4*m*s*t + 2*s*t + t >= 2*m + 4*m*s + 4*m*s*t + 2*m*t + 2*s + 2*s*t + t = [Term_sub(m, Concat(s, t))] [Term_sub(Case(m, xi, n), s)] = 4 + 2*m + 2*n + 5*s + 2*m*s + 2*n*s > 2 + 2*m + 2*m*s + 4*s + 2*n + 2*n*s = [Frozen(m, Sum_sub(xi, s), n, s)] [Term_sub(Term_app(m, n), s)] = 4 + 2*m + 2*n + 5*s + 2*m*s + 2*n*s > 2 + 2*m + 2*m*s + 2*s + 2*n + 2*n*s = [Term_app(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_pair(m, n), s)] = 2 + 2*m + 2*n + 3*s + 2*m*s + 2*n*s > 1 + 2*m + 2*m*s + 2*s + 2*n + 2*n*s = [Term_pair(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_inl(m), s)] = 2*m + 2*m*s + s >= 2*m + 2*m*s + s = [Term_inl(Term_sub(m, s))] [Term_sub(Term_inr(m), s)] = 2*m + 2*m*s + s >= 2*m + 2*m*s + s = [Term_inr(Term_sub(m, s))] [Term_sub(Term_var(x), Id())] = >= = [Term_var(x)] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 1 + m + s > m = [m] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 1 + m + s > s = [Term_sub(Term_var(x), s)] [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = s >= s = [Term_sub(Term_var(x), s)] [Frozen(m, Sum_constant(Left()), n, s)] = 2 + 2*m + 2*m*s + 2*n + 2*n*s + 2*s > 2*m + 2*m*s + s = [Term_sub(m, s)] [Frozen(m, Sum_constant(Right()), n, s)] = 2 + 2*m + 2*m*s + 2*n + 2*n*s + 2*s > 2*n + 2*n*s + s = [Term_sub(n, s)] [Frozen(m, Sum_term_var(xi), n, s)] = 2 + 2*m + 2*m*s + 2*n + 2*n*s + 2*s >= 2 + 2*m + 2*m*s + 2*s + 2*n + 2*n*s = [Case(Term_sub(m, s), xi, Term_sub(n, s))] [Sum_sub(xi, Id())] = >= = [Sum_term_var(xi)] [Sum_sub(xi, Cons_usual(y, m, s))] = 2 + 2*m + 2*s > 2*s = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 2*s >= 2*s = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 2*s >= = [Sum_constant(k)] [Concat(Id(), s)] = s >= s = [s] [Concat(Cons_usual(x, m, s), t)] = 2 + 2*m + 2*s + 3*t + 2*m*t + 2*s*t > 1 + 2*m + 2*m*t + 2*t + 2*s + 2*s*t = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] [Concat(Cons_sum(xi, k, s), t)] = 2*s + 2*s*t + t >= 2*s + 2*s*t + t = [Cons_sum(xi, k, Concat(s, t))] [Concat(Concat(s, t), u)] = 4*s + 4*s*t + 2*t + 4*s*u + 4*s*t*u + 2*t*u + u >= 2*s + 4*s*t + 4*s*t*u + 2*s*u + 2*t + 2*t*u + u = [Concat(s, Concat(t, u))] 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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Weak Trs: { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) , Concat(Id(), s) -> s , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) } 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 considered usable: Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, Uargs(Frozen) = {2}, Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, Uargs(Concat) = {2} TcT has computed the following constructor-restricted polynomial interpretation. [Term_sub](x1, x2) = x1 + x1*x2 + x2 [Case](x1, x2, x3) = 1 + x1 + x3 [Frozen](x1, x2, x3, x4) = x1 + x1*x4 + x2 + 2*x2*x4 + x3 + x3*x4 [Sum_sub](x1, x2) = 1 [Sum_constant](x1) = 1 [Left]() = 0 [Right]() = 0 [Sum_term_var](x1) = 1 [Term_app](x1, x2) = 1 + x1 + x2 [Term_pair](x1, x2) = 1 + x1 + x2 [Term_inl](x1) = x1 [Term_inr](x1) = x1 [Term_var](x1) = 0 [Id]() = 0 [Cons_usual](x1, x2, x3) = 1 + x2 + x3 [Cons_sum](x1, x2, x3) = 2 + x3 [Concat](x1, x2) = x1 + x1*x2 + x2 The following symbols are considered usable {Term_sub, Frozen, Sum_sub, Concat} This order satisfies the following ordering constraints. [Term_sub(Term_sub(m, s), t)] = m + m*s + s + m*t + m*s*t + s*t + t >= m + m*s + m*s*t + m*t + s + s*t + t = [Term_sub(m, Concat(s, t))] [Term_sub(Case(m, xi, n), s)] = 1 + m + n + 2*s + m*s + n*s >= m + m*s + 1 + 2*s + n + n*s = [Frozen(m, Sum_sub(xi, s), n, s)] [Term_sub(Term_app(m, n), s)] = 1 + m + n + 2*s + m*s + n*s >= 1 + m + m*s + 2*s + n + n*s = [Term_app(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_pair(m, n), s)] = 1 + m + n + 2*s + m*s + n*s >= 1 + m + m*s + 2*s + n + n*s = [Term_pair(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_inl(m), s)] = m + m*s + s >= m + m*s + s = [Term_inl(Term_sub(m, s))] [Term_sub(Term_inr(m), s)] = m + m*s + s >= m + m*s + s = [Term_inr(Term_sub(m, s))] [Term_sub(Term_var(x), Id())] = >= = [Term_var(x)] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 1 + m + s > m = [m] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 1 + m + s > s = [Term_sub(Term_var(x), s)] [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = 2 + s > s = [Term_sub(Term_var(x), s)] [Frozen(m, Sum_constant(Left()), n, s)] = m + m*s + 1 + 2*s + n + n*s > m + m*s + s = [Term_sub(m, s)] [Frozen(m, Sum_constant(Right()), n, s)] = m + m*s + 1 + 2*s + n + n*s > n + n*s + s = [Term_sub(n, s)] [Frozen(m, Sum_term_var(xi), n, s)] = m + m*s + 1 + 2*s + n + n*s >= 1 + m + m*s + 2*s + n + n*s = [Case(Term_sub(m, s), xi, Term_sub(n, s))] [Sum_sub(xi, Id())] = 1 >= 1 = [Sum_term_var(xi)] [Sum_sub(xi, Cons_usual(y, m, s))] = 1 >= 1 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 >= 1 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 >= 1 = [Sum_constant(k)] [Concat(Id(), s)] = s >= s = [s] [Concat(Cons_usual(x, m, s), t)] = 1 + m + s + 2*t + m*t + s*t >= 1 + m + m*t + 2*t + s + s*t = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] [Concat(Cons_sum(xi, k, s), t)] = 2 + s + 3*t + s*t >= 2 + s + s*t + t = [Cons_sum(xi, k, Concat(s, t))] [Concat(Concat(s, t), u)] = s + s*t + t + s*u + s*t*u + t*u + u >= s + s*t + s*t*u + s*u + t + t*u + u = [Concat(s, Concat(t, u))] 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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Weak Trs: { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) , Concat(Id(), s) -> s , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) } 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 considered usable: Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, Uargs(Frozen) = {2}, Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, Uargs(Concat) = {2} TcT has computed the following constructor-restricted polynomial interpretation. [Term_sub](x1, x2) = 2*x1 + 2*x1*x2 + x2 [Case](x1, x2, x3) = 1 + x1 + x3 [Frozen](x1, x2, x3, x4) = 2*x1 + 2*x1*x4 + x2 + 2*x2*x3 + x2*x4 + 2*x3*x4 + x4 [Sum_sub](x1, x2) = 1 [Sum_constant](x1) = 1 [Left]() = 0 [Right]() = 0 [Sum_term_var](x1) = 1 [Term_app](x1, x2) = 1 + x1 + x2 [Term_pair](x1, x2) = 1 + x1 + x2 [Term_inl](x1) = x1 [Term_inr](x1) = 2 + x1 [Term_var](x1) = 0 [Id]() = 0 [Cons_usual](x1, x2, x3) = 1 + x2 + x3 [Cons_sum](x1, x2, x3) = x3 [Concat](x1, x2) = 2*x1 + 2*x1*x2 + x2 The following symbols are considered usable {Term_sub, Frozen, Sum_sub, Concat} This order satisfies the following ordering constraints. [Term_sub(Term_sub(m, s), t)] = 4*m + 4*m*s + 2*s + 4*m*t + 4*m*s*t + 2*s*t + t >= 2*m + 4*m*s + 4*m*s*t + 2*m*t + 2*s + 2*s*t + t = [Term_sub(m, Concat(s, t))] [Term_sub(Case(m, xi, n), s)] = 2 + 2*m + 2*n + 3*s + 2*m*s + 2*n*s > 2*m + 2*m*s + 1 + 2*n + 2*s + 2*n*s = [Frozen(m, Sum_sub(xi, s), n, s)] [Term_sub(Term_app(m, n), s)] = 2 + 2*m + 2*n + 3*s + 2*m*s + 2*n*s > 1 + 2*m + 2*m*s + 2*s + 2*n + 2*n*s = [Term_app(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_pair(m, n), s)] = 2 + 2*m + 2*n + 3*s + 2*m*s + 2*n*s > 1 + 2*m + 2*m*s + 2*s + 2*n + 2*n*s = [Term_pair(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_inl(m), s)] = 2*m + 2*m*s + s >= 2*m + 2*m*s + s = [Term_inl(Term_sub(m, s))] [Term_sub(Term_inr(m), s)] = 4 + 2*m + 5*s + 2*m*s > 2 + 2*m + 2*m*s + s = [Term_inr(Term_sub(m, s))] [Term_sub(Term_var(x), Id())] = >= = [Term_var(x)] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 1 + m + s > m = [m] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 1 + m + s > s = [Term_sub(Term_var(x), s)] [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = s >= s = [Term_sub(Term_var(x), s)] [Frozen(m, Sum_constant(Left()), n, s)] = 2*m + 2*m*s + 1 + 2*n + 2*s + 2*n*s > 2*m + 2*m*s + s = [Term_sub(m, s)] [Frozen(m, Sum_constant(Right()), n, s)] = 2*m + 2*m*s + 1 + 2*n + 2*s + 2*n*s > 2*n + 2*n*s + s = [Term_sub(n, s)] [Frozen(m, Sum_term_var(xi), n, s)] = 2*m + 2*m*s + 1 + 2*n + 2*s + 2*n*s >= 1 + 2*m + 2*m*s + 2*s + 2*n + 2*n*s = [Case(Term_sub(m, s), xi, Term_sub(n, s))] [Sum_sub(xi, Id())] = 1 >= 1 = [Sum_term_var(xi)] [Sum_sub(xi, Cons_usual(y, m, s))] = 1 >= 1 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 >= 1 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 >= 1 = [Sum_constant(k)] [Concat(Id(), s)] = s >= s = [s] [Concat(Cons_usual(x, m, s), t)] = 2 + 2*m + 2*s + 3*t + 2*m*t + 2*s*t > 1 + 2*m + 2*m*t + 2*t + 2*s + 2*s*t = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] [Concat(Cons_sum(xi, k, s), t)] = 2*s + 2*s*t + t >= 2*s + 2*s*t + t = [Cons_sum(xi, k, Concat(s, t))] [Concat(Concat(s, t), u)] = 4*s + 4*s*t + 2*t + 4*s*u + 4*s*t*u + 2*t*u + u >= 2*s + 4*s*t + 4*s*t*u + 2*s*u + 2*t + 2*t*u + u = [Concat(s, Concat(t, u))] 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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Weak Trs: { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) , Concat(Id(), s) -> s , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) } 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 considered usable: Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, Uargs(Frozen) = {2}, Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, Uargs(Concat) = {2} TcT has computed the following constructor-restricted polynomial interpretation. [Term_sub](x1, x2) = x1 + 2*x1*x2 + x2 [Case](x1, x2, x3) = 1 + x1 + x3 [Frozen](x1, x2, x3, x4) = 1 + x1 + 2*x1*x4 + x2 + x3 + 2*x3*x4 + 2*x4 [Sum_sub](x1, x2) = x2 [Sum_constant](x1) = 0 [Left]() = 0 [Right]() = 0 [Sum_term_var](x1) = 0 [Term_app](x1, x2) = 2 + x1 + x2 [Term_pair](x1, x2) = 1 + x1 + x2 [Term_inl](x1) = x1 [Term_inr](x1) = x1 [Term_var](x1) = 0 [Id]() = 0 [Cons_usual](x1, x2, x3) = 1 + x2 + x3 [Cons_sum](x1, x2, x3) = 1 + x3 [Concat](x1, x2) = x1 + 2*x1*x2 + x2 The following symbols are considered usable {Term_sub, Frozen, Sum_sub, Concat} This order satisfies the following ordering constraints. [Term_sub(Term_sub(m, s), t)] = m + 2*m*s + s + 2*m*t + 4*m*s*t + 2*s*t + t >= m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t = [Term_sub(m, Concat(s, t))] [Term_sub(Case(m, xi, n), s)] = 1 + m + n + 3*s + 2*m*s + 2*n*s >= 1 + m + 2*m*s + 3*s + n + 2*n*s = [Frozen(m, Sum_sub(xi, s), n, s)] [Term_sub(Term_app(m, n), s)] = 2 + m + n + 5*s + 2*m*s + 2*n*s >= 2 + m + 2*m*s + 2*s + n + 2*n*s = [Term_app(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_pair(m, n), s)] = 1 + m + n + 3*s + 2*m*s + 2*n*s >= 1 + m + 2*m*s + 2*s + n + 2*n*s = [Term_pair(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_inl(m), s)] = m + 2*m*s + s >= m + 2*m*s + s = [Term_inl(Term_sub(m, s))] [Term_sub(Term_inr(m), s)] = m + 2*m*s + s >= m + 2*m*s + s = [Term_inr(Term_sub(m, s))] [Term_sub(Term_var(x), Id())] = >= = [Term_var(x)] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 1 + m + s > m = [m] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 1 + m + s > s = [Term_sub(Term_var(x), s)] [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = 1 + s > s = [Term_sub(Term_var(x), s)] [Frozen(m, Sum_constant(Left()), n, s)] = 1 + m + 2*m*s + n + 2*n*s + 2*s > m + 2*m*s + s = [Term_sub(m, s)] [Frozen(m, Sum_constant(Right()), n, s)] = 1 + m + 2*m*s + n + 2*n*s + 2*s > n + 2*n*s + s = [Term_sub(n, s)] [Frozen(m, Sum_term_var(xi), n, s)] = 1 + m + 2*m*s + n + 2*n*s + 2*s >= 1 + m + 2*m*s + 2*s + n + 2*n*s = [Case(Term_sub(m, s), xi, Term_sub(n, s))] [Sum_sub(xi, Id())] = >= = [Sum_term_var(xi)] [Sum_sub(xi, Cons_usual(y, m, s))] = 1 + m + s > s = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 + s > s = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 + s > = [Sum_constant(k)] [Concat(Id(), s)] = s >= s = [s] [Concat(Cons_usual(x, m, s), t)] = 1 + m + s + 3*t + 2*m*t + 2*s*t >= 1 + m + 2*m*t + 2*t + s + 2*s*t = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] [Concat(Cons_sum(xi, k, s), t)] = 1 + s + 3*t + 2*s*t >= 1 + s + 2*s*t + t = [Cons_sum(xi, k, Concat(s, t))] [Concat(Concat(s, t), u)] = s + 2*s*t + t + 2*s*u + 4*s*t*u + 2*t*u + u >= s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u = [Concat(s, Concat(t, u))] 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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Weak Trs: { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) , Concat(Id(), s) -> s , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { Sum_sub(xi, Id()) -> Sum_term_var(xi) } 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 considered usable: Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, Uargs(Frozen) = {2}, Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, Uargs(Concat) = {2} TcT has computed the following constructor-restricted polynomial interpretation. [Term_sub](x1, x2) = x1 + 2*x1*x2 + x2 [Case](x1, x2, x3) = 1 + x1 + x3 [Frozen](x1, x2, x3, x4) = 1 + x1 + 2*x1*x4 + x2 + x3 + 2*x3*x4 + 2*x4 [Sum_sub](x1, x2) = x2 [Sum_constant](x1) = 0 [Left]() = 0 [Right]() = 0 [Sum_term_var](x1) = 0 [Term_app](x1, x2) = 1 + x1 + x2 [Term_pair](x1, x2) = 1 + x1 + x2 [Term_inl](x1) = x1 [Term_inr](x1) = x1 [Term_var](x1) = 0 [Id]() = 1 [Cons_usual](x1, x2, x3) = 2 + x2 + x3 [Cons_sum](x1, x2, x3) = x3 [Concat](x1, x2) = x1 + 2*x1*x2 + x2 The following symbols are considered usable {Term_sub, Frozen, Sum_sub, Concat} This order satisfies the following ordering constraints. [Term_sub(Term_sub(m, s), t)] = m + 2*m*s + s + 2*m*t + 4*m*s*t + 2*s*t + t >= m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t = [Term_sub(m, Concat(s, t))] [Term_sub(Case(m, xi, n), s)] = 1 + m + n + 3*s + 2*m*s + 2*n*s >= 1 + m + 2*m*s + 3*s + n + 2*n*s = [Frozen(m, Sum_sub(xi, s), n, s)] [Term_sub(Term_app(m, n), s)] = 1 + m + n + 3*s + 2*m*s + 2*n*s >= 1 + m + 2*m*s + 2*s + n + 2*n*s = [Term_app(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_pair(m, n), s)] = 1 + m + n + 3*s + 2*m*s + 2*n*s >= 1 + m + 2*m*s + 2*s + n + 2*n*s = [Term_pair(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_inl(m), s)] = m + 2*m*s + s >= m + 2*m*s + s = [Term_inl(Term_sub(m, s))] [Term_sub(Term_inr(m), s)] = m + 2*m*s + s >= m + 2*m*s + s = [Term_inr(Term_sub(m, s))] [Term_sub(Term_var(x), Id())] = 1 > = [Term_var(x)] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s > m = [m] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s > s = [Term_sub(Term_var(x), s)] [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = s >= s = [Term_sub(Term_var(x), s)] [Frozen(m, Sum_constant(Left()), n, s)] = 1 + m + 2*m*s + n + 2*n*s + 2*s > m + 2*m*s + s = [Term_sub(m, s)] [Frozen(m, Sum_constant(Right()), n, s)] = 1 + m + 2*m*s + n + 2*n*s + 2*s > n + 2*n*s + s = [Term_sub(n, s)] [Frozen(m, Sum_term_var(xi), n, s)] = 1 + m + 2*m*s + n + 2*n*s + 2*s >= 1 + m + 2*m*s + 2*s + n + 2*n*s = [Case(Term_sub(m, s), xi, Term_sub(n, s))] [Sum_sub(xi, Id())] = 1 > = [Sum_term_var(xi)] [Sum_sub(xi, Cons_usual(y, m, s))] = 2 + m + s > s = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = s >= s = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = s >= = [Sum_constant(k)] [Concat(Id(), s)] = 1 + 3*s > s = [s] [Concat(Cons_usual(x, m, s), t)] = 2 + m + s + 5*t + 2*m*t + 2*s*t >= 2 + m + 2*m*t + 2*t + s + 2*s*t = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] [Concat(Cons_sum(xi, k, s), t)] = s + 2*s*t + t >= s + 2*s*t + t = [Cons_sum(xi, k, Concat(s, t))] [Concat(Concat(s, t), u)] = s + 2*s*t + t + 2*s*u + 4*s*t*u + 2*t*u + u >= s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u = [Concat(s, Concat(t, u))] 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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Weak Trs: { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) , Concat(Id(), s) -> s , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) } 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 considered usable: Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, Uargs(Frozen) = {2}, Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, Uargs(Concat) = {2} TcT has computed the following constructor-restricted polynomial interpretation. [Term_sub](x1, x2) = x1 + x1*x2 + 2*x1^2 + x2 [Case](x1, x2, x3) = 1 + x1 + x3 [Frozen](x1, x2, x3, x4) = 1 + x1 + x1*x4 + 2*x1^2 + 2*x2 + x3 + x3*x4 + 2*x3^2 + 2*x4 [Sum_sub](x1, x2) = 0 [Sum_constant](x1) = 0 [Left]() = 0 [Right]() = 0 [Sum_term_var](x1) = 0 [Term_app](x1, x2) = 1 + x1 + x2 [Term_pair](x1, x2) = 1 + x1 + x2 [Term_inl](x1) = x1 [Term_inr](x1) = x1 [Term_var](x1) = 0 [Id]() = 0 [Cons_usual](x1, x2, x3) = 1 + x2 + x3 [Cons_sum](x1, x2, x3) = 1 + x3 [Concat](x1, x2) = x1 + x1*x2 + 2*x1^2 + x2 The following symbols are considered usable {Term_sub, Frozen, Sum_sub, Concat} This order satisfies the following ordering constraints. [Term_sub(Term_sub(m, s), t)] = m + 3*m*s + 4*m^2 + s + m*t + m*s*t + 2*m^2*t + s*t + 8*m^2*s + 8*m^3 + 2*m^2*s^2 + 8*m^3*s + 2*m*s^2 + 8*m^4 + 2*s*m + 2*s^2*m + 4*s*m^2 + 2*s^2 + t >= m + m*s + m*s*t + 2*m*s^2 + m*t + 2*m^2 + s + s*t + 2*s^2 + t = [Term_sub(m, Concat(s, t))] [Term_sub(Case(m, xi, n), s)] = 3 + 5*m + 5*n + 2*s + m*s + n*s + 2*m^2 + 2*m*n + 2*n*m + 2*n^2 > 1 + m + m*s + 2*m^2 + n + n*s + 2*n^2 + 2*s = [Frozen(m, Sum_sub(xi, s), n, s)] [Term_sub(Term_app(m, n), s)] = 3 + 5*m + 5*n + 2*s + m*s + n*s + 2*m^2 + 2*m*n + 2*n*m + 2*n^2 > 1 + m + m*s + 2*m^2 + 2*s + n + n*s + 2*n^2 = [Term_app(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_pair(m, n), s)] = 3 + 5*m + 5*n + 2*s + m*s + n*s + 2*m^2 + 2*m*n + 2*n*m + 2*n^2 > 1 + m + m*s + 2*m^2 + 2*s + n + n*s + 2*n^2 = [Term_pair(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_inl(m), s)] = m + m*s + 2*m^2 + s >= m + m*s + 2*m^2 + s = [Term_inl(Term_sub(m, s))] [Term_sub(Term_inr(m), s)] = m + m*s + 2*m^2 + s >= m + m*s + 2*m^2 + s = [Term_inr(Term_sub(m, s))] [Term_sub(Term_var(x), Id())] = >= = [Term_var(x)] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 1 + m + s > m = [m] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 1 + m + s > s = [Term_sub(Term_var(x), s)] [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = 1 + s > s = [Term_sub(Term_var(x), s)] [Frozen(m, Sum_constant(Left()), n, s)] = 1 + m + m*s + 2*m^2 + n + n*s + 2*n^2 + 2*s > m + m*s + 2*m^2 + s = [Term_sub(m, s)] [Frozen(m, Sum_constant(Right()), n, s)] = 1 + m + m*s + 2*m^2 + n + n*s + 2*n^2 + 2*s > n + n*s + 2*n^2 + s = [Term_sub(n, s)] [Frozen(m, Sum_term_var(xi), n, s)] = 1 + m + m*s + 2*m^2 + n + n*s + 2*n^2 + 2*s >= 1 + m + m*s + 2*m^2 + 2*s + n + n*s + 2*n^2 = [Case(Term_sub(m, s), xi, Term_sub(n, s))] [Sum_sub(xi, Id())] = >= = [Sum_term_var(xi)] [Sum_sub(xi, Cons_usual(y, m, s))] = >= = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = >= = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = >= = [Sum_constant(k)] [Concat(Id(), s)] = s >= s = [s] [Concat(Cons_usual(x, m, s), t)] = 3 + 5*m + 5*s + 2*t + m*t + s*t + 2*m^2 + 2*m*s + 2*s*m + 2*s^2 > 1 + m + m*t + 2*m^2 + 2*t + s + s*t + 2*s^2 = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] [Concat(Cons_sum(xi, k, s), t)] = 3 + 5*s + 2*t + s*t + 2*s^2 > 1 + s + s*t + 2*s^2 + t = [Cons_sum(xi, k, Concat(s, t))] [Concat(Concat(s, t), u)] = s + 3*s*t + 4*s^2 + t + s*u + s*t*u + 2*s^2*u + t*u + 8*s^2*t + 8*s^3 + 2*s^2*t^2 + 8*s^3*t + 2*s*t^2 + 8*s^4 + 2*t*s + 2*t^2*s + 4*t*s^2 + 2*t^2 + u >= s + s*t + s*t*u + 2*s*t^2 + s*u + 2*s^2 + t + t*u + 2*t^2 + u = [Concat(s, Concat(t, u))] 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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Weak Trs: { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) , Concat(Id(), s) -> s , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) } 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 considered usable: Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, Uargs(Frozen) = {2}, Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, Uargs(Concat) = {2} TcT has computed the following constructor-restricted polynomial interpretation. [Term_sub](x1, x2) = x1 + x1*x2 + x1^2 + 2*x2 [Case](x1, x2, x3) = 2 + x1 + x3 [Frozen](x1, x2, x3, x4) = x1 + x1*x3 + x1*x4 + x1^2 + 2*x2 + 2*x2*x4 + x3 + x3*x4 + x3^2 [Sum_sub](x1, x2) = 2 [Sum_constant](x1) = 1 [Left]() = 0 [Right]() = 0 [Sum_term_var](x1) = 2 [Term_app](x1, x2) = 2 + x1 + x2 [Term_pair](x1, x2) = 2 + x1 + x2 [Term_inl](x1) = x1 [Term_inr](x1) = 2 + x1 [Term_var](x1) = 0 [Id]() = 0 [Cons_usual](x1, x2, x3) = 2 + x2 + x3 [Cons_sum](x1, x2, x3) = x3 [Concat](x1, x2) = x1 + x1*x2 + x1^2 + x2 The following symbols are considered usable {Term_sub, Frozen, Sum_sub, Concat} This order satisfies the following ordering constraints. [Term_sub(Term_sub(m, s), t)] = m + 3*m*s + 2*m^2 + 2*s + m*t + m*s*t + m^2*t + 2*s*t + 4*m^2*s + 2*m^3 + m^2*s^2 + 2*m^3*s + 2*m*s^2 + m^4 + 2*s*m + 2*s^2*m + 2*s*m^2 + 4*s^2 + 2*t >= m + m*s + m*s*t + m*s^2 + m*t + m^2 + 2*s + 2*s*t + 2*s^2 + 2*t = [Term_sub(m, Concat(s, t))] [Term_sub(Case(m, xi, n), s)] = 6 + 5*m + 5*n + 4*s + m*s + n*s + m^2 + m*n + n*m + n^2 > m + m*n + m*s + m^2 + 4 + 4*s + n + n*s + n^2 = [Frozen(m, Sum_sub(xi, s), n, s)] [Term_sub(Term_app(m, n), s)] = 6 + 5*m + 5*n + 4*s + m*s + n*s + m^2 + m*n + n*m + n^2 > 2 + m + m*s + m^2 + 4*s + n + n*s + n^2 = [Term_app(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_pair(m, n), s)] = 6 + 5*m + 5*n + 4*s + m*s + n*s + m^2 + m*n + n*m + n^2 > 2 + m + m*s + m^2 + 4*s + n + n*s + n^2 = [Term_pair(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_inl(m), s)] = m + m*s + m^2 + 2*s >= m + m*s + m^2 + 2*s = [Term_inl(Term_sub(m, s))] [Term_sub(Term_inr(m), s)] = 6 + 5*m + 4*s + m*s + m^2 > 2 + m + m*s + m^2 + 2*s = [Term_inr(Term_sub(m, s))] [Term_sub(Term_var(x), Id())] = >= = [Term_var(x)] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 4 + 2*m + 2*s > m = [m] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 4 + 2*m + 2*s > 2*s = [Term_sub(Term_var(x), s)] [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = 2*s >= 2*s = [Term_sub(Term_var(x), s)] [Frozen(m, Sum_constant(Left()), n, s)] = m + m*n + m*s + m^2 + 2 + 2*s + n + n*s + n^2 > m + m*s + m^2 + 2*s = [Term_sub(m, s)] [Frozen(m, Sum_constant(Right()), n, s)] = m + m*n + m*s + m^2 + 2 + 2*s + n + n*s + n^2 > n + n*s + n^2 + 2*s = [Term_sub(n, s)] [Frozen(m, Sum_term_var(xi), n, s)] = m + m*n + m*s + m^2 + 4 + 4*s + n + n*s + n^2 > 2 + m + m*s + m^2 + 4*s + n + n*s + n^2 = [Case(Term_sub(m, s), xi, Term_sub(n, s))] [Sum_sub(xi, Id())] = 2 >= 2 = [Sum_term_var(xi)] [Sum_sub(xi, Cons_usual(y, m, s))] = 2 >= 2 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 2 >= 2 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 2 > 1 = [Sum_constant(k)] [Concat(Id(), s)] = s >= s = [s] [Concat(Cons_usual(x, m, s), t)] = 6 + 5*m + 5*s + 3*t + m*t + s*t + m^2 + m*s + s*m + s^2 > 2 + m + m*t + m^2 + 3*t + s + s*t + s^2 = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] [Concat(Cons_sum(xi, k, s), t)] = s + s*t + s^2 + t >= s + s*t + s^2 + t = [Cons_sum(xi, k, Concat(s, t))] [Concat(Concat(s, t), u)] = s + 2*s*t + 2*s^2 + t + s*u + s*t*u + s^2*u + t*u + 3*s^2*t + 2*s^3 + s^2*t^2 + 2*s^3*t + s*t^2 + s^4 + t*s + t^2*s + t*s^2 + t^2 + u >= s + s*t + s*t*u + s*t^2 + s*u + s^2 + t + t*u + t^2 + u = [Concat(s, Concat(t, u))] 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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Weak Trs: { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) , Concat(Id(), s) -> s , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) } 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 considered usable: Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, Uargs(Frozen) = {2}, Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, Uargs(Concat) = {2} TcT has computed the following constructor-restricted polynomial interpretation. [Term_sub](x1, x2) = x1 + x1*x2 + 2*x1^2 + x2 [Case](x1, x2, x3) = 1 + x1 + x3 [Frozen](x1, x2, x3, x4) = x1 + x1*x4 + 2*x1^2 + x2 + x2*x4 + x3 + x3*x4 + 2*x3^2 [Sum_sub](x1, x2) = 2 [Sum_constant](x1) = 1 [Left]() = 0 [Right]() = 0 [Sum_term_var](x1) = 2 [Term_app](x1, x2) = 1 + x1 + x2 [Term_pair](x1, x2) = 1 + x1 + x2 [Term_inl](x1) = 1 + x1 [Term_inr](x1) = x1 [Term_var](x1) = 0 [Id]() = 0 [Cons_usual](x1, x2, x3) = 1 + x2 + x3 [Cons_sum](x1, x2, x3) = x3 [Concat](x1, x2) = x1 + x1*x2 + 2*x1^2 + x2 The following symbols are considered usable {Term_sub, Frozen, Sum_sub, Concat} This order satisfies the following ordering constraints. [Term_sub(Term_sub(m, s), t)] = m + 3*m*s + 4*m^2 + s + m*t + m*s*t + 2*m^2*t + s*t + 8*m^2*s + 8*m^3 + 2*m^2*s^2 + 8*m^3*s + 2*m*s^2 + 8*m^4 + 2*s*m + 2*s^2*m + 4*s*m^2 + 2*s^2 + t >= m + m*s + m*s*t + 2*m*s^2 + m*t + 2*m^2 + s + s*t + 2*s^2 + t = [Term_sub(m, Concat(s, t))] [Term_sub(Case(m, xi, n), s)] = 3 + 5*m + 5*n + 2*s + m*s + n*s + 2*m^2 + 2*m*n + 2*n*m + 2*n^2 > m + m*s + 2*m^2 + 2 + 2*s + n + n*s + 2*n^2 = [Frozen(m, Sum_sub(xi, s), n, s)] [Term_sub(Term_app(m, n), s)] = 3 + 5*m + 5*n + 2*s + m*s + n*s + 2*m^2 + 2*m*n + 2*n*m + 2*n^2 > 1 + m + m*s + 2*m^2 + 2*s + n + n*s + 2*n^2 = [Term_app(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_pair(m, n), s)] = 3 + 5*m + 5*n + 2*s + m*s + n*s + 2*m^2 + 2*m*n + 2*n*m + 2*n^2 > 1 + m + m*s + 2*m^2 + 2*s + n + n*s + 2*n^2 = [Term_pair(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_inl(m), s)] = 3 + 5*m + 2*s + m*s + 2*m^2 > 1 + m + m*s + 2*m^2 + s = [Term_inl(Term_sub(m, s))] [Term_sub(Term_inr(m), s)] = m + m*s + 2*m^2 + s >= m + m*s + 2*m^2 + s = [Term_inr(Term_sub(m, s))] [Term_sub(Term_var(x), Id())] = >= = [Term_var(x)] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 1 + m + s > m = [m] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 1 + m + s > s = [Term_sub(Term_var(x), s)] [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = s >= s = [Term_sub(Term_var(x), s)] [Frozen(m, Sum_constant(Left()), n, s)] = m + m*s + 2*m^2 + 1 + s + n + n*s + 2*n^2 > m + m*s + 2*m^2 + s = [Term_sub(m, s)] [Frozen(m, Sum_constant(Right()), n, s)] = m + m*s + 2*m^2 + 1 + s + n + n*s + 2*n^2 > n + n*s + 2*n^2 + s = [Term_sub(n, s)] [Frozen(m, Sum_term_var(xi), n, s)] = m + m*s + 2*m^2 + 2 + 2*s + n + n*s + 2*n^2 > 1 + m + m*s + 2*m^2 + 2*s + n + n*s + 2*n^2 = [Case(Term_sub(m, s), xi, Term_sub(n, s))] [Sum_sub(xi, Id())] = 2 >= 2 = [Sum_term_var(xi)] [Sum_sub(xi, Cons_usual(y, m, s))] = 2 >= 2 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 2 >= 2 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 2 > 1 = [Sum_constant(k)] [Concat(Id(), s)] = s >= s = [s] [Concat(Cons_usual(x, m, s), t)] = 3 + 5*m + 5*s + 2*t + m*t + s*t + 2*m^2 + 2*m*s + 2*s*m + 2*s^2 > 1 + m + m*t + 2*m^2 + 2*t + s + s*t + 2*s^2 = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] [Concat(Cons_sum(xi, k, s), t)] = s + s*t + 2*s^2 + t >= s + s*t + 2*s^2 + t = [Cons_sum(xi, k, Concat(s, t))] [Concat(Concat(s, t), u)] = s + 3*s*t + 4*s^2 + t + s*u + s*t*u + 2*s^2*u + t*u + 8*s^2*t + 8*s^3 + 2*s^2*t^2 + 8*s^3*t + 2*s*t^2 + 8*s^4 + 2*t*s + 2*t^2*s + 4*t*s^2 + 2*t^2 + u >= s + s*t + s*t*u + 2*s*t^2 + s*u + 2*s^2 + t + t*u + 2*t^2 + u = [Concat(s, Concat(t, u))] 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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Weak Trs: { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) , Concat(Id(), s) -> s , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } 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 considered usable: Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, Uargs(Frozen) = {2}, Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, Uargs(Concat) = {2} TcT has computed the following constructor-restricted polynomial interpretation. [Term_sub](x1, x2) = 1 + 2*x1 + x1*x2 + x2 [Case](x1, x2, x3) = 2 + x1 + x3 [Frozen](x1, x2, x3, x4) = 1 + 2*x1 + x1*x4 + 2*x2 + 2*x2^2 + 2*x3 + x3*x4 + 2*x4 [Sum_sub](x1, x2) = 1 [Sum_constant](x1) = 0 [Left]() = 0 [Right]() = 0 [Sum_term_var](x1) = 1 [Term_app](x1, x2) = 1 + x1 + x2 [Term_pair](x1, x2) = 1 + x1 + x2 [Term_inl](x1) = x1 [Term_inr](x1) = x1 [Term_var](x1) = 0 [Id]() = 0 [Cons_usual](x1, x2, x3) = 1 + x2 + x3 [Cons_sum](x1, x2, x3) = 2 + x3 [Concat](x1, x2) = 2 + 2*x1 + x1*x2 + x2 The following symbols are considered usable {Term_sub, Frozen, Sum_sub, Concat} This order satisfies the following ordering constraints. [Term_sub(Term_sub(m, s), t)] = 3 + 4*m + 2*m*s + 2*s + 2*t + 2*m*t + m*s*t + s*t >= 3 + 4*m + 2*m*s + m*s*t + m*t + 2*s + s*t + t = [Term_sub(m, Concat(s, t))] [Term_sub(Case(m, xi, n), s)] = 5 + 2*m + 2*n + 3*s + m*s + n*s >= 5 + 2*m + m*s + 2*n + n*s + 2*s = [Frozen(m, Sum_sub(xi, s), n, s)] [Term_sub(Term_app(m, n), s)] = 3 + 2*m + 2*n + 2*s + m*s + n*s >= 3 + 2*m + m*s + 2*s + 2*n + n*s = [Term_app(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_pair(m, n), s)] = 3 + 2*m + 2*n + 2*s + m*s + n*s >= 3 + 2*m + m*s + 2*s + 2*n + n*s = [Term_pair(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_inl(m), s)] = 1 + 2*m + m*s + s >= 1 + 2*m + m*s + s = [Term_inl(Term_sub(m, s))] [Term_sub(Term_inr(m), s)] = 1 + 2*m + m*s + s >= 1 + 2*m + m*s + s = [Term_inr(Term_sub(m, s))] [Term_sub(Term_var(x), Id())] = 1 > = [Term_var(x)] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s > m = [m] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s > 1 + s = [Term_sub(Term_var(x), s)] [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = 3 + s > 1 + s = [Term_sub(Term_var(x), s)] [Frozen(m, Sum_constant(Left()), n, s)] = 1 + 2*m + m*s + 2*n + n*s + 2*s >= 1 + 2*m + m*s + s = [Term_sub(m, s)] [Frozen(m, Sum_constant(Right()), n, s)] = 1 + 2*m + m*s + 2*n + n*s + 2*s >= 1 + 2*n + n*s + s = [Term_sub(n, s)] [Frozen(m, Sum_term_var(xi), n, s)] = 5 + 2*m + m*s + 2*n + n*s + 2*s > 4 + 2*m + m*s + 2*s + 2*n + n*s = [Case(Term_sub(m, s), xi, Term_sub(n, s))] [Sum_sub(xi, Id())] = 1 >= 1 = [Sum_term_var(xi)] [Sum_sub(xi, Cons_usual(y, m, s))] = 1 >= 1 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 >= 1 = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 > = [Sum_constant(k)] [Concat(Id(), s)] = 2 + s > s = [s] [Concat(Cons_usual(x, m, s), t)] = 4 + 2*m + 2*s + 2*t + m*t + s*t >= 4 + 2*m + m*t + 2*t + 2*s + s*t = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] [Concat(Cons_sum(xi, k, s), t)] = 6 + 2*s + 3*t + s*t > 4 + 2*s + s*t + t = [Cons_sum(xi, k, Concat(s, t))] [Concat(Concat(s, t), u)] = 6 + 4*s + 2*s*t + 2*t + 3*u + 2*s*u + s*t*u + t*u > 4 + 4*s + 2*s*t + s*t*u + s*u + 2*t + t*u + u = [Concat(s, Concat(t, u))] 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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) } Weak Trs: { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) , Concat(Id(), s) -> s , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'polynomial interpretation' to orient following rules strictly. Trs: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) } 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 considered usable: Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, Uargs(Frozen) = {2}, Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, Uargs(Concat) = {2} TcT has computed the following constructor-restricted polynomial interpretation. [Term_sub](x1, x2) = 1 + 2*x1 + x1*x2 + x2 [Case](x1, x2, x3) = 1 + x1 + x3 [Frozen](x1, x2, x3, x4) = 3 + 2*x1 + x1*x4 + x2 + 2*x3 + x3*x4 + 2*x4 [Sum_sub](x1, x2) = 0 [Sum_constant](x1) = 0 [Left]() = 0 [Right]() = 0 [Sum_term_var](x1) = 0 [Term_app](x1, x2) = 1 + x1 + x2 [Term_pair](x1, x2) = 1 + x1 + x2 [Term_inl](x1) = x1 [Term_inr](x1) = 1 + x1 [Term_var](x1) = 0 [Id]() = 0 [Cons_usual](x1, x2, x3) = 1 + x2 + x3 [Cons_sum](x1, x2, x3) = x3 [Concat](x1, x2) = 2*x1 + x1*x2 + x2 The following symbols are considered usable {Term_sub, Frozen, Sum_sub, Concat} This order satisfies the following ordering constraints. [Term_sub(Term_sub(m, s), t)] = 3 + 4*m + 2*m*s + 2*s + 2*t + 2*m*t + m*s*t + s*t > 1 + 2*m + 2*m*s + m*s*t + m*t + 2*s + s*t + t = [Term_sub(m, Concat(s, t))] [Term_sub(Case(m, xi, n), s)] = 3 + 2*m + 2*n + 2*s + m*s + n*s >= 3 + 2*m + m*s + 2*n + n*s + 2*s = [Frozen(m, Sum_sub(xi, s), n, s)] [Term_sub(Term_app(m, n), s)] = 3 + 2*m + 2*n + 2*s + m*s + n*s >= 3 + 2*m + m*s + 2*s + 2*n + n*s = [Term_app(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_pair(m, n), s)] = 3 + 2*m + 2*n + 2*s + m*s + n*s >= 3 + 2*m + m*s + 2*s + 2*n + n*s = [Term_pair(Term_sub(m, s), Term_sub(n, s))] [Term_sub(Term_inl(m), s)] = 1 + 2*m + m*s + s >= 1 + 2*m + m*s + s = [Term_inl(Term_sub(m, s))] [Term_sub(Term_inr(m), s)] = 3 + 2*m + 2*s + m*s > 2 + 2*m + m*s + s = [Term_inr(Term_sub(m, s))] [Term_sub(Term_var(x), Id())] = 1 > = [Term_var(x)] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s > m = [m] [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s > 1 + s = [Term_sub(Term_var(x), s)] [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = 1 + s >= 1 + s = [Term_sub(Term_var(x), s)] [Frozen(m, Sum_constant(Left()), n, s)] = 3 + 2*m + m*s + 2*n + n*s + 2*s > 1 + 2*m + m*s + s = [Term_sub(m, s)] [Frozen(m, Sum_constant(Right()), n, s)] = 3 + 2*m + m*s + 2*n + n*s + 2*s > 1 + 2*n + n*s + s = [Term_sub(n, s)] [Frozen(m, Sum_term_var(xi), n, s)] = 3 + 2*m + m*s + 2*n + n*s + 2*s >= 3 + 2*m + m*s + 2*s + 2*n + n*s = [Case(Term_sub(m, s), xi, Term_sub(n, s))] [Sum_sub(xi, Id())] = >= = [Sum_term_var(xi)] [Sum_sub(xi, Cons_usual(y, m, s))] = >= = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = >= = [Sum_sub(xi, s)] [Sum_sub(xi, Cons_sum(psi, k, s))] = >= = [Sum_constant(k)] [Concat(Id(), s)] = s >= s = [s] [Concat(Cons_usual(x, m, s), t)] = 2 + 2*m + 2*s + 2*t + m*t + s*t >= 2 + 2*m + m*t + 2*t + 2*s + s*t = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] [Concat(Cons_sum(xi, k, s), t)] = 2*s + s*t + t >= 2*s + s*t + t = [Cons_sum(xi, k, Concat(s, t))] [Concat(Concat(s, t), u)] = 4*s + 2*s*t + 2*t + 2*s*u + s*t*u + t*u + u >= 2*s + 2*s*t + s*t*u + s*u + 2*t + t*u + u = [Concat(s, Concat(t, u))] 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: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) , Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) , Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)) , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) , Term_sub(Term_var(x), Id()) -> Term_var(x) , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s) , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s) , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) , Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)) , Sum_sub(xi, Id()) -> Sum_term_var(xi) , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) , Concat(Id(), s) -> s , Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)) , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))