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