YES(O(1),O(n^2)) 877.91/297.40 YES(O(1),O(n^2)) 877.91/297.40 877.91/297.40 We are left with following problem, upon which TcT provides the 877.91/297.40 certificate YES(O(1),O(n^2)). 877.91/297.40 877.91/297.40 Strict Trs: 877.91/297.40 { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) 877.91/297.40 , Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) 877.91/297.40 , Term_sub(Term_app(m, n), s) -> 877.91/297.40 Term_app(Term_sub(m, s), Term_sub(n, s)) 877.91/297.40 , Term_sub(Term_pair(m, n), s) -> 877.91/297.40 Term_pair(Term_sub(m, s), Term_sub(n, s)) 877.91/297.40 , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) 877.91/297.40 , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) 877.91/297.40 , Term_sub(Term_var(x), Id()) -> Term_var(x) 877.91/297.40 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m 877.91/297.40 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> 877.91/297.40 Term_sub(Term_var(x), s) 877.91/297.40 , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> 877.91/297.40 Term_sub(Term_var(x), s) 877.91/297.40 , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) 877.91/297.40 , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) 877.91/297.40 , Frozen(m, Sum_term_var(xi), n, s) -> 877.91/297.40 Case(Term_sub(m, s), xi, Term_sub(n, s)) 877.91/297.40 , Sum_sub(xi, Id()) -> Sum_term_var(xi) 877.91/297.40 , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) 877.91/297.40 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) 877.91/297.40 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) 877.91/297.40 , Concat(Id(), s) -> s 877.91/297.40 , Concat(Cons_usual(x, m, s), t) -> 877.91/297.40 Cons_usual(x, Term_sub(m, t), Concat(s, t)) 877.91/297.40 , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) 877.91/297.40 , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } 877.91/297.40 Obligation: 877.91/297.40 runtime complexity 877.91/297.40 Answer: 877.91/297.40 YES(O(1),O(n^2)) 877.91/297.40 877.91/297.40 We use the processor 'polynomial interpretation' to orient 877.91/297.40 following rules strictly. 877.91/297.40 877.91/297.40 Trs: 877.91/297.40 { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) 877.91/297.40 , Term_sub(Term_app(m, n), s) -> 877.91/297.40 Term_app(Term_sub(m, s), Term_sub(n, s)) 877.91/297.40 , Term_sub(Term_var(x), Id()) -> Term_var(x) 877.91/297.40 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m 877.91/297.40 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> 877.91/297.40 Term_sub(Term_var(x), s) 877.91/297.40 , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> 877.91/297.40 Term_sub(Term_var(x), s) 877.91/297.40 , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) 877.91/297.40 , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) 877.91/297.40 , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) 877.91/297.40 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) 877.91/297.40 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) 877.91/297.40 , Concat(Id(), s) -> s 877.91/297.40 , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) } 877.91/297.40 877.91/297.40 The induced complexity on above rules (modulo remaining rules) is 877.91/297.40 YES(?,O(n^2)) . These rules are moved into the corresponding weak 877.91/297.40 component(s). 877.91/297.40 877.91/297.40 Sub-proof: 877.91/297.40 ---------- 877.91/297.40 We consider the following typing: 877.91/297.40 877.91/297.40 Term_sub :: (g,b) -> g 877.91/297.40 Case :: (g,c,g) -> g 877.91/297.40 Frozen :: (g,a,g,b) -> g 877.91/297.40 Sum_sub :: (c,b) -> a 877.91/297.40 Sum_constant :: d -> a 877.91/297.40 Left :: d 877.91/297.40 Right :: d 877.91/297.40 Sum_term_var :: c -> a 877.91/297.40 Term_app :: (g,g) -> g 877.91/297.40 Term_pair :: (g,g) -> g 877.91/297.40 Term_inl :: g -> g 877.91/297.40 Term_inr :: g -> g 877.91/297.40 Term_var :: e -> g 877.91/297.40 Id :: b 877.91/297.40 Cons_usual :: (f,g,b) -> b 877.91/297.40 Cons_sum :: (h,d,b) -> b 877.91/297.40 Concat :: (b,b) -> b 877.91/297.40 877.91/297.40 The following argument positions are considered usable: 877.91/297.40 877.91/297.40 Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, 877.91/297.40 Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2}, 877.91/297.40 Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, 877.91/297.40 Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, 877.91/297.40 Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, 877.91/297.40 Uargs(Concat) = {2} 877.91/297.40 877.91/297.40 TcT has computed the following constructor-restricted 877.91/297.40 typedpolynomial interpretation. 877.91/297.40 877.91/297.40 [Term_sub](x1, x2) = 1 + 2*x1 + x1*x2 + x2 877.91/297.40 877.91/297.40 [Case](x1, x2, x3) = 2 + x1 + x3 877.91/297.40 877.91/297.40 [Frozen](x1, x2, x3, x4) = 2 + 2*x1 + x1*x4 + x2 + 2*x3 + x3*x4 + 2*x4 877.91/297.40 877.91/297.40 [Sum_sub](x1, x2) = 2 + x2 877.91/297.40 877.91/297.40 [Sum_constant](x1) = 0 877.91/297.40 877.91/297.40 [Left]() = 0 877.91/297.40 877.91/297.40 [Right]() = 0 877.91/297.40 877.91/297.40 [Sum_term_var](x1) = 2 877.91/297.40 877.91/297.40 [Term_app](x1, x2) = 2 + x1 + x2 877.91/297.40 877.91/297.40 [Term_pair](x1, x2) = 1 + x1 + x2 877.91/297.40 877.91/297.40 [Term_inl](x1) = x1 877.91/297.40 877.91/297.40 [Term_inr](x1) = x1 877.91/297.40 877.91/297.40 [Term_var](x1) = 0 877.91/297.40 877.91/297.40 [Id]() = 0 877.91/297.40 877.91/297.40 [Cons_usual](x1, x2, x3) = 1 + x2 + x3 877.91/297.40 877.91/297.40 [Cons_sum](x1, x2, x3) = 2 + x3 877.91/297.40 877.91/297.40 [Concat](x1, x2) = 2 + 2*x1 + x1*x2 + 2*x2 877.91/297.40 877.91/297.40 877.91/297.40 This order satisfies the following ordering constraints. 877.91/297.40 877.91/297.40 [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 877.91/297.40 >= 3 + 4*m + 2*m*s + m*s*t + 2*m*t + 2*s + s*t + 2*t 877.91/297.40 = [Term_sub(m, Concat(s, t))] 877.91/297.40 877.91/297.40 [Term_sub(Case(m, xi, n), s)] = 5 + 2*m + 2*n + 3*s + m*s + n*s 877.91/297.40 > 4 + 2*m + m*s + 3*s + 2*n + n*s 877.91/297.40 = [Frozen(m, Sum_sub(xi, s), n, s)] 877.91/297.40 877.91/297.40 [Term_sub(Term_app(m, n), s)] = 5 + 2*m + 2*n + 3*s + m*s + n*s 877.91/297.40 > 4 + 2*m + m*s + 2*s + 2*n + n*s 877.91/297.40 = [Term_app(Term_sub(m, s), Term_sub(n, s))] 877.91/297.40 877.91/297.40 [Term_sub(Term_pair(m, n), s)] = 3 + 2*m + 2*n + 2*s + m*s + n*s 877.91/297.40 >= 3 + 2*m + m*s + 2*s + 2*n + n*s 877.91/297.40 = [Term_pair(Term_sub(m, s), Term_sub(n, s))] 877.91/297.40 877.91/297.40 [Term_sub(Term_inl(m), s)] = 1 + 2*m + m*s + s 877.91/297.40 >= 1 + 2*m + m*s + s 877.91/297.40 = [Term_inl(Term_sub(m, s))] 877.91/297.40 877.91/297.40 [Term_sub(Term_inr(m), s)] = 1 + 2*m + m*s + s 877.91/297.40 >= 1 + 2*m + m*s + s 877.91/297.40 = [Term_inr(Term_sub(m, s))] 877.91/297.40 877.91/297.40 [Term_sub(Term_var(x), Id())] = 1 877.91/297.40 > 877.91/297.40 = [Term_var(x)] 877.91/297.40 877.91/297.40 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s 877.91/297.40 > m 877.91/297.40 = [m] 877.91/297.40 877.91/297.40 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s 877.91/297.40 > 1 + s 877.91/297.40 = [Term_sub(Term_var(x), s)] 877.91/297.40 877.91/297.40 [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = 3 + s 877.91/297.40 > 1 + s 877.91/297.40 = [Term_sub(Term_var(x), s)] 877.91/297.40 877.91/297.40 [Frozen(m, Sum_constant(Left()), n, s)] = 2 + 2*m + m*s + 2*n + n*s + 2*s 877.91/297.40 > 1 + 2*m + m*s + s 877.91/297.40 = [Term_sub(m, s)] 877.91/297.40 877.91/297.40 [Frozen(m, Sum_constant(Right()), n, s)] = 2 + 2*m + m*s + 2*n + n*s + 2*s 877.91/297.40 > 1 + 2*n + n*s + s 877.91/297.40 = [Term_sub(n, s)] 877.91/297.40 877.91/297.40 [Frozen(m, Sum_term_var(xi), n, s)] = 4 + 2*m + m*s + 2*n + n*s + 2*s 877.91/297.40 >= 4 + 2*m + m*s + 2*s + 2*n + n*s 877.91/297.40 = [Case(Term_sub(m, s), xi, Term_sub(n, s))] 877.91/297.40 877.91/297.40 [Sum_sub(xi, Id())] = 2 877.91/297.40 >= 2 877.91/297.40 = [Sum_term_var(xi)] 877.91/297.40 877.91/297.40 [Sum_sub(xi, Cons_usual(y, m, s))] = 3 + m + s 877.91/297.40 > 2 + s 877.91/297.40 = [Sum_sub(xi, s)] 877.91/297.40 877.91/297.40 [Sum_sub(xi, Cons_sum(psi, k, s))] = 4 + s 877.91/297.40 > 2 + s 877.91/297.40 = [Sum_sub(xi, s)] 877.91/297.40 877.91/297.40 [Sum_sub(xi, Cons_sum(psi, k, s))] = 4 + s 877.91/297.40 > 877.91/297.40 = [Sum_constant(k)] 877.91/297.40 877.91/297.40 [Concat(Id(), s)] = 2 + 2*s 877.91/297.40 > s 877.91/297.40 = [s] 877.91/297.40 877.91/297.40 [Concat(Cons_usual(x, m, s), t)] = 4 + 2*m + 2*s + 3*t + m*t + s*t 877.91/297.40 >= 4 + 2*m + m*t + 3*t + 2*s + s*t 877.91/297.40 = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] 877.91/297.40 877.91/297.40 [Concat(Cons_sum(xi, k, s), t)] = 6 + 2*s + 4*t + s*t 877.91/297.40 > 4 + 2*s + s*t + 2*t 877.91/297.40 = [Cons_sum(xi, k, Concat(s, t))] 877.91/297.40 877.91/297.40 [Concat(Concat(s, t), u)] = 6 + 4*s + 2*s*t + 4*t + 4*u + 2*s*u + s*t*u + 2*t*u 877.91/297.40 >= 6 + 4*s + 2*s*t + s*t*u + 2*s*u + 4*t + 2*t*u + 4*u 877.91/297.40 = [Concat(s, Concat(t, u))] 877.91/297.40 877.91/297.40 877.91/297.40 We return to the main proof. 877.91/297.40 877.91/297.40 We are left with following problem, upon which TcT provides the 877.91/297.40 certificate YES(O(1),O(n^2)). 877.91/297.40 877.91/297.40 Strict Trs: 877.91/297.40 { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) 877.91/297.40 , Term_sub(Term_pair(m, n), s) -> 877.91/297.40 Term_pair(Term_sub(m, s), Term_sub(n, s)) 877.91/297.40 , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) 877.91/297.40 , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) 877.91/297.40 , Frozen(m, Sum_term_var(xi), n, s) -> 877.91/297.40 Case(Term_sub(m, s), xi, Term_sub(n, s)) 877.91/297.40 , Sum_sub(xi, Id()) -> Sum_term_var(xi) 877.91/297.40 , Concat(Cons_usual(x, m, s), t) -> 877.91/297.40 Cons_usual(x, Term_sub(m, t), Concat(s, t)) 877.91/297.40 , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } 877.91/297.40 Weak Trs: 877.91/297.40 { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) 877.91/297.40 , Term_sub(Term_app(m, n), s) -> 877.91/297.40 Term_app(Term_sub(m, s), Term_sub(n, s)) 877.91/297.40 , Term_sub(Term_var(x), Id()) -> Term_var(x) 877.91/297.40 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m 877.91/297.40 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> 877.91/297.40 Term_sub(Term_var(x), s) 877.91/297.40 , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> 877.91/297.40 Term_sub(Term_var(x), s) 877.91/297.40 , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) 877.91/297.40 , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) 877.91/297.40 , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) 877.91/297.40 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) 877.91/297.40 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) 877.91/297.40 , Concat(Id(), s) -> s 877.91/297.40 , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) } 877.91/297.40 Obligation: 877.91/297.40 runtime complexity 877.91/297.40 Answer: 877.91/297.40 YES(O(1),O(n^2)) 877.91/297.40 877.91/297.40 We use the processor 'polynomial interpretation' to orient 877.91/297.40 following rules strictly. 877.91/297.40 877.91/297.40 Trs: 877.91/297.40 { Term_sub(Term_pair(m, n), s) -> 877.91/297.40 Term_pair(Term_sub(m, s), Term_sub(n, s)) 877.91/297.40 , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) } 877.91/297.40 877.91/297.40 The induced complexity on above rules (modulo remaining rules) is 877.91/297.40 YES(?,O(n^2)) . These rules are moved into the corresponding weak 877.91/297.40 component(s). 877.91/297.40 877.91/297.40 Sub-proof: 877.91/297.40 ---------- 877.91/297.40 We consider the following typing: 877.91/297.40 877.91/297.40 Term_sub :: (g,b) -> g 877.91/297.40 Case :: (g,c,g) -> g 877.91/297.40 Frozen :: (g,a,g,b) -> g 877.91/297.40 Sum_sub :: (c,b) -> a 877.91/297.40 Sum_constant :: d -> a 877.91/297.40 Left :: d 877.91/297.40 Right :: d 877.91/297.40 Sum_term_var :: c -> a 877.91/297.40 Term_app :: (g,g) -> g 877.91/297.40 Term_pair :: (g,g) -> g 877.91/297.40 Term_inl :: g -> g 877.91/297.40 Term_inr :: g -> g 877.91/297.40 Term_var :: e -> g 877.91/297.40 Id :: b 877.91/297.40 Cons_usual :: (f,g,b) -> b 877.91/297.40 Cons_sum :: (h,d,b) -> b 877.91/297.40 Concat :: (b,b) -> b 877.91/297.40 877.91/297.40 The following argument positions are considered usable: 877.91/297.40 877.91/297.40 Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, 877.91/297.40 Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2}, 877.91/297.40 Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, 877.91/297.40 Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, 877.91/297.40 Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, 877.91/297.40 Uargs(Concat) = {2} 877.91/297.40 877.91/297.40 TcT has computed the following constructor-restricted 877.91/297.40 typedpolynomial interpretation. 877.91/297.40 877.91/297.40 [Term_sub](x1, x2) = 1 + 2*x1 + x1*x2 + x2 877.91/297.40 877.91/297.40 [Case](x1, x2, x3) = 2 + x1 + x3 877.91/297.40 877.91/297.40 [Frozen](x1, x2, x3, x4) = 2 + 2*x1 + x1*x4 + x2 + 2*x3 + x3*x4 + 2*x4 877.91/297.40 877.91/297.40 [Sum_sub](x1, x2) = 2 + x2 877.91/297.40 877.91/297.40 [Sum_constant](x1) = 0 877.91/297.40 877.91/297.40 [Left]() = 0 877.91/297.40 877.91/297.40 [Right]() = 0 877.91/297.40 877.91/297.40 [Sum_term_var](x1) = 2 877.91/297.40 877.91/297.40 [Term_app](x1, x2) = 2 + x1 + x2 877.91/297.40 877.91/297.40 [Term_pair](x1, x2) = 2 + x1 + x2 877.91/297.40 877.91/297.40 [Term_inl](x1) = x1 877.91/297.40 877.91/297.40 [Term_inr](x1) = 2 + x1 877.91/297.40 877.91/297.40 [Term_var](x1) = 0 877.91/297.40 877.91/297.40 [Id]() = 0 877.91/297.40 877.91/297.40 [Cons_usual](x1, x2, x3) = 1 + x2 + x3 877.91/297.40 877.91/297.40 [Cons_sum](x1, x2, x3) = x3 877.91/297.40 877.91/297.40 [Concat](x1, x2) = 2 + 2*x1 + x1*x2 + 2*x2 877.91/297.40 877.91/297.40 877.91/297.40 This order satisfies the following ordering constraints. 877.91/297.40 877.91/297.40 [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 877.91/297.40 >= 3 + 4*m + 2*m*s + m*s*t + 2*m*t + 2*s + s*t + 2*t 877.91/297.40 = [Term_sub(m, Concat(s, t))] 877.91/297.40 877.91/297.40 [Term_sub(Case(m, xi, n), s)] = 5 + 2*m + 2*n + 3*s + m*s + n*s 877.91/297.40 > 4 + 2*m + m*s + 3*s + 2*n + n*s 877.91/297.40 = [Frozen(m, Sum_sub(xi, s), n, s)] 877.91/297.40 877.91/297.40 [Term_sub(Term_app(m, n), s)] = 5 + 2*m + 2*n + 3*s + m*s + n*s 877.91/297.40 > 4 + 2*m + m*s + 2*s + 2*n + n*s 877.91/297.40 = [Term_app(Term_sub(m, s), Term_sub(n, s))] 877.91/297.40 877.91/297.40 [Term_sub(Term_pair(m, n), s)] = 5 + 2*m + 2*n + 3*s + m*s + n*s 877.91/297.40 > 4 + 2*m + m*s + 2*s + 2*n + n*s 877.91/297.40 = [Term_pair(Term_sub(m, s), Term_sub(n, s))] 877.91/297.40 877.91/297.40 [Term_sub(Term_inl(m), s)] = 1 + 2*m + m*s + s 877.91/297.40 >= 1 + 2*m + m*s + s 877.91/297.40 = [Term_inl(Term_sub(m, s))] 877.91/297.40 877.91/297.40 [Term_sub(Term_inr(m), s)] = 5 + 2*m + 3*s + m*s 877.91/297.40 > 3 + 2*m + m*s + s 877.91/297.40 = [Term_inr(Term_sub(m, s))] 877.91/297.40 877.91/297.40 [Term_sub(Term_var(x), Id())] = 1 877.91/297.40 > 877.91/297.40 = [Term_var(x)] 877.91/297.40 877.91/297.40 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s 877.91/297.40 > m 877.91/297.40 = [m] 877.91/297.40 877.91/297.40 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s 877.91/297.40 > 1 + s 877.91/297.40 = [Term_sub(Term_var(x), s)] 877.91/297.40 877.91/297.40 [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = 1 + s 877.91/297.40 >= 1 + s 877.91/297.40 = [Term_sub(Term_var(x), s)] 877.91/297.40 877.91/297.40 [Frozen(m, Sum_constant(Left()), n, s)] = 2 + 2*m + m*s + 2*n + n*s + 2*s 877.91/297.40 > 1 + 2*m + m*s + s 877.91/297.40 = [Term_sub(m, s)] 877.91/297.40 877.91/297.40 [Frozen(m, Sum_constant(Right()), n, s)] = 2 + 2*m + m*s + 2*n + n*s + 2*s 877.91/297.40 > 1 + 2*n + n*s + s 877.91/297.40 = [Term_sub(n, s)] 877.91/297.40 877.91/297.40 [Frozen(m, Sum_term_var(xi), n, s)] = 4 + 2*m + m*s + 2*n + n*s + 2*s 877.91/297.40 >= 4 + 2*m + m*s + 2*s + 2*n + n*s 877.91/297.40 = [Case(Term_sub(m, s), xi, Term_sub(n, s))] 877.91/297.40 877.91/297.40 [Sum_sub(xi, Id())] = 2 877.91/297.40 >= 2 877.91/297.40 = [Sum_term_var(xi)] 877.91/297.40 877.91/297.40 [Sum_sub(xi, Cons_usual(y, m, s))] = 3 + m + s 877.91/297.40 > 2 + s 877.91/297.40 = [Sum_sub(xi, s)] 877.91/297.40 877.91/297.40 [Sum_sub(xi, Cons_sum(psi, k, s))] = 2 + s 877.91/297.40 >= 2 + s 877.91/297.40 = [Sum_sub(xi, s)] 877.91/297.40 877.91/297.40 [Sum_sub(xi, Cons_sum(psi, k, s))] = 2 + s 877.91/297.40 > 877.91/297.40 = [Sum_constant(k)] 877.91/297.40 877.91/297.40 [Concat(Id(), s)] = 2 + 2*s 877.91/297.40 > s 877.91/297.40 = [s] 877.91/297.40 877.91/297.40 [Concat(Cons_usual(x, m, s), t)] = 4 + 2*m + 2*s + 3*t + m*t + s*t 877.91/297.40 >= 4 + 2*m + m*t + 3*t + 2*s + s*t 877.91/297.40 = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] 877.91/297.40 877.91/297.40 [Concat(Cons_sum(xi, k, s), t)] = 2 + 2*s + s*t + 2*t 877.91/297.40 >= 2 + 2*s + s*t + 2*t 877.91/297.40 = [Cons_sum(xi, k, Concat(s, t))] 877.91/297.40 877.91/297.40 [Concat(Concat(s, t), u)] = 6 + 4*s + 2*s*t + 4*t + 4*u + 2*s*u + s*t*u + 2*t*u 877.91/297.40 >= 6 + 4*s + 2*s*t + s*t*u + 2*s*u + 4*t + 2*t*u + 4*u 877.91/297.40 = [Concat(s, Concat(t, u))] 877.91/297.40 877.91/297.40 877.91/297.40 We return to the main proof. 877.91/297.40 877.91/297.40 We are left with following problem, upon which TcT provides the 877.91/297.40 certificate YES(O(1),O(n^2)). 877.91/297.40 877.91/297.40 Strict Trs: 877.91/297.40 { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) 877.91/297.40 , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) 877.91/297.40 , Frozen(m, Sum_term_var(xi), n, s) -> 877.91/297.40 Case(Term_sub(m, s), xi, Term_sub(n, s)) 877.91/297.40 , Sum_sub(xi, Id()) -> Sum_term_var(xi) 877.91/297.40 , Concat(Cons_usual(x, m, s), t) -> 877.91/297.40 Cons_usual(x, Term_sub(m, t), Concat(s, t)) 877.91/297.40 , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } 877.91/297.40 Weak Trs: 877.91/297.40 { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) 877.91/297.40 , Term_sub(Term_app(m, n), s) -> 877.91/297.40 Term_app(Term_sub(m, s), Term_sub(n, s)) 877.91/297.40 , Term_sub(Term_pair(m, n), s) -> 877.91/297.40 Term_pair(Term_sub(m, s), Term_sub(n, s)) 877.91/297.40 , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) 877.91/297.40 , Term_sub(Term_var(x), Id()) -> Term_var(x) 877.91/297.40 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m 877.91/297.40 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> 877.91/297.40 Term_sub(Term_var(x), s) 877.91/297.40 , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> 877.91/297.40 Term_sub(Term_var(x), s) 877.91/297.40 , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) 877.91/297.40 , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) 877.91/297.40 , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) 877.91/297.40 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) 877.91/297.40 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) 877.91/297.40 , Concat(Id(), s) -> s 877.91/297.40 , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) } 877.91/297.40 Obligation: 877.91/297.40 runtime complexity 877.91/297.40 Answer: 877.91/297.40 YES(O(1),O(n^2)) 877.91/297.40 877.91/297.40 We use the processor 'polynomial interpretation' to orient 877.91/297.40 following rules strictly. 877.91/297.40 877.91/297.40 Trs: { Sum_sub(xi, Id()) -> Sum_term_var(xi) } 877.91/297.40 877.91/297.40 The induced complexity on above rules (modulo remaining rules) is 877.91/297.40 YES(?,O(n^2)) . These rules are moved into the corresponding weak 877.91/297.40 component(s). 877.91/297.40 877.91/297.40 Sub-proof: 877.91/297.40 ---------- 877.91/297.40 We consider the following typing: 877.91/297.40 877.91/297.40 Term_sub :: (g,b) -> g 877.91/297.40 Case :: (g,c,g) -> g 877.91/297.40 Frozen :: (g,a,g,b) -> g 877.91/297.40 Sum_sub :: (c,b) -> a 877.91/297.40 Sum_constant :: d -> a 877.91/297.40 Left :: d 877.91/297.40 Right :: d 877.91/297.40 Sum_term_var :: c -> a 877.91/297.40 Term_app :: (g,g) -> g 877.91/297.40 Term_pair :: (g,g) -> g 877.91/297.40 Term_inl :: g -> g 877.91/297.40 Term_inr :: g -> g 877.91/297.40 Term_var :: e -> g 877.91/297.40 Id :: b 877.91/297.40 Cons_usual :: (f,g,b) -> b 877.91/297.40 Cons_sum :: (h,d,b) -> b 877.91/297.40 Concat :: (b,b) -> b 877.91/297.40 877.91/297.40 The following argument positions are considered usable: 877.91/297.40 877.91/297.40 Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, 877.91/297.40 Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2}, 877.91/297.40 Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, 877.91/297.40 Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, 877.91/297.40 Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, 877.91/297.40 Uargs(Concat) = {2} 877.91/297.40 877.91/297.40 TcT has computed the following constructor-restricted 877.91/297.40 typedpolynomial interpretation. 877.91/297.40 877.91/297.40 [Term_sub](x1, x2) = x1 + x1*x2 + x2 877.91/297.40 877.91/297.40 [Case](x1, x2, x3) = 2 + x1 + x3 877.91/297.40 877.91/297.40 [Frozen](x1, x2, x3, x4) = 2 + x1 + x1*x4 + x2 + x3 + x3*x4 + 2*x4 877.91/297.40 877.91/297.40 [Sum_sub](x1, x2) = x2 877.91/297.40 877.91/297.40 [Sum_constant](x1) = 0 877.91/297.40 877.91/297.40 [Left]() = 0 877.91/297.40 877.91/297.40 [Right]() = 0 877.91/297.40 877.91/297.40 [Sum_term_var](x1) = 0 877.91/297.40 877.91/297.40 [Term_app](x1, x2) = 1 + x1 + x2 877.91/297.40 877.91/297.40 [Term_pair](x1, x2) = 1 + x1 + x2 877.91/297.40 877.91/297.40 [Term_inl](x1) = x1 877.91/297.40 877.91/297.40 [Term_inr](x1) = x1 877.91/297.40 877.91/297.40 [Term_var](x1) = 0 877.91/297.40 877.91/297.40 [Id]() = 1 877.91/297.40 877.91/297.40 [Cons_usual](x1, x2, x3) = 2 + x2 + x3 877.91/297.40 877.91/297.40 [Cons_sum](x1, x2, x3) = x3 877.91/297.40 877.91/297.40 [Concat](x1, x2) = x1 + x1*x2 + x2 877.91/297.40 877.91/297.40 877.91/297.40 This order satisfies the following ordering constraints. 877.91/297.40 877.91/297.40 [Term_sub(Term_sub(m, s), t)] = m + m*s + s + m*t + m*s*t + s*t + t 877.91/297.40 >= m + m*s + m*s*t + m*t + s + s*t + t 877.91/297.40 = [Term_sub(m, Concat(s, t))] 877.91/297.40 877.91/297.40 [Term_sub(Case(m, xi, n), s)] = 2 + m + n + 3*s + m*s + n*s 877.91/297.40 >= 2 + m + m*s + 3*s + n + n*s 877.91/297.40 = [Frozen(m, Sum_sub(xi, s), n, s)] 877.91/297.40 877.91/297.40 [Term_sub(Term_app(m, n), s)] = 1 + m + n + 2*s + m*s + n*s 877.91/297.40 >= 1 + m + m*s + 2*s + n + n*s 877.91/297.40 = [Term_app(Term_sub(m, s), Term_sub(n, s))] 877.91/297.40 877.91/297.40 [Term_sub(Term_pair(m, n), s)] = 1 + m + n + 2*s + m*s + n*s 877.91/297.40 >= 1 + m + m*s + 2*s + n + n*s 877.91/297.40 = [Term_pair(Term_sub(m, s), Term_sub(n, s))] 877.91/297.40 877.91/297.40 [Term_sub(Term_inl(m), s)] = m + m*s + s 877.91/297.40 >= m + m*s + s 877.91/297.40 = [Term_inl(Term_sub(m, s))] 877.91/297.40 877.91/297.40 [Term_sub(Term_inr(m), s)] = m + m*s + s 877.91/297.40 >= m + m*s + s 877.91/297.40 = [Term_inr(Term_sub(m, s))] 877.91/297.40 877.91/297.40 [Term_sub(Term_var(x), Id())] = 1 877.91/297.40 > 877.91/297.40 = [Term_var(x)] 877.91/297.40 877.91/297.40 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s 877.91/297.40 > m 877.91/297.40 = [m] 877.91/297.40 877.91/297.40 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s 877.91/297.40 > s 877.91/297.40 = [Term_sub(Term_var(x), s)] 877.91/297.40 877.91/297.40 [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = s 877.91/297.40 >= s 877.91/297.40 = [Term_sub(Term_var(x), s)] 877.91/297.40 877.91/297.40 [Frozen(m, Sum_constant(Left()), n, s)] = 2 + m + m*s + n + n*s + 2*s 877.91/297.40 > m + m*s + s 877.91/297.40 = [Term_sub(m, s)] 877.91/297.40 877.91/297.40 [Frozen(m, Sum_constant(Right()), n, s)] = 2 + m + m*s + n + n*s + 2*s 877.91/297.40 > n + n*s + s 877.91/297.40 = [Term_sub(n, s)] 877.91/297.40 877.91/297.40 [Frozen(m, Sum_term_var(xi), n, s)] = 2 + m + m*s + n + n*s + 2*s 877.91/297.40 >= 2 + m + m*s + 2*s + n + n*s 877.91/297.40 = [Case(Term_sub(m, s), xi, Term_sub(n, s))] 877.91/297.40 877.91/297.40 [Sum_sub(xi, Id())] = 1 877.91/297.40 > 877.91/297.40 = [Sum_term_var(xi)] 877.91/297.40 877.91/297.40 [Sum_sub(xi, Cons_usual(y, m, s))] = 2 + m + s 877.91/297.40 > s 877.91/297.40 = [Sum_sub(xi, s)] 877.91/297.40 877.91/297.40 [Sum_sub(xi, Cons_sum(psi, k, s))] = s 877.91/297.40 >= s 877.91/297.40 = [Sum_sub(xi, s)] 877.91/297.40 877.91/297.40 [Sum_sub(xi, Cons_sum(psi, k, s))] = s 877.91/297.40 >= 877.91/297.40 = [Sum_constant(k)] 877.91/297.41 877.91/297.41 [Concat(Id(), s)] = 1 + 2*s 877.91/297.41 > s 877.91/297.41 = [s] 877.91/297.41 877.91/297.41 [Concat(Cons_usual(x, m, s), t)] = 2 + m + s + 3*t + m*t + s*t 877.91/297.41 >= 2 + m + m*t + 2*t + s + s*t 877.91/297.41 = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] 877.91/297.41 877.91/297.41 [Concat(Cons_sum(xi, k, s), t)] = s + s*t + t 877.91/297.41 >= s + s*t + t 877.91/297.41 = [Cons_sum(xi, k, Concat(s, t))] 877.91/297.41 877.91/297.41 [Concat(Concat(s, t), u)] = s + s*t + t + s*u + s*t*u + t*u + u 877.91/297.41 >= s + s*t + s*t*u + s*u + t + t*u + u 877.91/297.41 = [Concat(s, Concat(t, u))] 877.91/297.41 877.91/297.41 877.91/297.41 We return to the main proof. 877.91/297.41 877.91/297.41 We are left with following problem, upon which TcT provides the 877.91/297.41 certificate YES(O(1),O(n^2)). 877.91/297.41 877.91/297.41 Strict Trs: 877.91/297.41 { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) 877.91/297.41 , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) 877.91/297.41 , Frozen(m, Sum_term_var(xi), n, s) -> 877.91/297.41 Case(Term_sub(m, s), xi, Term_sub(n, s)) 877.91/297.41 , Concat(Cons_usual(x, m, s), t) -> 877.91/297.41 Cons_usual(x, Term_sub(m, t), Concat(s, t)) 877.91/297.41 , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } 877.91/297.41 Weak Trs: 877.91/297.41 { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) 877.91/297.41 , Term_sub(Term_app(m, n), s) -> 877.91/297.41 Term_app(Term_sub(m, s), Term_sub(n, s)) 877.91/297.41 , Term_sub(Term_pair(m, n), s) -> 877.91/297.41 Term_pair(Term_sub(m, s), Term_sub(n, s)) 877.91/297.41 , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) 877.91/297.41 , Term_sub(Term_var(x), Id()) -> Term_var(x) 877.91/297.41 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m 877.91/297.41 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> 877.91/297.41 Term_sub(Term_var(x), s) 877.91/297.41 , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> 877.91/297.41 Term_sub(Term_var(x), s) 877.91/297.41 , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) 877.91/297.41 , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) 877.91/297.41 , Sum_sub(xi, Id()) -> Sum_term_var(xi) 877.91/297.41 , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) 877.91/297.41 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) 877.91/297.41 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) 877.91/297.41 , Concat(Id(), s) -> s 877.91/297.41 , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) } 877.91/297.41 Obligation: 877.91/297.41 runtime complexity 877.91/297.41 Answer: 877.91/297.41 YES(O(1),O(n^2)) 877.91/297.41 877.91/297.41 We use the processor 'polynomial interpretation' to orient 877.91/297.41 following rules strictly. 877.91/297.41 877.91/297.41 Trs: 877.91/297.41 { Frozen(m, Sum_term_var(xi), n, s) -> 877.91/297.41 Case(Term_sub(m, s), xi, Term_sub(n, s)) } 877.91/297.41 877.91/297.41 The induced complexity on above rules (modulo remaining rules) is 877.91/297.41 YES(?,O(n^2)) . These rules are moved into the corresponding weak 877.91/297.41 component(s). 877.91/297.41 877.91/297.41 Sub-proof: 877.91/297.41 ---------- 877.91/297.41 We consider the following typing: 877.91/297.41 877.91/297.41 Term_sub :: (g,b) -> g 877.91/297.41 Case :: (g,c,g) -> g 877.91/297.41 Frozen :: (g,a,g,b) -> g 877.91/297.41 Sum_sub :: (c,b) -> a 877.91/297.41 Sum_constant :: d -> a 877.91/297.41 Left :: d 877.91/297.41 Right :: d 877.91/297.41 Sum_term_var :: c -> a 877.91/297.41 Term_app :: (g,g) -> g 877.91/297.41 Term_pair :: (g,g) -> g 877.91/297.41 Term_inl :: g -> g 877.91/297.41 Term_inr :: g -> g 877.91/297.41 Term_var :: e -> g 877.91/297.41 Id :: b 877.91/297.41 Cons_usual :: (f,g,b) -> b 877.91/297.41 Cons_sum :: (h,d,b) -> b 877.91/297.41 Concat :: (b,b) -> b 877.91/297.41 877.91/297.41 The following argument positions are considered usable: 877.91/297.41 877.91/297.41 Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, 877.91/297.41 Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2}, 877.91/297.41 Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, 877.91/297.41 Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, 877.91/297.41 Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, 877.91/297.41 Uargs(Concat) = {2} 877.91/297.41 877.91/297.41 TcT has computed the following constructor-restricted 877.91/297.41 typedpolynomial interpretation. 877.91/297.41 877.91/297.41 [Term_sub](x1, x2) = 1 + 2*x1 + x1*x2 + x2 877.91/297.41 877.91/297.41 [Case](x1, x2, x3) = 2 + x1 + x3 877.91/297.41 877.91/297.41 [Frozen](x1, x2, x3, x4) = 3 + 2*x1 + x1*x4 + x2 + 2*x3 + x3*x4 + 2*x4 877.91/297.41 877.91/297.41 [Sum_sub](x1, x2) = x2 877.91/297.41 877.91/297.41 [Sum_constant](x1) = 0 877.91/297.41 877.91/297.41 [Left]() = 0 877.91/297.41 877.91/297.41 [Right]() = 0 877.91/297.41 877.91/297.41 [Sum_term_var](x1) = 2 877.91/297.41 877.91/297.41 [Term_app](x1, x2) = 1 + x1 + x2 877.91/297.41 877.91/297.41 [Term_pair](x1, x2) = 2 + x1 + x2 877.91/297.41 877.91/297.41 [Term_inl](x1) = x1 877.91/297.41 877.91/297.41 [Term_inr](x1) = x1 877.91/297.41 877.91/297.41 [Term_var](x1) = 0 877.91/297.41 877.91/297.41 [Id]() = 2 877.91/297.41 877.91/297.41 [Cons_usual](x1, x2, x3) = 2 + 2*x2 + x3 877.91/297.41 877.91/297.41 [Cons_sum](x1, x2, x3) = 2 + x3 877.91/297.41 877.91/297.41 [Concat](x1, x2) = 2 + 2*x1 + x1*x2 + 2*x2 877.91/297.41 877.91/297.41 877.91/297.41 This order satisfies the following ordering constraints. 877.91/297.41 877.91/297.41 [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 877.91/297.41 >= 3 + 4*m + 2*m*s + m*s*t + 2*m*t + 2*s + s*t + 2*t 877.91/297.41 = [Term_sub(m, Concat(s, t))] 877.91/297.41 877.91/297.41 [Term_sub(Case(m, xi, n), s)] = 5 + 2*m + 2*n + 3*s + m*s + n*s 877.91/297.41 > 3 + 2*m + m*s + 3*s + 2*n + n*s 877.91/297.41 = [Frozen(m, Sum_sub(xi, s), n, s)] 877.91/297.41 877.91/297.41 [Term_sub(Term_app(m, n), s)] = 3 + 2*m + 2*n + 2*s + m*s + n*s 877.91/297.41 >= 3 + 2*m + m*s + 2*s + 2*n + n*s 877.91/297.41 = [Term_app(Term_sub(m, s), Term_sub(n, s))] 877.91/297.41 877.91/297.41 [Term_sub(Term_pair(m, n), s)] = 5 + 2*m + 2*n + 3*s + m*s + n*s 877.91/297.41 > 4 + 2*m + m*s + 2*s + 2*n + n*s 877.91/297.41 = [Term_pair(Term_sub(m, s), Term_sub(n, s))] 877.91/297.41 877.91/297.41 [Term_sub(Term_inl(m), s)] = 1 + 2*m + m*s + s 877.91/297.41 >= 1 + 2*m + m*s + s 877.91/297.41 = [Term_inl(Term_sub(m, s))] 877.91/297.41 877.91/297.41 [Term_sub(Term_inr(m), s)] = 1 + 2*m + m*s + s 877.91/297.41 >= 1 + 2*m + m*s + s 877.91/297.41 = [Term_inr(Term_sub(m, s))] 877.91/297.41 877.91/297.41 [Term_sub(Term_var(x), Id())] = 3 877.91/297.41 > 877.91/297.41 = [Term_var(x)] 877.91/297.41 877.91/297.41 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 3 + 2*m + s 877.91/297.41 > m 877.91/297.41 = [m] 877.91/297.41 877.91/297.41 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 3 + 2*m + s 877.91/297.41 > 1 + s 877.91/297.41 = [Term_sub(Term_var(x), s)] 877.91/297.41 877.91/297.41 [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = 3 + s 877.91/297.41 > 1 + s 877.91/297.41 = [Term_sub(Term_var(x), s)] 877.91/297.41 877.91/297.41 [Frozen(m, Sum_constant(Left()), n, s)] = 3 + 2*m + m*s + 2*n + n*s + 2*s 877.91/297.41 > 1 + 2*m + m*s + s 877.91/297.41 = [Term_sub(m, s)] 877.91/297.41 877.91/297.41 [Frozen(m, Sum_constant(Right()), n, s)] = 3 + 2*m + m*s + 2*n + n*s + 2*s 877.91/297.41 > 1 + 2*n + n*s + s 877.91/297.41 = [Term_sub(n, s)] 877.91/297.41 877.91/297.41 [Frozen(m, Sum_term_var(xi), n, s)] = 5 + 2*m + m*s + 2*n + n*s + 2*s 877.91/297.41 > 4 + 2*m + m*s + 2*s + 2*n + n*s 877.91/297.41 = [Case(Term_sub(m, s), xi, Term_sub(n, s))] 877.91/297.41 877.91/297.41 [Sum_sub(xi, Id())] = 2 877.91/297.41 >= 2 877.91/297.41 = [Sum_term_var(xi)] 877.91/297.41 877.91/297.41 [Sum_sub(xi, Cons_usual(y, m, s))] = 2 + 2*m + s 877.91/297.41 > s 877.91/297.41 = [Sum_sub(xi, s)] 877.91/297.41 877.91/297.41 [Sum_sub(xi, Cons_sum(psi, k, s))] = 2 + s 877.91/297.41 > s 877.91/297.41 = [Sum_sub(xi, s)] 877.91/297.41 877.91/297.41 [Sum_sub(xi, Cons_sum(psi, k, s))] = 2 + s 877.91/297.41 > 877.91/297.41 = [Sum_constant(k)] 877.91/297.41 877.91/297.41 [Concat(Id(), s)] = 6 + 4*s 877.91/297.41 > s 877.91/297.41 = [s] 877.91/297.41 877.91/297.41 [Concat(Cons_usual(x, m, s), t)] = 6 + 4*m + 2*s + 4*t + 2*m*t + s*t 877.91/297.41 >= 6 + 4*m + 2*m*t + 4*t + 2*s + s*t 877.91/297.41 = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] 877.91/297.41 877.91/297.41 [Concat(Cons_sum(xi, k, s), t)] = 6 + 2*s + 4*t + s*t 877.91/297.41 > 4 + 2*s + s*t + 2*t 877.91/297.41 = [Cons_sum(xi, k, Concat(s, t))] 877.91/297.41 877.91/297.41 [Concat(Concat(s, t), u)] = 6 + 4*s + 2*s*t + 4*t + 4*u + 2*s*u + s*t*u + 2*t*u 877.91/297.41 >= 6 + 4*s + 2*s*t + s*t*u + 2*s*u + 4*t + 2*t*u + 4*u 877.91/297.41 = [Concat(s, Concat(t, u))] 877.91/297.41 877.91/297.41 877.91/297.41 We return to the main proof. 877.91/297.41 877.91/297.41 We are left with following problem, upon which TcT provides the 877.91/297.41 certificate YES(O(1),O(n^2)). 877.91/297.41 877.91/297.41 Strict Trs: 877.91/297.41 { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) 877.91/297.41 , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) 877.91/297.41 , Concat(Cons_usual(x, m, s), t) -> 877.91/297.41 Cons_usual(x, Term_sub(m, t), Concat(s, t)) 877.91/297.41 , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } 877.91/297.41 Weak Trs: 877.91/297.41 { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) 877.91/297.41 , Term_sub(Term_app(m, n), s) -> 877.91/297.41 Term_app(Term_sub(m, s), Term_sub(n, s)) 877.91/297.41 , Term_sub(Term_pair(m, n), s) -> 877.91/297.41 Term_pair(Term_sub(m, s), Term_sub(n, s)) 877.91/297.41 , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) 877.91/297.41 , Term_sub(Term_var(x), Id()) -> Term_var(x) 877.91/297.41 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m 877.91/297.41 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> 877.91/297.41 Term_sub(Term_var(x), s) 877.91/297.41 , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> 877.91/297.41 Term_sub(Term_var(x), s) 877.91/297.41 , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) 877.91/297.41 , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) 877.91/297.41 , Frozen(m, Sum_term_var(xi), n, s) -> 877.91/297.41 Case(Term_sub(m, s), xi, Term_sub(n, s)) 877.91/297.41 , Sum_sub(xi, Id()) -> Sum_term_var(xi) 877.91/297.41 , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) 877.91/297.41 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) 877.91/297.41 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) 877.91/297.41 , Concat(Id(), s) -> s 877.91/297.41 , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) } 877.91/297.41 Obligation: 877.91/297.41 runtime complexity 877.91/297.41 Answer: 877.91/297.41 YES(O(1),O(n^2)) 877.91/297.41 877.91/297.41 We use the processor 'polynomial interpretation' to orient 877.91/297.41 following rules strictly. 877.91/297.41 877.91/297.41 Trs: 877.91/297.41 { Concat(Cons_usual(x, m, s), t) -> 877.91/297.41 Cons_usual(x, Term_sub(m, t), Concat(s, t)) } 877.91/297.41 877.91/297.41 The induced complexity on above rules (modulo remaining rules) is 877.91/297.41 YES(?,O(n^2)) . These rules are moved into the corresponding weak 877.91/297.41 component(s). 877.91/297.41 877.91/297.41 Sub-proof: 877.91/297.41 ---------- 877.91/297.41 We consider the following typing: 877.91/297.41 877.91/297.41 Term_sub :: (g,b) -> g 877.91/297.41 Case :: (g,c,g) -> g 877.91/297.41 Frozen :: (g,a,g,b) -> g 877.91/297.41 Sum_sub :: (c,b) -> a 877.91/297.41 Sum_constant :: d -> a 877.91/297.41 Left :: d 877.91/297.41 Right :: d 877.91/297.41 Sum_term_var :: c -> a 877.91/297.41 Term_app :: (g,g) -> g 877.91/297.41 Term_pair :: (g,g) -> g 877.91/297.41 Term_inl :: g -> g 877.91/297.41 Term_inr :: g -> g 877.91/297.41 Term_var :: e -> g 877.91/297.41 Id :: b 877.91/297.41 Cons_usual :: (f,g,b) -> b 877.91/297.41 Cons_sum :: (h,d,b) -> b 877.91/297.41 Concat :: (b,b) -> b 877.91/297.41 877.91/297.41 The following argument positions are considered usable: 877.91/297.41 877.91/297.41 Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, 877.91/297.41 Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2}, 877.91/297.41 Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, 877.91/297.41 Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, 877.91/297.41 Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, 877.91/297.41 Uargs(Concat) = {2} 877.91/297.41 877.91/297.41 TcT has computed the following constructor-restricted 877.91/297.41 typedpolynomial interpretation. 877.91/297.41 877.91/297.41 [Term_sub](x1, x2) = x1 + 2*x1*x2 + x1^2 + x2 877.91/297.41 877.91/297.41 [Case](x1, x2, x3) = 1 + x1 + x3 877.91/297.41 877.91/297.41 [Frozen](x1, x2, x3, x4) = 1 + x1 + x1*x3 + 2*x1*x4 + x1^2 + x2 + x3 + 2*x3*x4 + x3^2 + 2*x4 877.91/297.41 877.91/297.41 [Sum_sub](x1, x2) = 1 + x2 877.91/297.41 877.91/297.41 [Sum_constant](x1) = 0 877.91/297.41 877.91/297.41 [Left]() = 0 877.91/297.41 877.91/297.41 [Right]() = 0 877.91/297.41 877.91/297.41 [Sum_term_var](x1) = 0 877.91/297.41 877.91/297.41 [Term_app](x1, x2) = 2 + x1 + x2 877.91/297.41 877.91/297.41 [Term_pair](x1, x2) = 2 + x1 + x2 877.91/297.41 877.91/297.41 [Term_inl](x1) = x1 877.91/297.41 877.91/297.41 [Term_inr](x1) = 1 + x1 877.91/297.41 877.91/297.41 [Term_var](x1) = x1 877.91/297.41 877.91/297.41 [Id]() = 0 877.91/297.41 877.91/297.41 [Cons_usual](x1, x2, x3) = 2 + x2 + x3 877.91/297.41 877.91/297.41 [Cons_sum](x1, x2, x3) = x3 877.91/297.41 877.91/297.41 [Concat](x1, x2) = x1 + 2*x1*x2 + x1^2 + x2 877.91/297.41 877.91/297.41 877.91/297.41 This order satisfies the following ordering constraints. 877.91/297.41 877.91/297.41 [Term_sub(Term_sub(m, s), t)] = m + 3*m*s + 2*m^2 + s + 2*m*t + 4*m*s*t + 2*m^2*t + 2*s*t + 5*m^2*s + 2*m^3 + 4*m^2*s^2 + 4*m^3*s + 2*m*s^2 + m^4 + s*m + 2*s^2*m + s*m^2 + s^2 + t 877.91/297.41 >= m + 2*m*s + 4*m*s*t + 2*m*s^2 + 2*m*t + m^2 + s + 2*s*t + s^2 + t 877.91/297.41 = [Term_sub(m, Concat(s, t))] 877.91/297.41 877.91/297.41 [Term_sub(Case(m, xi, n), s)] = 2 + 3*m + 3*n + 3*s + 2*m*s + 2*n*s + m^2 + m*n + n*m + n^2 877.91/297.41 >= 2 + m + m*n + 2*m*s + m^2 + 3*s + n + 2*n*s + n^2 877.91/297.41 = [Frozen(m, Sum_sub(xi, s), n, s)] 877.91/297.41 877.91/297.41 [Term_sub(Term_app(m, n), s)] = 6 + 5*m + 5*n + 5*s + 2*m*s + 2*n*s + m^2 + m*n + n*m + n^2 877.91/297.41 > 2 + m + 2*m*s + m^2 + 2*s + n + 2*n*s + n^2 877.91/297.41 = [Term_app(Term_sub(m, s), Term_sub(n, s))] 877.91/297.41 877.91/297.41 [Term_sub(Term_pair(m, n), s)] = 6 + 5*m + 5*n + 5*s + 2*m*s + 2*n*s + m^2 + m*n + n*m + n^2 877.91/297.41 > 2 + m + 2*m*s + m^2 + 2*s + n + 2*n*s + n^2 877.91/297.41 = [Term_pair(Term_sub(m, s), Term_sub(n, s))] 877.91/297.41 877.91/297.41 [Term_sub(Term_inl(m), s)] = m + 2*m*s + m^2 + s 877.91/297.41 >= m + 2*m*s + m^2 + s 877.91/297.41 = [Term_inl(Term_sub(m, s))] 877.91/297.41 877.91/297.41 [Term_sub(Term_inr(m), s)] = 2 + 3*m + 3*s + 2*m*s + m^2 877.91/297.41 > 1 + m + 2*m*s + m^2 + s 877.91/297.41 = [Term_inr(Term_sub(m, s))] 877.91/297.41 877.91/297.41 [Term_sub(Term_var(x), Id())] = x + x^2 877.91/297.41 >= x 877.91/297.41 = [Term_var(x)] 877.91/297.41 877.91/297.41 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 5*x + 2*x*m + 2*x*s + x^2 + 2 + m + s 877.91/297.41 > m 877.91/297.41 = [m] 877.91/297.41 877.91/297.41 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 5*x + 2*x*m + 2*x*s + x^2 + 2 + m + s 877.91/297.41 > x + 2*x*s + x^2 + s 877.91/297.41 = [Term_sub(Term_var(x), s)] 877.91/297.41 877.91/297.41 [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = x + 2*x*s + x^2 + s 877.91/297.41 >= x + 2*x*s + x^2 + s 877.91/297.41 = [Term_sub(Term_var(x), s)] 877.91/297.41 877.91/297.41 [Frozen(m, Sum_constant(Left()), n, s)] = 1 + m + m*n + 2*m*s + m^2 + n + 2*n*s + n^2 + 2*s 877.91/297.41 > m + 2*m*s + m^2 + s 877.91/297.41 = [Term_sub(m, s)] 877.91/297.41 877.91/297.41 [Frozen(m, Sum_constant(Right()), n, s)] = 1 + m + m*n + 2*m*s + m^2 + n + 2*n*s + n^2 + 2*s 877.91/297.41 > n + 2*n*s + n^2 + s 877.91/297.41 = [Term_sub(n, s)] 877.91/297.41 877.91/297.41 [Frozen(m, Sum_term_var(xi), n, s)] = 1 + m + m*n + 2*m*s + m^2 + n + 2*n*s + n^2 + 2*s 877.91/297.41 >= 1 + m + 2*m*s + m^2 + 2*s + n + 2*n*s + n^2 877.91/297.41 = [Case(Term_sub(m, s), xi, Term_sub(n, s))] 877.91/297.41 877.91/297.41 [Sum_sub(xi, Id())] = 1 877.91/297.41 > 877.91/297.41 = [Sum_term_var(xi)] 877.91/297.41 877.91/297.41 [Sum_sub(xi, Cons_usual(y, m, s))] = 3 + m + s 877.91/297.41 > 1 + s 877.91/297.41 = [Sum_sub(xi, s)] 877.91/297.41 877.91/297.41 [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 + s 877.91/297.41 >= 1 + s 877.91/297.41 = [Sum_sub(xi, s)] 877.91/297.41 877.91/297.41 [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 + s 877.91/297.41 > 877.91/297.41 = [Sum_constant(k)] 877.91/297.41 877.91/297.41 [Concat(Id(), s)] = s 877.91/297.41 >= s 877.91/297.41 = [s] 877.91/297.41 877.91/297.41 [Concat(Cons_usual(x, m, s), t)] = 6 + 5*m + 5*s + 5*t + 2*m*t + 2*s*t + m^2 + m*s + s*m + s^2 877.91/297.41 > 2 + m + 2*m*t + m^2 + 2*t + s + 2*s*t + s^2 877.91/297.41 = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] 877.91/297.41 877.91/297.41 [Concat(Cons_sum(xi, k, s), t)] = s + 2*s*t + s^2 + t 877.91/297.41 >= s + 2*s*t + s^2 + t 877.91/297.41 = [Cons_sum(xi, k, Concat(s, t))] 877.91/297.41 877.91/297.41 [Concat(Concat(s, t), u)] = s + 3*s*t + 2*s^2 + t + 2*s*u + 4*s*t*u + 2*s^2*u + 2*t*u + 5*s^2*t + 2*s^3 + 4*s^2*t^2 + 4*s^3*t + 2*s*t^2 + s^4 + t*s + 2*t^2*s + t*s^2 + t^2 + u 877.91/297.41 >= s + 2*s*t + 4*s*t*u + 2*s*t^2 + 2*s*u + s^2 + t + 2*t*u + t^2 + u 877.91/297.41 = [Concat(s, Concat(t, u))] 877.91/297.41 877.91/297.41 877.91/297.41 We return to the main proof. 877.91/297.41 877.91/297.41 We are left with following problem, upon which TcT provides the 877.91/297.41 certificate YES(O(1),O(n^2)). 877.91/297.41 877.91/297.41 Strict Trs: 877.91/297.41 { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) 877.91/297.41 , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) 877.91/297.41 , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } 877.91/297.41 Weak Trs: 877.91/297.41 { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) 877.91/297.41 , Term_sub(Term_app(m, n), s) -> 877.91/297.41 Term_app(Term_sub(m, s), Term_sub(n, s)) 877.91/297.41 , Term_sub(Term_pair(m, n), s) -> 877.91/297.41 Term_pair(Term_sub(m, s), Term_sub(n, s)) 877.91/297.41 , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) 877.91/297.41 , Term_sub(Term_var(x), Id()) -> Term_var(x) 877.91/297.41 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m 877.91/297.41 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> 877.91/297.41 Term_sub(Term_var(x), s) 877.91/297.41 , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> 877.91/297.41 Term_sub(Term_var(x), s) 877.91/297.41 , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) 877.91/297.41 , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) 877.91/297.41 , Frozen(m, Sum_term_var(xi), n, s) -> 877.91/297.41 Case(Term_sub(m, s), xi, Term_sub(n, s)) 877.91/297.41 , Sum_sub(xi, Id()) -> Sum_term_var(xi) 877.91/297.41 , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) 877.91/297.41 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) 877.91/297.41 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) 877.91/297.41 , Concat(Id(), s) -> s 877.91/297.41 , Concat(Cons_usual(x, m, s), t) -> 877.91/297.41 Cons_usual(x, Term_sub(m, t), Concat(s, t)) 877.91/297.41 , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) } 877.91/297.41 Obligation: 877.91/297.41 runtime complexity 877.91/297.41 Answer: 877.91/297.41 YES(O(1),O(n^2)) 877.91/297.41 877.91/297.41 We use the processor 'polynomial interpretation' to orient 877.91/297.41 following rules strictly. 877.91/297.41 877.91/297.41 Trs: { Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) } 877.91/297.41 877.91/297.41 The induced complexity on above rules (modulo remaining rules) is 877.91/297.41 YES(?,O(n^2)) . These rules are moved into the corresponding weak 877.91/297.41 component(s). 877.91/297.41 877.91/297.41 Sub-proof: 877.91/297.41 ---------- 877.91/297.41 We consider the following typing: 877.91/297.41 877.91/297.41 Term_sub :: (g,b) -> g 877.91/297.41 Case :: (g,c,g) -> g 877.91/297.41 Frozen :: (g,a,g,b) -> g 877.91/297.41 Sum_sub :: (c,b) -> a 877.91/297.41 Sum_constant :: d -> a 877.91/297.41 Left :: d 877.91/297.41 Right :: d 877.91/297.41 Sum_term_var :: c -> a 877.91/297.41 Term_app :: (g,g) -> g 877.91/297.41 Term_pair :: (g,g) -> g 877.91/297.41 Term_inl :: g -> g 877.91/297.41 Term_inr :: g -> g 877.91/297.41 Term_var :: e -> g 877.91/297.41 Id :: b 877.91/297.41 Cons_usual :: (f,g,b) -> b 877.91/297.41 Cons_sum :: (h,d,b) -> b 877.91/297.41 Concat :: (b,b) -> b 877.91/297.41 877.91/297.41 The following argument positions are considered usable: 877.91/297.41 877.91/297.41 Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, 877.91/297.41 Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2}, 877.91/297.41 Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, 877.91/297.41 Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, 877.91/297.41 Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, 877.91/297.41 Uargs(Concat) = {2} 877.91/297.41 877.91/297.41 TcT has computed the following constructor-restricted 877.91/297.41 typedpolynomial interpretation. 877.91/297.41 877.91/297.41 [Term_sub](x1, x2) = x1 + x1*x2 + x1^2 + x2 877.91/297.41 877.91/297.41 [Case](x1, x2, x3) = 2 + x1 + x3 877.91/297.41 877.91/297.41 [Frozen](x1, x2, x3, x4) = 2 + x1 + x1*x3 + x1*x4 + x1^2 + x2 + x3 + x3*x4 + x3^2 + 2*x4 877.91/297.41 877.91/297.41 [Sum_sub](x1, x2) = x2 877.91/297.41 877.91/297.41 [Sum_constant](x1) = 0 877.91/297.41 877.91/297.41 [Left]() = 0 877.91/297.41 877.91/297.41 [Right]() = 0 877.91/297.41 877.91/297.41 [Sum_term_var](x1) = 0 877.91/297.41 877.91/297.41 [Term_app](x1, x2) = 1 + x1 + x2 877.91/297.41 877.91/297.41 [Term_pair](x1, x2) = 2 + x1 + x2 877.91/297.41 877.91/297.41 [Term_inl](x1) = 2 + x1 877.91/297.41 877.91/297.41 [Term_inr](x1) = x1 877.91/297.41 877.91/297.41 [Term_var](x1) = 0 877.91/297.41 877.91/297.41 [Id]() = 0 877.91/297.41 877.91/297.41 [Cons_usual](x1, x2, x3) = 2 + x2 + x3 877.91/297.41 877.91/297.41 [Cons_sum](x1, x2, x3) = x3 877.91/297.41 877.91/297.41 [Concat](x1, x2) = x1 + x1*x2 + x1^2 + x2 877.91/297.41 877.91/297.41 877.91/297.41 This order satisfies the following ordering constraints. 877.91/297.41 877.91/297.41 [Term_sub(Term_sub(m, s), t)] = m + 2*m*s + 2*m^2 + s + m*t + m*s*t + m^2*t + s*t + 3*m^2*s + 2*m^3 + m^2*s^2 + 2*m^3*s + m*s^2 + m^4 + s*m + s^2*m + s*m^2 + s^2 + t 877.91/297.41 >= m + m*s + m*s*t + m*s^2 + m*t + m^2 + s + s*t + s^2 + t 877.91/297.41 = [Term_sub(m, Concat(s, t))] 877.91/297.41 877.91/297.41 [Term_sub(Case(m, xi, n), s)] = 6 + 5*m + 5*n + 3*s + m*s + n*s + m^2 + m*n + n*m + n^2 877.91/297.41 > 2 + m + m*n + m*s + m^2 + 3*s + n + n*s + n^2 877.91/297.41 = [Frozen(m, Sum_sub(xi, s), n, s)] 877.91/297.41 877.91/297.41 [Term_sub(Term_app(m, n), s)] = 2 + 3*m + 3*n + 2*s + m*s + n*s + m^2 + m*n + n*m + n^2 877.91/297.41 > 1 + m + m*s + m^2 + 2*s + n + n*s + n^2 877.91/297.41 = [Term_app(Term_sub(m, s), Term_sub(n, s))] 877.91/297.41 877.91/297.41 [Term_sub(Term_pair(m, n), s)] = 6 + 5*m + 5*n + 3*s + m*s + n*s + m^2 + m*n + n*m + n^2 877.91/297.41 > 2 + m + m*s + m^2 + 2*s + n + n*s + n^2 877.91/297.41 = [Term_pair(Term_sub(m, s), Term_sub(n, s))] 877.91/297.41 877.91/297.41 [Term_sub(Term_inl(m), s)] = 6 + 5*m + 3*s + m*s + m^2 877.91/297.41 > 2 + m + m*s + m^2 + s 877.91/297.41 = [Term_inl(Term_sub(m, s))] 877.91/297.41 877.91/297.41 [Term_sub(Term_inr(m), s)] = m + m*s + m^2 + s 877.91/297.41 >= m + m*s + m^2 + s 877.91/297.41 = [Term_inr(Term_sub(m, s))] 877.91/297.41 877.91/297.41 [Term_sub(Term_var(x), Id())] = 877.91/297.41 >= 877.91/297.41 = [Term_var(x)] 877.91/297.41 877.91/297.41 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s 877.91/297.41 > m 877.91/297.41 = [m] 877.91/297.41 877.91/297.41 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s 877.91/297.41 > s 877.91/297.41 = [Term_sub(Term_var(x), s)] 877.91/297.41 877.91/297.41 [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = s 877.91/297.41 >= s 877.91/297.41 = [Term_sub(Term_var(x), s)] 877.91/297.41 877.91/297.41 [Frozen(m, Sum_constant(Left()), n, s)] = 2 + m + m*n + m*s + m^2 + n + n*s + n^2 + 2*s 877.91/297.41 > m + m*s + m^2 + s 877.91/297.41 = [Term_sub(m, s)] 877.91/297.41 877.91/297.41 [Frozen(m, Sum_constant(Right()), n, s)] = 2 + m + m*n + m*s + m^2 + n + n*s + n^2 + 2*s 877.91/297.41 > n + n*s + n^2 + s 877.91/297.41 = [Term_sub(n, s)] 877.91/297.41 877.91/297.41 [Frozen(m, Sum_term_var(xi), n, s)] = 2 + m + m*n + m*s + m^2 + n + n*s + n^2 + 2*s 877.91/297.41 >= 2 + m + m*s + m^2 + 2*s + n + n*s + n^2 877.91/297.41 = [Case(Term_sub(m, s), xi, Term_sub(n, s))] 877.91/297.41 877.91/297.41 [Sum_sub(xi, Id())] = 877.91/297.41 >= 877.91/297.41 = [Sum_term_var(xi)] 877.91/297.41 877.91/297.41 [Sum_sub(xi, Cons_usual(y, m, s))] = 2 + m + s 877.91/297.41 > s 877.91/297.41 = [Sum_sub(xi, s)] 877.91/297.41 877.91/297.41 [Sum_sub(xi, Cons_sum(psi, k, s))] = s 877.91/297.41 >= s 877.91/297.41 = [Sum_sub(xi, s)] 877.91/297.41 877.91/297.41 [Sum_sub(xi, Cons_sum(psi, k, s))] = s 877.91/297.41 >= 877.91/297.42 = [Sum_constant(k)] 877.91/297.42 877.91/297.42 [Concat(Id(), s)] = s 877.91/297.42 >= s 877.91/297.42 = [s] 877.91/297.42 877.91/297.42 [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 877.91/297.42 > 2 + m + m*t + m^2 + 2*t + s + s*t + s^2 877.91/297.42 = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] 877.91/297.42 877.91/297.42 [Concat(Cons_sum(xi, k, s), t)] = s + s*t + s^2 + t 877.91/297.42 >= s + s*t + s^2 + t 877.91/297.42 = [Cons_sum(xi, k, Concat(s, t))] 877.91/297.42 877.91/297.42 [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 877.91/297.42 >= s + s*t + s*t*u + s*t^2 + s*u + s^2 + t + t*u + t^2 + u 877.91/297.42 = [Concat(s, Concat(t, u))] 877.91/297.42 877.91/297.42 877.91/297.42 We return to the main proof. 877.91/297.42 877.91/297.42 We are left with following problem, upon which TcT provides the 877.91/297.42 certificate YES(O(1),O(n^2)). 877.91/297.42 877.91/297.42 Strict Trs: 877.91/297.42 { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) 877.91/297.42 , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } 877.91/297.42 Weak Trs: 877.91/297.42 { Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) 877.91/297.42 , Term_sub(Term_app(m, n), s) -> 877.91/297.42 Term_app(Term_sub(m, s), Term_sub(n, s)) 877.91/297.42 , Term_sub(Term_pair(m, n), s) -> 877.91/297.42 Term_pair(Term_sub(m, s), Term_sub(n, s)) 877.91/297.42 , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) 877.91/297.42 , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) 877.91/297.42 , Term_sub(Term_var(x), Id()) -> Term_var(x) 877.91/297.42 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m 877.91/297.42 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> 877.91/297.42 Term_sub(Term_var(x), s) 877.91/297.42 , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> 877.91/297.42 Term_sub(Term_var(x), s) 877.91/297.42 , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) 877.91/297.42 , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) 877.91/297.42 , Frozen(m, Sum_term_var(xi), n, s) -> 877.91/297.42 Case(Term_sub(m, s), xi, Term_sub(n, s)) 877.91/297.42 , Sum_sub(xi, Id()) -> Sum_term_var(xi) 877.91/297.42 , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) 877.91/297.42 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) 877.91/297.42 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) 877.91/297.42 , Concat(Id(), s) -> s 877.91/297.42 , Concat(Cons_usual(x, m, s), t) -> 877.91/297.42 Cons_usual(x, Term_sub(m, t), Concat(s, t)) 877.91/297.42 , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) } 877.91/297.42 Obligation: 877.91/297.42 runtime complexity 877.91/297.42 Answer: 877.91/297.42 YES(O(1),O(n^2)) 877.91/297.42 877.91/297.42 We use the processor 'polynomial interpretation' to orient 877.91/297.42 following rules strictly. 877.91/297.42 877.91/297.42 Trs: { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) } 877.91/297.42 877.91/297.42 The induced complexity on above rules (modulo remaining rules) is 877.91/297.42 YES(?,O(n^2)) . These rules are moved into the corresponding weak 877.91/297.42 component(s). 877.91/297.42 877.91/297.42 Sub-proof: 877.91/297.42 ---------- 877.91/297.42 We consider the following typing: 877.91/297.42 877.91/297.42 Term_sub :: (g,b) -> g 877.91/297.42 Case :: (g,c,g) -> g 877.91/297.42 Frozen :: (g,a,g,b) -> g 877.91/297.42 Sum_sub :: (c,b) -> a 877.91/297.42 Sum_constant :: d -> a 877.91/297.42 Left :: d 877.91/297.42 Right :: d 877.91/297.42 Sum_term_var :: c -> a 877.91/297.42 Term_app :: (g,g) -> g 877.91/297.42 Term_pair :: (g,g) -> g 877.91/297.42 Term_inl :: g -> g 877.91/297.42 Term_inr :: g -> g 877.91/297.42 Term_var :: e -> g 877.91/297.42 Id :: b 877.91/297.42 Cons_usual :: (f,g,b) -> b 877.91/297.42 Cons_sum :: (h,d,b) -> b 877.91/297.42 Concat :: (b,b) -> b 877.91/297.42 877.91/297.42 The following argument positions are considered usable: 877.91/297.42 877.91/297.42 Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, 877.91/297.42 Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2}, 877.91/297.42 Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, 877.91/297.42 Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, 877.91/297.42 Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, 877.91/297.42 Uargs(Concat) = {2} 877.91/297.42 877.91/297.42 TcT has computed the following constructor-restricted 877.91/297.42 typedpolynomial interpretation. 877.91/297.42 877.91/297.42 [Term_sub](x1, x2) = 1 + x1 + x1*x2 + x1^2 + x2 877.91/297.42 877.91/297.42 [Case](x1, x2, x3) = 2 + x1 + x3 877.91/297.42 877.91/297.42 [Frozen](x1, x2, x3, x4) = 3 + x1 + x1*x3 + x1*x4 + x1^2 + x2 + x3 + x3*x4 + x3^2 + 2*x4 877.91/297.42 877.91/297.42 [Sum_sub](x1, x2) = 1 + x2 877.91/297.42 877.91/297.42 [Sum_constant](x1) = 1 877.91/297.42 877.91/297.42 [Left]() = 0 877.91/297.42 877.91/297.42 [Right]() = 0 877.91/297.42 877.91/297.42 [Sum_term_var](x1) = 1 877.91/297.42 877.91/297.42 [Term_app](x1, x2) = 1 + x1 + x2 877.91/297.42 877.91/297.42 [Term_pair](x1, x2) = 1 + x1 + x2 877.91/297.42 877.91/297.42 [Term_inl](x1) = x1 877.91/297.42 877.91/297.42 [Term_inr](x1) = x1 877.91/297.42 877.91/297.42 [Term_var](x1) = 0 877.91/297.42 877.91/297.42 [Id]() = 0 877.91/297.42 877.91/297.42 [Cons_usual](x1, x2, x3) = 2 + x2 + x3 877.91/297.42 877.91/297.42 [Cons_sum](x1, x2, x3) = x3 877.91/297.42 877.91/297.42 [Concat](x1, x2) = x1 + x1*x2 + x1^2 + x2 877.91/297.42 877.91/297.42 877.91/297.42 This order satisfies the following ordering constraints. 877.91/297.42 877.91/297.42 [Term_sub(Term_sub(m, s), t)] = 3 + 3*m + 4*m*s + 4*m^2 + 3*s + 2*t + m*t + m*s*t + m^2*t + s*t + 3*m^2*s + 2*m^3 + m^2*s^2 + 2*m^3*s + m*s^2 + m^4 + s*m + s^2*m + s*m^2 + s^2 877.91/297.42 > 1 + m + m*s + m*s*t + m*s^2 + m*t + m^2 + s + s*t + s^2 + t 877.91/297.42 = [Term_sub(m, Concat(s, t))] 877.91/297.42 877.91/297.42 [Term_sub(Case(m, xi, n), s)] = 7 + 5*m + 5*n + 3*s + m*s + n*s + m^2 + m*n + n*m + n^2 877.91/297.42 > 4 + m + m*n + m*s + m^2 + 3*s + n + n*s + n^2 877.91/297.42 = [Frozen(m, Sum_sub(xi, s), n, s)] 877.91/297.42 877.91/297.42 [Term_sub(Term_app(m, n), s)] = 3 + 3*m + 3*n + 2*s + m*s + n*s + m^2 + m*n + n*m + n^2 877.91/297.42 >= 3 + m + m*s + m^2 + 2*s + n + n*s + n^2 877.91/297.42 = [Term_app(Term_sub(m, s), Term_sub(n, s))] 877.91/297.42 877.91/297.42 [Term_sub(Term_pair(m, n), s)] = 3 + 3*m + 3*n + 2*s + m*s + n*s + m^2 + m*n + n*m + n^2 877.91/297.42 >= 3 + m + m*s + m^2 + 2*s + n + n*s + n^2 877.91/297.42 = [Term_pair(Term_sub(m, s), Term_sub(n, s))] 877.91/297.42 877.91/297.42 [Term_sub(Term_inl(m), s)] = 1 + m + m*s + m^2 + s 877.91/297.42 >= 1 + m + m*s + m^2 + s 877.91/297.42 = [Term_inl(Term_sub(m, s))] 877.91/297.42 877.91/297.42 [Term_sub(Term_inr(m), s)] = 1 + m + m*s + m^2 + s 877.91/297.42 >= 1 + m + m*s + m^2 + s 877.91/297.42 = [Term_inr(Term_sub(m, s))] 877.91/297.42 877.91/297.42 [Term_sub(Term_var(x), Id())] = 1 877.91/297.42 > 877.91/297.42 = [Term_var(x)] 877.91/297.42 877.91/297.42 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 3 + m + s 877.91/297.42 > m 877.91/297.42 = [m] 877.91/297.42 877.91/297.42 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 3 + m + s 877.91/297.42 > 1 + s 877.91/297.42 = [Term_sub(Term_var(x), s)] 877.91/297.42 877.91/297.42 [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = 1 + s 877.91/297.42 >= 1 + s 877.91/297.42 = [Term_sub(Term_var(x), s)] 877.91/297.42 877.91/297.42 [Frozen(m, Sum_constant(Left()), n, s)] = 4 + m + m*n + m*s + m^2 + n + n*s + n^2 + 2*s 877.91/297.42 > 1 + m + m*s + m^2 + s 877.91/297.42 = [Term_sub(m, s)] 877.91/297.42 877.91/297.42 [Frozen(m, Sum_constant(Right()), n, s)] = 4 + m + m*n + m*s + m^2 + n + n*s + n^2 + 2*s 877.91/297.42 > 1 + n + n*s + n^2 + s 877.91/297.42 = [Term_sub(n, s)] 877.91/297.42 877.91/297.42 [Frozen(m, Sum_term_var(xi), n, s)] = 4 + m + m*n + m*s + m^2 + n + n*s + n^2 + 2*s 877.91/297.42 >= 4 + m + m*s + m^2 + 2*s + n + n*s + n^2 877.91/297.42 = [Case(Term_sub(m, s), xi, Term_sub(n, s))] 877.91/297.42 877.91/297.42 [Sum_sub(xi, Id())] = 1 877.91/297.42 >= 1 877.91/297.42 = [Sum_term_var(xi)] 877.91/297.42 877.91/297.42 [Sum_sub(xi, Cons_usual(y, m, s))] = 3 + m + s 877.91/297.42 > 1 + s 877.91/297.42 = [Sum_sub(xi, s)] 877.91/297.42 877.91/297.42 [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 + s 877.91/297.42 >= 1 + s 877.91/297.42 = [Sum_sub(xi, s)] 877.91/297.42 877.91/297.42 [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 + s 877.91/297.42 >= 1 877.91/297.42 = [Sum_constant(k)] 877.91/297.42 877.91/297.42 [Concat(Id(), s)] = s 877.91/297.42 >= s 877.91/297.42 = [s] 877.91/297.42 877.91/297.42 [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 877.91/297.42 > 3 + m + m*t + m^2 + 2*t + s + s*t + s^2 877.91/297.42 = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] 877.91/297.42 877.91/297.42 [Concat(Cons_sum(xi, k, s), t)] = s + s*t + s^2 + t 877.91/297.42 >= s + s*t + s^2 + t 877.91/297.42 = [Cons_sum(xi, k, Concat(s, t))] 877.91/297.42 877.91/297.42 [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 877.91/297.42 >= s + s*t + s*t*u + s*t^2 + s*u + s^2 + t + t*u + t^2 + u 877.91/297.42 = [Concat(s, Concat(t, u))] 877.91/297.42 877.91/297.42 877.91/297.42 We return to the main proof. 877.91/297.42 877.91/297.42 We are left with following problem, upon which TcT provides the 877.91/297.42 certificate YES(O(1),O(n^2)). 877.91/297.42 877.91/297.42 Strict Trs: { Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } 877.91/297.42 Weak Trs: 877.91/297.42 { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) 877.91/297.42 , Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) 877.91/297.42 , Term_sub(Term_app(m, n), s) -> 877.91/297.42 Term_app(Term_sub(m, s), Term_sub(n, s)) 877.91/297.42 , Term_sub(Term_pair(m, n), s) -> 877.91/297.42 Term_pair(Term_sub(m, s), Term_sub(n, s)) 877.91/297.42 , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) 877.91/297.42 , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) 877.91/297.42 , Term_sub(Term_var(x), Id()) -> Term_var(x) 877.91/297.42 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m 877.91/297.42 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> 877.91/297.42 Term_sub(Term_var(x), s) 877.91/297.42 , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> 877.91/297.42 Term_sub(Term_var(x), s) 877.91/297.42 , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) 877.91/297.42 , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) 877.91/297.42 , Frozen(m, Sum_term_var(xi), n, s) -> 877.91/297.42 Case(Term_sub(m, s), xi, Term_sub(n, s)) 877.91/297.42 , Sum_sub(xi, Id()) -> Sum_term_var(xi) 877.91/297.42 , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) 877.91/297.42 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) 877.91/297.42 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) 877.91/297.42 , Concat(Id(), s) -> s 877.91/297.42 , Concat(Cons_usual(x, m, s), t) -> 877.91/297.42 Cons_usual(x, Term_sub(m, t), Concat(s, t)) 877.91/297.42 , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) } 877.91/297.42 Obligation: 877.91/297.42 runtime complexity 877.91/297.42 Answer: 877.91/297.42 YES(O(1),O(n^2)) 877.91/297.42 877.91/297.42 We use the processor 'polynomial interpretation' to orient 877.91/297.42 following rules strictly. 877.91/297.42 877.91/297.42 Trs: { Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } 877.91/297.42 877.91/297.42 The induced complexity on above rules (modulo remaining rules) is 877.91/297.42 YES(?,O(n^2)) . These rules are moved into the corresponding weak 877.91/297.42 component(s). 877.91/297.42 877.91/297.42 Sub-proof: 877.91/297.42 ---------- 877.91/297.42 We consider the following typing: 877.91/297.42 877.91/297.42 Term_sub :: (g,b) -> g 877.91/297.42 Case :: (g,c,g) -> g 877.91/297.42 Frozen :: (g,a,g,b) -> g 877.91/297.42 Sum_sub :: (c,b) -> a 877.91/297.42 Sum_constant :: d -> a 877.91/297.42 Left :: d 877.91/297.42 Right :: d 877.91/297.42 Sum_term_var :: c -> a 877.91/297.42 Term_app :: (g,g) -> g 877.91/297.42 Term_pair :: (g,g) -> g 877.91/297.42 Term_inl :: g -> g 877.91/297.42 Term_inr :: g -> g 877.91/297.42 Term_var :: e -> g 877.91/297.42 Id :: b 877.91/297.42 Cons_usual :: (f,g,b) -> b 877.91/297.42 Cons_sum :: (h,d,b) -> b 877.91/297.42 Concat :: (b,b) -> b 877.91/297.42 877.91/297.42 The following argument positions are considered usable: 877.91/297.42 877.91/297.42 Uargs(Term_sub) = {2}, Uargs(Case) = {1, 3}, 877.91/297.42 Uargs(Frozen) = {2, 4}, Uargs(Sum_sub) = {2}, 877.91/297.42 Uargs(Term_app) = {1, 2}, Uargs(Term_pair) = {1, 2}, 877.91/297.42 Uargs(Term_inl) = {1}, Uargs(Term_inr) = {1}, 877.91/297.42 Uargs(Cons_usual) = {2, 3}, Uargs(Cons_sum) = {3}, 877.91/297.42 Uargs(Concat) = {2} 877.91/297.42 877.91/297.42 TcT has computed the following constructor-restricted 877.91/297.42 typedpolynomial interpretation. 877.91/297.42 877.91/297.42 [Term_sub](x1, x2) = 1 + 2*x1 + 2*x1*x2 + x2 877.91/297.42 877.91/297.42 [Case](x1, x2, x3) = 2 + x1 + x3 877.91/297.42 877.91/297.42 [Frozen](x1, x2, x3, x4) = 3 + 2*x1 + 2*x1*x4 + x2 + 2*x3 + 2*x3*x4 + 2*x4 877.91/297.42 877.91/297.42 [Sum_sub](x1, x2) = 1 + x2 877.91/297.42 877.91/297.42 [Sum_constant](x1) = 0 877.91/297.42 877.91/297.42 [Left]() = 0 877.91/297.42 877.91/297.42 [Right]() = 0 877.91/297.42 877.91/297.42 [Sum_term_var](x1) = 1 877.91/297.42 877.91/297.42 [Term_app](x1, x2) = 1 + x1 + x2 877.91/297.42 877.91/297.42 [Term_pair](x1, x2) = 1 + x1 + x2 877.91/297.42 877.91/297.42 [Term_inl](x1) = x1 877.91/297.42 877.91/297.42 [Term_inr](x1) = 2 + x1 877.91/297.42 877.91/297.42 [Term_var](x1) = 0 877.91/297.42 877.91/297.42 [Id]() = 0 877.91/297.42 877.91/297.42 [Cons_usual](x1, x2, x3) = 1 + x2 + x3 877.91/297.42 877.91/297.42 [Cons_sum](x1, x2, x3) = x3 877.91/297.42 877.91/297.42 [Concat](x1, x2) = 1 + 2*x1 + 2*x1*x2 + x2 877.91/297.42 877.91/297.42 877.91/297.42 This order satisfies the following ordering constraints. 877.91/297.42 877.91/297.42 [Term_sub(Term_sub(m, s), t)] = 3 + 4*m + 4*m*s + 2*s + 3*t + 4*m*t + 4*m*s*t + 2*s*t 877.91/297.42 > 2 + 4*m + 4*m*s + 4*m*s*t + 2*m*t + 2*s + 2*s*t + t 877.91/297.42 = [Term_sub(m, Concat(s, t))] 877.91/297.42 877.91/297.42 [Term_sub(Case(m, xi, n), s)] = 5 + 2*m + 2*n + 5*s + 2*m*s + 2*n*s 877.91/297.42 > 4 + 2*m + 2*m*s + 3*s + 2*n + 2*n*s 877.91/297.42 = [Frozen(m, Sum_sub(xi, s), n, s)] 877.91/297.42 877.91/297.42 [Term_sub(Term_app(m, n), s)] = 3 + 2*m + 2*n + 3*s + 2*m*s + 2*n*s 877.91/297.42 >= 3 + 2*m + 2*m*s + 2*s + 2*n + 2*n*s 877.91/297.42 = [Term_app(Term_sub(m, s), Term_sub(n, s))] 877.91/297.42 877.91/297.42 [Term_sub(Term_pair(m, n), s)] = 3 + 2*m + 2*n + 3*s + 2*m*s + 2*n*s 877.91/297.42 >= 3 + 2*m + 2*m*s + 2*s + 2*n + 2*n*s 877.91/297.42 = [Term_pair(Term_sub(m, s), Term_sub(n, s))] 877.91/297.42 877.91/297.42 [Term_sub(Term_inl(m), s)] = 1 + 2*m + 2*m*s + s 877.91/297.42 >= 1 + 2*m + 2*m*s + s 877.91/297.42 = [Term_inl(Term_sub(m, s))] 877.91/297.42 877.91/297.42 [Term_sub(Term_inr(m), s)] = 5 + 2*m + 5*s + 2*m*s 877.91/297.42 > 3 + 2*m + 2*m*s + s 877.91/297.42 = [Term_inr(Term_sub(m, s))] 877.91/297.42 877.91/297.42 [Term_sub(Term_var(x), Id())] = 1 877.91/297.42 > 877.91/297.42 = [Term_var(x)] 877.91/297.42 877.91/297.42 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s 877.91/297.42 > m 877.91/297.42 = [m] 877.91/297.42 877.91/297.42 [Term_sub(Term_var(x), Cons_usual(y, m, s))] = 2 + m + s 877.91/297.42 > 1 + s 877.91/297.42 = [Term_sub(Term_var(x), s)] 877.91/297.42 877.91/297.42 [Term_sub(Term_var(x), Cons_sum(xi, k, s))] = 1 + s 877.91/297.42 >= 1 + s 877.91/297.42 = [Term_sub(Term_var(x), s)] 877.91/297.42 877.91/297.42 [Frozen(m, Sum_constant(Left()), n, s)] = 3 + 2*m + 2*m*s + 2*n + 2*n*s + 2*s 877.91/297.42 > 1 + 2*m + 2*m*s + s 877.91/297.42 = [Term_sub(m, s)] 877.91/297.42 877.91/297.42 [Frozen(m, Sum_constant(Right()), n, s)] = 3 + 2*m + 2*m*s + 2*n + 2*n*s + 2*s 877.91/297.42 > 1 + 2*n + 2*n*s + s 877.91/297.42 = [Term_sub(n, s)] 877.91/297.42 877.91/297.42 [Frozen(m, Sum_term_var(xi), n, s)] = 4 + 2*m + 2*m*s + 2*n + 2*n*s + 2*s 877.91/297.42 >= 4 + 2*m + 2*m*s + 2*s + 2*n + 2*n*s 877.91/297.42 = [Case(Term_sub(m, s), xi, Term_sub(n, s))] 877.91/297.42 877.91/297.42 [Sum_sub(xi, Id())] = 1 877.91/297.42 >= 1 877.91/297.42 = [Sum_term_var(xi)] 877.91/297.42 877.91/297.42 [Sum_sub(xi, Cons_usual(y, m, s))] = 2 + m + s 877.91/297.42 > 1 + s 877.91/297.42 = [Sum_sub(xi, s)] 877.91/297.42 877.91/297.42 [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 + s 877.91/297.42 >= 1 + s 877.91/297.42 = [Sum_sub(xi, s)] 877.91/297.42 877.91/297.42 [Sum_sub(xi, Cons_sum(psi, k, s))] = 1 + s 877.91/297.42 > 877.91/297.42 = [Sum_constant(k)] 877.91/297.42 877.91/297.42 [Concat(Id(), s)] = 1 + s 877.91/297.42 > s 877.91/297.42 = [s] 877.91/297.42 877.91/297.42 [Concat(Cons_usual(x, m, s), t)] = 3 + 2*m + 2*s + 3*t + 2*m*t + 2*s*t 877.91/297.42 >= 3 + 2*m + 2*m*t + 2*t + 2*s + 2*s*t 877.91/297.42 = [Cons_usual(x, Term_sub(m, t), Concat(s, t))] 877.91/297.42 877.91/297.42 [Concat(Cons_sum(xi, k, s), t)] = 1 + 2*s + 2*s*t + t 877.91/297.42 >= 1 + 2*s + 2*s*t + t 877.91/297.42 = [Cons_sum(xi, k, Concat(s, t))] 877.91/297.42 877.91/297.42 [Concat(Concat(s, t), u)] = 3 + 4*s + 4*s*t + 2*t + 3*u + 4*s*u + 4*s*t*u + 2*t*u 877.91/297.42 > 2 + 4*s + 4*s*t + 4*s*t*u + 2*s*u + 2*t + 2*t*u + u 877.91/297.42 = [Concat(s, Concat(t, u))] 877.91/297.42 877.91/297.42 877.91/297.42 We return to the main proof. 877.91/297.42 877.91/297.42 We are left with following problem, upon which TcT provides the 877.91/297.42 certificate YES(O(1),O(1)). 877.91/297.42 877.91/297.42 Weak Trs: 877.91/297.42 { Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)) 877.91/297.42 , Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s) 877.91/297.42 , Term_sub(Term_app(m, n), s) -> 877.91/297.42 Term_app(Term_sub(m, s), Term_sub(n, s)) 877.91/297.42 , Term_sub(Term_pair(m, n), s) -> 877.91/297.42 Term_pair(Term_sub(m, s), Term_sub(n, s)) 877.91/297.42 , Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s)) 877.91/297.42 , Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s)) 877.91/297.42 , Term_sub(Term_var(x), Id()) -> Term_var(x) 877.91/297.42 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m 877.91/297.42 , Term_sub(Term_var(x), Cons_usual(y, m, s)) -> 877.91/297.42 Term_sub(Term_var(x), s) 877.91/297.42 , Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> 877.91/297.42 Term_sub(Term_var(x), s) 877.91/297.42 , Frozen(m, Sum_constant(Left()), n, s) -> Term_sub(m, s) 877.91/297.42 , Frozen(m, Sum_constant(Right()), n, s) -> Term_sub(n, s) 877.91/297.42 , Frozen(m, Sum_term_var(xi), n, s) -> 877.91/297.42 Case(Term_sub(m, s), xi, Term_sub(n, s)) 877.91/297.42 , Sum_sub(xi, Id()) -> Sum_term_var(xi) 877.91/297.42 , Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s) 877.91/297.42 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s) 877.91/297.42 , Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k) 877.91/297.42 , Concat(Id(), s) -> s 877.91/297.42 , Concat(Cons_usual(x, m, s), t) -> 877.91/297.42 Cons_usual(x, Term_sub(m, t), Concat(s, t)) 877.91/297.42 , Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)) 877.91/297.42 , Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)) } 877.91/297.42 Obligation: 877.91/297.42 runtime complexity 877.91/297.42 Answer: 877.91/297.42 YES(O(1),O(1)) 877.91/297.42 877.91/297.42 Empty rules are trivially bounded 877.91/297.42 877.91/297.42 Hurray, we answered YES(O(1),O(n^2)) 878.16/297.65 EOF