WORST_CASE(Omega(n^1),O(n^3)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^3)) + Considered Problem: - Strict TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0 ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1} - Obligation: innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0 ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1} - Obligation: innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: Concat(z,u){z -> Cons_sum(x,y,z)} = Concat(Cons_sum(x,y,z),u) ->^+ Cons_sum(x,y,Concat(z,u)) = C[Concat(z,u) = Concat(z,u){}] ** Step 1.b:1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0 ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1} - Obligation: innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Concat#(Id(),s) -> c_4() Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8() Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)) Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)) Sum_sub#(xi,Id()) -> c_11() Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19() Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Id()) -> c_21() Weak DPs and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Concat#(Id(),s) -> c_4() Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8() Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)) Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)) Sum_sub#(xi,Id()) -> c_11() Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19() Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Id()) -> c_21() - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4,8,11,19,21} by application of Pre({4,8,11,19,21}) = {1,2,3,5,6,7,9,10,12,13,14,15,16,17,18,20}. Here rules are labelled as follows: 1: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) 2: Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) 3: Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) 4: Concat#(Id(),s) -> c_4() 5: Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) 6: Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) 7: Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) 8: Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8() 9: Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)) 10: Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)) 11: Sum_sub#(xi,Id()) -> c_11() 12: Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)) 13: Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) 14: Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) 15: Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) 16: Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) 17: Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) 18: Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)) 19: Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19() 20: Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)) 21: Term_sub#(Term_var(x),Id()) -> c_21() ** Step 1.b:3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)) Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)) Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)) - Weak DPs: Concat#(Id(),s) -> c_4() Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8() Sum_sub#(xi,Id()) -> c_11() Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19() Term_sub#(Term_var(x),Id()) -> c_21() - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) -->_2 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3 -->_1 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3 -->_2 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2 -->_1 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2 -->_2 Concat#(Id(),s) -> c_4():17 -->_1 Concat#(Id(),s) -> c_4():17 -->_2 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1 -->_1 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1 2:S:Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) -->_1 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3 -->_1 Concat#(Id(),s) -> c_4():17 -->_1 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2 -->_1 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1 3:S:Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9 -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 -->_2 Concat#(Id(),s) -> c_4():17 -->_2 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3 -->_2 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2 -->_2 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1 4:S:Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9 -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 5:S:Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9 -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 6:S:Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) -->_2 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_2 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 -->_2 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14 -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14 -->_2 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13 -->_2 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12 -->_2 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11 -->_2 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10 -->_2 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9 -->_2 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_2 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 7:S:Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)) -->_1 Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)):8 -->_1 Sum_sub#(xi,Id()) -> c_11():19 -->_1 Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8():18 -->_1 Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)):7 8:S:Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)) -->_1 Sum_sub#(xi,Id()) -> c_11():19 -->_1 Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8():18 -->_1 Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)):8 -->_1 Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)):7 9:S:Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)) -->_2 Sum_sub#(xi,Id()) -> c_11():19 -->_2 Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8():18 -->_2 Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)):8 -->_2 Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)):7 -->_1 Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)):6 -->_1 Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)):5 -->_1 Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)):4 10:S:Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) -->_2 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_2 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 -->_2 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14 -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14 -->_2 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13 -->_2 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12 -->_2 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11 -->_2 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_2 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 -->_2 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10 -->_2 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9 11:S:Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12 -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9 12:S:Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13 -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9 13:S:Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) -->_2 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_2 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 -->_2 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14 -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14 -->_2 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_2 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 -->_2 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13 -->_2 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12 -->_2 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11 -->_2 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10 -->_2 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9 14:S:Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 -->_2 Concat#(Id(),s) -> c_4():17 -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9 -->_2 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3 -->_2 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2 -->_2 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1 15:S:Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)) -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 16:S:Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)) -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20 -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16 -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15 17:W:Concat#(Id(),s) -> c_4() 18:W:Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8() 19:W:Sum_sub#(xi,Id()) -> c_11() 20:W:Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19() 21:W:Term_sub#(Term_var(x),Id()) -> c_21() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 18: Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8() 19: Sum_sub#(xi,Id()) -> c_11() 17: Concat#(Id(),s) -> c_4() 20: Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19() 21: Term_sub#(Term_var(x),Id()) -> c_21() ** Step 1.b:4: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)) Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)) Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) and a lower component Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)) Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)) Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)) Further, following extension rules are added to the lower component. Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s) Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) *** Step 1.b:4.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) -->_2 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3 -->_1 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3 -->_2 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2 -->_1 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2 -->_2 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1 -->_1 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1 2:S:Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) -->_1 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3 -->_1 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2 -->_1 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1 3:S:Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):12 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):11 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):10 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):9 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):8 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):7 -->_2 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3 -->_2 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2 -->_2 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1 4:S:Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):12 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):11 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):10 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):9 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):8 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):7 5:S:Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):12 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):11 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):10 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):9 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):8 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):7 6:S:Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) -->_2 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):12 -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):12 -->_2 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):11 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):11 -->_2 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):10 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):10 -->_2 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):9 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):9 -->_2 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):8 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):8 -->_2 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):7 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):7 7:S:Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)) -->_1 Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)):6 -->_1 Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)):5 -->_1 Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)):4 8:S:Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) -->_2 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):12 -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):12 -->_2 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):11 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):11 -->_2 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):10 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):10 -->_2 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):9 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):9 -->_2 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):8 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):8 -->_2 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):7 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):7 9:S:Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):12 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):11 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):10 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):9 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):8 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):7 10:S:Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):12 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):11 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):10 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):9 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):8 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):7 11:S:Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) -->_2 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):12 -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):12 -->_2 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):11 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):11 -->_2 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):10 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):10 -->_2 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):9 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):9 -->_2 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):8 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):8 -->_2 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):7 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):7 12:S:Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):12 -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):11 -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):10 -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):9 -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):8 -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):7 -->_2 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3 -->_2 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2 -->_2 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s)) *** Step 1.b:4.a:2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_2) = {1}, uargs(c_3) = {1,2}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1,2}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2} Following symbols are considered usable: {Sum_sub,Concat#,Frozen#,Sum_sub#,Term_sub#} TcT has computed the following interpretation: p(Case) = [1] x1 + [1] x2 + [1] x3 + [3] p(Concat) = [3] x1 + [3] x2 + [1] p(Cons_sum) = [1] x1 + [1] x3 + [0] p(Cons_usual) = [1] x2 + [1] x3 + [0] p(Frozen) = [4] x1 + [4] x4 + [6] p(Id) = [0] p(Left) = [4] p(Right) = [0] p(Sum_constant) = [4] p(Sum_sub) = [1] x1 + [6] p(Sum_term_var) = [2] p(Term_app) = [1] x1 + [1] x2 + [2] p(Term_inl) = [1] x1 + [1] p(Term_inr) = [1] x1 + [0] p(Term_pair) = [1] x1 + [1] x2 + [2] p(Term_sub) = [2] x1 + [2] x2 + [0] p(Term_var) = [1] p(Concat#) = [4] x1 + [0] p(Frozen#) = [4] x1 + [2] x2 + [4] x3 + [0] p(Sum_sub#) = [1] x1 + [4] p(Term_sub#) = [4] x1 + [0] p(c_1) = [1] x1 + [2] x2 + [3] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [1] x2 + [0] p(c_4) = [2] p(c_5) = [1] x1 + [1] p(c_6) = [1] x1 + [7] p(c_7) = [1] x1 + [1] x2 + [4] p(c_8) = [1] p(c_9) = [4] p(c_10) = [0] p(c_11) = [1] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [1] x2 + [6] p(c_14) = [1] x1 + [4] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [1] x2 + [4] p(c_17) = [1] x1 + [2] x2 + [0] p(c_18) = [1] x1 + [1] p(c_19) = [0] p(c_20) = [1] x1 + [0] p(c_21) = [0] Following rules are strictly oriented: Concat#(Concat(s,t),u) = [12] s + [12] t + [4] > [4] s + [8] t + [3] = c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Frozen#(m,Sum_constant(Left()),n,s) = [4] m + [4] n + [8] > [4] m + [1] = c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) = [4] m + [4] n + [8] > [4] n + [7] = c_6(Term_sub#(n,s)) Term_sub#(Term_app(m,n),s) = [4] m + [4] n + [8] > [4] m + [4] n + [6] = c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_pair(m,n),s) = [4] m + [4] n + [8] > [4] m + [4] n + [4] = c_16(Term_sub#(m,s),Term_sub#(n,s)) Following rules are (at-least) weakly oriented: Concat#(Cons_sum(xi,k,s),t) = [4] s + [4] xi + [0] >= [4] s + [0] = c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) = [4] m + [4] s + [0] >= [4] m + [4] s + [0] = c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_term_var(xi),n,s) = [4] m + [4] n + [4] >= [4] m + [4] n + [4] = c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) = [4] m + [4] n + [4] xi + [12] >= [4] m + [4] n + [2] xi + [12] = c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Term_sub#(Term_inl(m),s) = [4] m + [4] >= [4] m + [4] = c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) = [4] m + [0] >= [4] m + [0] = c_15(Term_sub#(m,s)) Term_sub#(Term_sub(m,s),t) = [8] m + [8] s + [0] >= [4] m + [8] s + [0] = c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) Sum_sub(xi,Cons_sum(psi,k,s)) = [1] xi + [6] >= [4] = Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) = [1] xi + [6] >= [1] xi + [6] = Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) = [1] xi + [6] >= [1] xi + [6] = Sum_sub(xi,s) Sum_sub(xi,Id()) = [1] xi + [6] >= [2] = Sum_term_var(xi) *** Step 1.b:4.a:3: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) - Weak DPs: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_2) = {1}, uargs(c_3) = {1,2}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1,2}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2} Following symbols are considered usable: {Concat#,Frozen#,Sum_sub#,Term_sub#} TcT has computed the following interpretation: p(Case) = [1] x1 + [1] x3 + [1] p(Concat) = [2] x1 + [1] x2 + [1] p(Cons_sum) = [1] x3 + [0] p(Cons_usual) = [1] x1 + [1] x2 + [1] x3 + [0] p(Frozen) = [1] x2 + [1] x3 + [2] p(Id) = [0] p(Left) = [2] p(Right) = [0] p(Sum_constant) = [2] p(Sum_sub) = [0] p(Sum_term_var) = [0] p(Term_app) = [1] x1 + [1] x2 + [0] p(Term_inl) = [1] x1 + [0] p(Term_inr) = [1] x1 + [0] p(Term_pair) = [1] x1 + [1] x2 + [1] p(Term_sub) = [2] x1 + [1] x2 + [0] p(Term_var) = [5] p(Concat#) = [4] x1 + [0] p(Frozen#) = [4] x1 + [4] x3 + [2] p(Sum_sub#) = [1] x1 + [4] x2 + [1] p(Term_sub#) = [4] x1 + [0] p(c_1) = [1] x1 + [1] x2 + [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [1] x2 + [0] p(c_4) = [1] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [2] p(c_7) = [1] x1 + [1] x2 + [1] p(c_8) = [1] p(c_9) = [1] p(c_10) = [1] p(c_11) = [2] p(c_12) = [1] x1 + [1] p(c_13) = [1] x1 + [1] x2 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [1] x2 + [2] p(c_17) = [2] x1 + [1] x2 + [0] p(c_18) = [1] x1 + [4] p(c_19) = [0] p(c_20) = [1] x1 + [4] p(c_21) = [1] Following rules are strictly oriented: Frozen#(m,Sum_term_var(xi),n,s) = [4] m + [4] n + [2] > [4] m + [4] n + [1] = c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) = [4] m + [4] n + [4] > [4] m + [4] n + [3] = c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Following rules are (at-least) weakly oriented: Concat#(Concat(s,t),u) = [8] s + [4] t + [4] >= [4] s + [4] t + [0] = c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) = [4] s + [0] >= [4] s + [0] = c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) = [4] m + [4] s + [4] x + [0] >= [4] m + [4] s + [0] = c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) = [4] m + [4] n + [2] >= [4] m + [0] = c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) = [4] m + [4] n + [2] >= [4] n + [2] = c_6(Term_sub#(n,s)) Term_sub#(Term_app(m,n),s) = [4] m + [4] n + [0] >= [4] m + [4] n + [0] = c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inl(m),s) = [4] m + [0] >= [4] m + [0] = c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) = [4] m + [0] >= [4] m + [0] = c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) = [4] m + [4] n + [4] >= [4] m + [4] n + [2] = c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) = [8] m + [4] s + [0] >= [8] m + [4] s + [0] = c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) *** Step 1.b:4.a:4: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) - Weak DPs: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_2) = {1}, uargs(c_3) = {1,2}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1,2}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2} Following symbols are considered usable: {Concat#,Frozen#,Sum_sub#,Term_sub#} TcT has computed the following interpretation: p(Case) = [1] x1 + [1] x2 + [1] x3 + [1] p(Concat) = [2] x1 + [1] x2 + [0] p(Cons_sum) = [1] x3 + [1] p(Cons_usual) = [1] x2 + [1] x3 + [0] p(Frozen) = [4] x2 + [1] x3 + [2] p(Id) = [0] p(Left) = [0] p(Right) = [2] p(Sum_constant) = [2] p(Sum_sub) = [0] p(Sum_term_var) = [2] p(Term_app) = [1] x1 + [1] x2 + [1] p(Term_inl) = [1] x1 + [0] p(Term_inr) = [1] x1 + [0] p(Term_pair) = [1] x1 + [1] x2 + [2] p(Term_sub) = [1] x1 + [2] x2 + [0] p(Term_var) = [0] p(Concat#) = [4] x1 + [0] p(Frozen#) = [4] x1 + [4] x3 + [4] p(Sum_sub#) = [0] p(Term_sub#) = [4] x1 + [0] p(c_1) = [2] x1 + [1] x2 + [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [1] x2 + [0] p(c_4) = [2] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [1] p(c_7) = [1] x1 + [1] x2 + [2] p(c_8) = [0] p(c_9) = [1] x1 + [2] p(c_10) = [2] x1 + [0] p(c_11) = [0] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [1] x2 + [1] p(c_14) = [1] x1 + [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [1] x2 + [7] p(c_17) = [1] x1 + [2] x2 + [0] p(c_18) = [1] p(c_19) = [2] p(c_20) = [2] x1 + [1] p(c_21) = [4] Following rules are strictly oriented: Concat#(Cons_sum(xi,k,s),t) = [4] s + [4] > [4] s + [0] = c_2(Concat#(s,t)) Following rules are (at-least) weakly oriented: Concat#(Concat(s,t),u) = [8] s + [4] t + [0] >= [8] s + [4] t + [0] = c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_usual(x,m,s),t) = [4] m + [4] s + [0] >= [4] m + [4] s + [0] = c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) = [4] m + [4] n + [4] >= [4] m + [0] = c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) = [4] m + [4] n + [4] >= [4] n + [1] = c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) = [4] m + [4] n + [4] >= [4] m + [4] n + [2] = c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) = [4] m + [4] n + [4] xi + [4] >= [4] m + [4] n + [4] = c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Term_sub#(Term_app(m,n),s) = [4] m + [4] n + [4] >= [4] m + [4] n + [1] = c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inl(m),s) = [4] m + [0] >= [4] m + [0] = c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) = [4] m + [0] >= [4] m + [0] = c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) = [4] m + [4] n + [8] >= [4] m + [4] n + [7] = c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) = [4] m + [8] s + [0] >= [4] m + [8] s + [0] = c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) *** Step 1.b:4.a:5: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) - Weak DPs: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_2) = {1}, uargs(c_3) = {1,2}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1,2}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2} Following symbols are considered usable: {Concat#,Frozen#,Sum_sub#,Term_sub#} TcT has computed the following interpretation: p(Case) = [1] x1 + [1] x2 + [1] x3 + [2] p(Concat) = [1] x1 + [2] x2 + [2] p(Cons_sum) = [1] x3 + [0] p(Cons_usual) = [1] x2 + [1] x3 + [0] p(Frozen) = [1] x3 + [6] p(Id) = [1] p(Left) = [0] p(Right) = [1] p(Sum_constant) = [0] p(Sum_sub) = [2] x2 + [1] p(Sum_term_var) = [0] p(Term_app) = [1] x1 + [1] x2 + [0] p(Term_inl) = [1] x1 + [0] p(Term_inr) = [1] x1 + [4] p(Term_pair) = [1] x1 + [1] x2 + [4] p(Term_sub) = [1] x1 + [4] x2 + [5] p(Term_var) = [4] p(Concat#) = [4] x1 + [0] p(Frozen#) = [2] x1 + [2] x3 + [0] p(Sum_sub#) = [4] x1 + [2] x2 + [4] p(Term_sub#) = [2] x1 + [0] p(c_1) = [1] x1 + [1] x2 + [1] p(c_2) = [1] x1 + [0] p(c_3) = [2] x1 + [1] x2 + [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [1] p(c_10) = [2] x1 + [0] p(c_11) = [1] p(c_12) = [1] x1 + [4] p(c_13) = [1] x1 + [1] x2 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [1] x1 + [6] p(c_16) = [1] x1 + [1] x2 + [6] p(c_17) = [1] x1 + [2] x2 + [6] p(c_18) = [1] x1 + [1] p(c_19) = [2] p(c_20) = [1] x1 + [1] p(c_21) = [1] Following rules are strictly oriented: Term_sub#(Term_inr(m),s) = [2] m + [8] > [2] m + [6] = c_15(Term_sub#(m,s)) Term_sub#(Term_sub(m,s),t) = [2] m + [8] s + [10] > [2] m + [8] s + [6] = c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) Following rules are (at-least) weakly oriented: Concat#(Concat(s,t),u) = [4] s + [8] t + [8] >= [4] s + [4] t + [1] = c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) = [4] s + [0] >= [4] s + [0] = c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) = [4] m + [4] s + [0] >= [4] m + [4] s + [0] = c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) = [2] m + [2] n + [0] >= [2] m + [0] = c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) = [2] m + [2] n + [0] >= [2] n + [0] = c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) = [2] m + [2] n + [0] >= [2] m + [2] n + [0] = c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) = [2] m + [2] n + [2] xi + [4] >= [2] m + [2] n + [4] = c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Term_sub#(Term_app(m,n),s) = [2] m + [2] n + [0] >= [2] m + [2] n + [0] = c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inl(m),s) = [2] m + [0] >= [2] m + [0] = c_14(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) = [2] m + [2] n + [8] >= [2] m + [2] n + [6] = c_16(Term_sub#(m,s),Term_sub#(n,s)) *** Step 1.b:4.a:6: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) - Weak DPs: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_2) = {1}, uargs(c_3) = {1,2}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1,2}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2} Following symbols are considered usable: {Concat#,Frozen#,Sum_sub#,Term_sub#} TcT has computed the following interpretation: p(Case) = [1] x1 + [1] x2 + [1] x3 + [2] p(Concat) = [1] x1 + [2] x2 + [3] p(Cons_sum) = [1] x1 + [1] x2 + [1] x3 + [0] p(Cons_usual) = [1] x1 + [1] x2 + [1] x3 + [2] p(Frozen) = [0] p(Id) = [0] p(Left) = [0] p(Right) = [0] p(Sum_constant) = [1] x1 + [0] p(Sum_sub) = [0] p(Sum_term_var) = [1] x1 + [0] p(Term_app) = [1] x1 + [1] x2 + [0] p(Term_inl) = [1] x1 + [0] p(Term_inr) = [1] x1 + [0] p(Term_pair) = [1] x1 + [1] x2 + [2] p(Term_sub) = [2] x1 + [1] x2 + [0] p(Term_var) = [1] x1 + [0] p(Concat#) = [4] x1 + [0] p(Frozen#) = [4] x1 + [4] x3 + [2] p(Sum_sub#) = [0] p(Term_sub#) = [4] x1 + [0] p(c_1) = [1] x1 + [1] x2 + [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [1] x2 + [6] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [1] x1 + [4] p(c_13) = [1] x1 + [1] x2 + [0] p(c_14) = [1] x1 + [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [1] x2 + [3] p(c_17) = [2] x1 + [1] x2 + [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] Following rules are strictly oriented: Concat#(Cons_usual(x,m,s),t) = [4] m + [4] s + [4] x + [8] > [4] m + [4] s + [6] = c_3(Term_sub#(m,t),Concat#(s,t)) Following rules are (at-least) weakly oriented: Concat#(Concat(s,t),u) = [4] s + [8] t + [12] >= [4] s + [4] t + [0] = c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) = [4] k + [4] s + [4] xi + [0] >= [4] s + [0] = c_2(Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) = [4] m + [4] n + [2] >= [4] m + [0] = c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) = [4] m + [4] n + [2] >= [4] n + [0] = c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) = [4] m + [4] n + [2] >= [4] m + [4] n + [0] = c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) = [4] m + [4] n + [4] xi + [8] >= [4] m + [4] n + [6] = c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Term_sub#(Term_app(m,n),s) = [4] m + [4] n + [0] >= [4] m + [4] n + [0] = c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inl(m),s) = [4] m + [0] >= [4] m + [0] = c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) = [4] m + [0] >= [4] m + [0] = c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) = [4] m + [4] n + [8] >= [4] m + [4] n + [3] = c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) = [8] m + [4] s + [0] >= [8] m + [4] s + [0] = c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) *** Step 1.b:4.a:7: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) - Weak DPs: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1,2}, uargs(c_2) = {1}, uargs(c_3) = {1,2}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1,2}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1,2}, uargs(c_17) = {1,2} Following symbols are considered usable: {Concat#,Frozen#,Sum_sub#,Term_sub#} TcT has computed the following interpretation: p(Case) = [1] x1 + [1] x3 + [0] p(Concat) = [3] x1 + [3] x2 + [0] p(Cons_sum) = [1] x1 + [1] x2 + [1] x3 + [0] p(Cons_usual) = [1] x1 + [1] x2 + [1] x3 + [3] p(Frozen) = [2] x2 + [0] p(Id) = [0] p(Left) = [0] p(Right) = [0] p(Sum_constant) = [1] x1 + [0] p(Sum_sub) = [4] x2 + [3] p(Sum_term_var) = [1] x1 + [0] p(Term_app) = [1] x1 + [1] x2 + [2] p(Term_inl) = [1] x1 + [2] p(Term_inr) = [1] x1 + [1] p(Term_pair) = [1] x1 + [1] x2 + [0] p(Term_sub) = [2] x1 + [1] x2 + [0] p(Term_var) = [1] x1 + [0] p(Concat#) = [2] x1 + [0] p(Frozen#) = [2] x1 + [2] x3 + [0] p(Sum_sub#) = [0] p(Term_sub#) = [2] x1 + [0] p(c_1) = [2] x1 + [2] x2 + [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [1] x2 + [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [1] x2 + [4] p(c_14) = [1] x1 + [0] p(c_15) = [1] x1 + [2] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [2] x1 + [1] x2 + [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] Following rules are strictly oriented: Term_sub#(Term_inl(m),s) = [2] m + [4] > [2] m + [0] = c_14(Term_sub#(m,s)) Following rules are (at-least) weakly oriented: Concat#(Concat(s,t),u) = [6] s + [6] t + [0] >= [4] s + [4] t + [0] = c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) = [2] k + [2] s + [2] xi + [0] >= [2] s + [0] = c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) = [2] m + [2] s + [2] x + [6] >= [2] m + [2] s + [0] = c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) = [2] m + [2] n + [0] >= [2] m + [0] = c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) = [2] m + [2] n + [0] >= [2] n + [0] = c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) = [2] m + [2] n + [0] >= [2] m + [2] n + [0] = c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) = [2] m + [2] n + [0] >= [2] m + [2] n + [0] = c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Term_sub#(Term_app(m,n),s) = [2] m + [2] n + [4] >= [2] m + [2] n + [4] = c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inr(m),s) = [2] m + [2] >= [2] m + [2] = c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) = [2] m + [2] n + [0] >= [2] m + [2] n + [0] = c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) = [4] m + [2] s + [0] >= [4] m + [2] s + [0] = c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) *** Step 1.b:4.a:8: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)) Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)) Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)) Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)) Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)) Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s)) Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)) Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)) Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)) Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/1,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:4.b:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)) Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)) Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)) - Weak DPs: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s) Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_18) = {1}, uargs(c_20) = {1} Following symbols are considered usable: {Concat,Frozen,Sum_sub,Term_sub,Concat#,Frozen#,Sum_sub#,Term_sub#} TcT has computed the following interpretation: p(Case) = 1 + x1 + x3 p(Concat) = x1 + x1*x2 + x2 p(Cons_sum) = x1 + x3 p(Cons_usual) = 1 + x2 + x3 p(Frozen) = 1 + x1 + x1*x4 + x2*x4 + x3 + x3*x4 + x4 p(Id) = 0 p(Left) = 0 p(Right) = 0 p(Sum_constant) = 0 p(Sum_sub) = 1 p(Sum_term_var) = 1 p(Term_app) = 1 + x1 + x2 p(Term_inl) = x1 p(Term_inr) = x1 p(Term_pair) = 1 + x1 + x2 p(Term_sub) = x1 + x1*x2 + x2 p(Term_var) = 0 p(Concat#) = x1 + x1*x2 p(Frozen#) = x1 + x1*x4 + x3 + x3*x4 + x4 p(Sum_sub#) = x2 p(Term_sub#) = x1 + x1*x2 p(c_1) = 0 p(c_2) = 0 p(c_3) = 0 p(c_4) = 0 p(c_5) = 0 p(c_6) = 0 p(c_7) = 0 p(c_8) = 0 p(c_9) = x1 p(c_10) = x1 p(c_11) = 0 p(c_12) = 0 p(c_13) = 0 p(c_14) = 0 p(c_15) = 0 p(c_16) = 0 p(c_17) = 0 p(c_18) = x1 p(c_19) = 0 p(c_20) = x1 p(c_21) = 0 Following rules are strictly oriented: Sum_sub#(xi,Cons_usual(y,m,s)) = 1 + m + s > s = c_10(Sum_sub#(xi,s)) Following rules are (at-least) weakly oriented: Concat#(Concat(s,t),u) = s + s*t + s*t*u + s*u + t + t*u >= s + s*t + s*t*u + s*u = Concat#(s,Concat(t,u)) Concat#(Concat(s,t),u) = s + s*t + s*t*u + s*u + t + t*u >= t + t*u = Concat#(t,u) Concat#(Cons_sum(xi,k,s),t) = s + s*t + t*xi + xi >= s + s*t = Concat#(s,t) Concat#(Cons_usual(x,m,s),t) = 1 + m + m*t + s + s*t + t >= s + s*t = Concat#(s,t) Concat#(Cons_usual(x,m,s),t) = 1 + m + m*t + s + s*t + t >= m + m*t = Term_sub#(m,t) Frozen#(m,Sum_constant(Left()),n,s) = m + m*s + n + n*s + s >= m + m*s = Term_sub#(m,s) Frozen#(m,Sum_constant(Right()),n,s) = m + m*s + n + n*s + s >= n + n*s = Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) = m + m*s + n + n*s + s >= m + m*s = Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) = m + m*s + n + n*s + s >= n + n*s = Term_sub#(n,s) Sum_sub#(xi,Cons_sum(psi,k,s)) = psi + s >= s = c_9(Sum_sub#(xi,s)) Term_sub#(Case(m,xi,n),s) = 1 + m + m*s + n + n*s + s >= m + m*s + n + n*s + s = Frozen#(m,Sum_sub(xi,s),n,s) Term_sub#(Case(m,xi,n),s) = 1 + m + m*s + n + n*s + s >= s = Sum_sub#(xi,s) Term_sub#(Term_app(m,n),s) = 1 + m + m*s + n + n*s + s >= m + m*s = Term_sub#(m,s) Term_sub#(Term_app(m,n),s) = 1 + m + m*s + n + n*s + s >= n + n*s = Term_sub#(n,s) Term_sub#(Term_inl(m),s) = m + m*s >= m + m*s = Term_sub#(m,s) Term_sub#(Term_inr(m),s) = m + m*s >= m + m*s = Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) = 1 + m + m*s + n + n*s + s >= m + m*s = Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) = 1 + m + m*s + n + n*s + s >= n + n*s = Term_sub#(n,s) Term_sub#(Term_sub(m,s),t) = m + m*s + m*s*t + m*t + s + s*t >= s + s*t = Concat#(s,t) Term_sub#(Term_sub(m,s),t) = m + m*s + m*s*t + m*t + s + s*t >= m + m*s + m*s*t + m*t = Term_sub#(m,Concat(s,t)) Term_sub#(Term_var(x),Cons_sum(xi,k,s)) = 0 >= 0 = c_18(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) = 0 >= 0 = c_20(Term_sub#(Term_var(x),s)) Concat(Concat(s,t),u) = s + s*t + s*t*u + s*u + t + t*u + u >= s + s*t + s*t*u + s*u + t + t*u + u = Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) = s + s*t + t + t*xi + xi >= s + s*t + t + xi = Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) = 1 + m + m*t + s + s*t + 2*t >= 1 + m + m*t + s + s*t + 2*t = Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) = s >= s = s Frozen(m,Sum_constant(Left()),n,s) = 1 + m + m*s + n + n*s + s >= m + m*s + s = Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) = 1 + m + m*s + n + n*s + s >= n + n*s + s = Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) = 1 >= 0 = Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) = 1 >= 1 = Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) = 1 >= 1 = Sum_sub(xi,s) Sum_sub(xi,Id()) = 1 >= 1 = Sum_term_var(xi) Term_sub(Case(m,xi,n),s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) = m + m*s + s >= m + m*s + s = Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) = m + m*s + s >= m + m*s + s = Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) = m + m*s + m*s*t + m*t + s + s*t + t >= m + m*s + m*s*t + m*t + s + s*t + t = Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) = s + xi >= s = Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + s >= m = m Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + s >= s = Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) = 0 >= 0 = Term_var(x) *** Step 1.b:4.b:2: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)) Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)) - Weak DPs: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)) Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s) Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_18) = {1}, uargs(c_20) = {1} Following symbols are considered usable: {Concat,Frozen,Sum_sub,Term_sub,Concat#,Frozen#,Sum_sub#,Term_sub#} TcT has computed the following interpretation: p(Case) = 1 + x1 + x3 p(Concat) = x1 + x1*x2 + x2 p(Cons_sum) = 1 + x1 + x3 p(Cons_usual) = 1 + x2 + x3 p(Frozen) = 1 + x1 + x1*x4 + x2*x4 + x3 + x3*x4 + x4 p(Id) = 0 p(Left) = 0 p(Right) = 0 p(Sum_constant) = 1 p(Sum_sub) = 1 p(Sum_term_var) = 1 p(Term_app) = 1 + x1 + x2 p(Term_inl) = x1 p(Term_inr) = 1 + x1 p(Term_pair) = 1 + x1 + x2 p(Term_sub) = x1 + x1*x2 + x2 p(Term_var) = 0 p(Concat#) = x1 + x1*x2 p(Frozen#) = x1*x2 + x1*x4 + x2*x4 + x3 + x3*x4 p(Sum_sub#) = x2 p(Term_sub#) = x1 + x1*x2 p(c_1) = 0 p(c_2) = 0 p(c_3) = 0 p(c_4) = 0 p(c_5) = 0 p(c_6) = 0 p(c_7) = 0 p(c_8) = 0 p(c_9) = x1 p(c_10) = x1 p(c_11) = 0 p(c_12) = 0 p(c_13) = 0 p(c_14) = 0 p(c_15) = 0 p(c_16) = 0 p(c_17) = 0 p(c_18) = x1 p(c_19) = 0 p(c_20) = x1 p(c_21) = 0 Following rules are strictly oriented: Sum_sub#(xi,Cons_sum(psi,k,s)) = 1 + psi + s > s = c_9(Sum_sub#(xi,s)) Following rules are (at-least) weakly oriented: Concat#(Concat(s,t),u) = s + s*t + s*t*u + s*u + t + t*u >= s + s*t + s*t*u + s*u = Concat#(s,Concat(t,u)) Concat#(Concat(s,t),u) = s + s*t + s*t*u + s*u + t + t*u >= t + t*u = Concat#(t,u) Concat#(Cons_sum(xi,k,s),t) = 1 + s + s*t + t + t*xi + xi >= s + s*t = Concat#(s,t) Concat#(Cons_usual(x,m,s),t) = 1 + m + m*t + s + s*t + t >= s + s*t = Concat#(s,t) Concat#(Cons_usual(x,m,s),t) = 1 + m + m*t + s + s*t + t >= m + m*t = Term_sub#(m,t) Frozen#(m,Sum_constant(Left()),n,s) = m + m*s + n + n*s + s >= m + m*s = Term_sub#(m,s) Frozen#(m,Sum_constant(Right()),n,s) = m + m*s + n + n*s + s >= n + n*s = Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) = m + m*s + n + n*s + s >= m + m*s = Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) = m + m*s + n + n*s + s >= n + n*s = Term_sub#(n,s) Sum_sub#(xi,Cons_usual(y,m,s)) = 1 + m + s >= s = c_10(Sum_sub#(xi,s)) Term_sub#(Case(m,xi,n),s) = 1 + m + m*s + n + n*s + s >= m + m*s + n + n*s + s = Frozen#(m,Sum_sub(xi,s),n,s) Term_sub#(Case(m,xi,n),s) = 1 + m + m*s + n + n*s + s >= s = Sum_sub#(xi,s) Term_sub#(Term_app(m,n),s) = 1 + m + m*s + n + n*s + s >= m + m*s = Term_sub#(m,s) Term_sub#(Term_app(m,n),s) = 1 + m + m*s + n + n*s + s >= n + n*s = Term_sub#(n,s) Term_sub#(Term_inl(m),s) = m + m*s >= m + m*s = Term_sub#(m,s) Term_sub#(Term_inr(m),s) = 1 + m + m*s + s >= m + m*s = Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) = 1 + m + m*s + n + n*s + s >= m + m*s = Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) = 1 + m + m*s + n + n*s + s >= n + n*s = Term_sub#(n,s) Term_sub#(Term_sub(m,s),t) = m + m*s + m*s*t + m*t + s + s*t >= s + s*t = Concat#(s,t) Term_sub#(Term_sub(m,s),t) = m + m*s + m*s*t + m*t + s + s*t >= m + m*s + m*s*t + m*t = Term_sub#(m,Concat(s,t)) Term_sub#(Term_var(x),Cons_sum(xi,k,s)) = 0 >= 0 = c_18(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) = 0 >= 0 = c_20(Term_sub#(Term_var(x),s)) Concat(Concat(s,t),u) = s + s*t + s*t*u + s*u + t + t*u + u >= s + s*t + s*t*u + s*u + t + t*u + u = Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) = 1 + s + s*t + 2*t + t*xi + xi >= 1 + s + s*t + t + xi = Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) = 1 + m + m*t + s + s*t + 2*t >= 1 + m + m*t + s + s*t + 2*t = Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) = s >= s = s Frozen(m,Sum_constant(Left()),n,s) = 1 + m + m*s + n + n*s + 2*s >= m + m*s + s = Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) = 1 + m + m*s + n + n*s + 2*s >= n + n*s + s = Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) = 1 >= 1 = Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) = 1 >= 1 = Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) = 1 >= 1 = Sum_sub(xi,s) Sum_sub(xi,Id()) = 1 >= 1 = Sum_term_var(xi) Term_sub(Case(m,xi,n),s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) = m + m*s + s >= m + m*s + s = Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) = 1 + m + m*s + 2*s >= 1 + m + m*s + s = Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) = m + m*s + m*s*t + m*t + s + s*t + t >= m + m*s + m*s*t + m*t + s + s*t + t = Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) = 1 + s + xi >= s = Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + s >= m = m Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + s >= s = Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) = 0 >= 0 = Term_var(x) *** Step 1.b:4.b:3: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)) - Weak DPs: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)) Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)) Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s) Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_18) = {1}, uargs(c_20) = {1} Following symbols are considered usable: {Concat,Frozen,Sum_sub,Term_sub,Concat#,Frozen#,Sum_sub#,Term_sub#} TcT has computed the following interpretation: p(Case) = 1 + x1 + x2 + x3 p(Concat) = x1 + x1*x2 + x2 p(Cons_sum) = x1 + x3 p(Cons_usual) = 1 + x2 + x3 p(Frozen) = x1 + x1*x4 + x2 + x2*x4 + x3 + x3*x4 + x4 p(Id) = 0 p(Left) = 0 p(Right) = 0 p(Sum_constant) = 0 p(Sum_sub) = 1 + x1 p(Sum_term_var) = 1 + x1 p(Term_app) = 1 + x1 + x2 p(Term_inl) = x1 p(Term_inr) = x1 p(Term_pair) = 1 + x1 + x2 p(Term_sub) = x1 + x1*x2 + x2 p(Term_var) = 0 p(Concat#) = x1 + x1*x2 p(Frozen#) = x1 + x1*x4 + x2*x4 + x3 + x3*x4 + x4 p(Sum_sub#) = 0 p(Term_sub#) = x1 + x1*x2 + x2 p(c_1) = 0 p(c_2) = 0 p(c_3) = 0 p(c_4) = 0 p(c_5) = 0 p(c_6) = 0 p(c_7) = 0 p(c_8) = 0 p(c_9) = x1 p(c_10) = x1 p(c_11) = 0 p(c_12) = 0 p(c_13) = 0 p(c_14) = 0 p(c_15) = 0 p(c_16) = 0 p(c_17) = 0 p(c_18) = x1 p(c_19) = 0 p(c_20) = x1 p(c_21) = 0 Following rules are strictly oriented: Term_sub#(Term_var(x),Cons_usual(y,m,s)) = 1 + m + s > s = c_20(Term_sub#(Term_var(x),s)) Following rules are (at-least) weakly oriented: Concat#(Concat(s,t),u) = s + s*t + s*t*u + s*u + t + t*u >= s + s*t + s*t*u + s*u = Concat#(s,Concat(t,u)) Concat#(Concat(s,t),u) = s + s*t + s*t*u + s*u + t + t*u >= t + t*u = Concat#(t,u) Concat#(Cons_sum(xi,k,s),t) = s + s*t + t*xi + xi >= s + s*t = Concat#(s,t) Concat#(Cons_usual(x,m,s),t) = 1 + m + m*t + s + s*t + t >= s + s*t = Concat#(s,t) Concat#(Cons_usual(x,m,s),t) = 1 + m + m*t + s + s*t + t >= m + m*t + t = Term_sub#(m,t) Frozen#(m,Sum_constant(Left()),n,s) = m + m*s + n + n*s + s >= m + m*s + s = Term_sub#(m,s) Frozen#(m,Sum_constant(Right()),n,s) = m + m*s + n + n*s + s >= n + n*s + s = Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) = m + m*s + n + n*s + 2*s + s*xi >= m + m*s + s = Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) = m + m*s + n + n*s + 2*s + s*xi >= n + n*s + s = Term_sub#(n,s) Sum_sub#(xi,Cons_sum(psi,k,s)) = 0 >= 0 = c_9(Sum_sub#(xi,s)) Sum_sub#(xi,Cons_usual(y,m,s)) = 0 >= 0 = c_10(Sum_sub#(xi,s)) Term_sub#(Case(m,xi,n),s) = 1 + m + m*s + n + n*s + 2*s + s*xi + xi >= m + m*s + n + n*s + 2*s + s*xi = Frozen#(m,Sum_sub(xi,s),n,s) Term_sub#(Case(m,xi,n),s) = 1 + m + m*s + n + n*s + 2*s + s*xi + xi >= 0 = Sum_sub#(xi,s) Term_sub#(Term_app(m,n),s) = 1 + m + m*s + n + n*s + 2*s >= m + m*s + s = Term_sub#(m,s) Term_sub#(Term_app(m,n),s) = 1 + m + m*s + n + n*s + 2*s >= n + n*s + s = Term_sub#(n,s) Term_sub#(Term_inl(m),s) = m + m*s + s >= m + m*s + s = Term_sub#(m,s) Term_sub#(Term_inr(m),s) = m + m*s + s >= m + m*s + s = Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) = 1 + m + m*s + n + n*s + 2*s >= m + m*s + s = Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) = 1 + m + m*s + n + n*s + 2*s >= n + n*s + s = Term_sub#(n,s) Term_sub#(Term_sub(m,s),t) = m + m*s + m*s*t + m*t + s + s*t + t >= s + s*t = Concat#(s,t) Term_sub#(Term_sub(m,s),t) = m + m*s + m*s*t + m*t + s + s*t + t >= m + m*s + m*s*t + m*t + s + s*t + t = Term_sub#(m,Concat(s,t)) Term_sub#(Term_var(x),Cons_sum(xi,k,s)) = s + xi >= s = c_18(Term_sub#(Term_var(x),s)) Concat(Concat(s,t),u) = s + s*t + s*t*u + s*u + t + t*u + u >= s + s*t + s*t*u + s*u + t + t*u + u = Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) = s + s*t + t + t*xi + xi >= s + s*t + t + xi = Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) = 1 + m + m*t + s + s*t + 2*t >= 1 + m + m*t + s + s*t + 2*t = Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) = s >= s = s Frozen(m,Sum_constant(Left()),n,s) = m + m*s + n + n*s + s >= m + m*s + s = Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) = m + m*s + n + n*s + s >= n + n*s + s = Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) = 1 + m + m*s + n + n*s + 2*s + s*xi + xi >= 1 + m + m*s + n + n*s + 2*s + xi = Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) = 1 + xi >= 0 = Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) = 1 + xi >= 1 + xi = Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) = 1 + xi >= 1 + xi = Sum_sub(xi,s) Sum_sub(xi,Id()) = 1 + xi >= 1 + xi = Sum_term_var(xi) Term_sub(Case(m,xi,n),s) = 1 + m + m*s + n + n*s + 2*s + s*xi + xi >= 1 + m + m*s + n + n*s + 2*s + s*xi + xi = Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) = m + m*s + s >= m + m*s + s = Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) = m + m*s + s >= m + m*s + s = Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) = m + m*s + m*s*t + m*t + s + s*t + t >= m + m*s + m*s*t + m*t + s + s*t + t = Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) = s + xi >= s = Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + s >= m = m Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + s >= s = Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) = 0 >= 0 = Term_var(x) *** Step 1.b:4.b:4: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)) - Weak DPs: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)) Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)) Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s) Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_18) = {1}, uargs(c_20) = {1} Following symbols are considered usable: {Concat,Frozen,Sum_sub,Term_sub,Concat#,Frozen#,Sum_sub#,Term_sub#} TcT has computed the following interpretation: p(Case) = 1 + x1 + x3 p(Concat) = x1 + x1*x2 + x2 p(Cons_sum) = 1 + x1 + x3 p(Cons_usual) = 1 + x1 + x2 + x3 p(Frozen) = x1 + x1*x4 + x2*x4 + x2^2 + x3 + x3*x4 + x4 p(Id) = 0 p(Left) = 0 p(Right) = 0 p(Sum_constant) = 1 p(Sum_sub) = 1 p(Sum_term_var) = 1 p(Term_app) = 1 + x1 + x2 p(Term_inl) = x1 p(Term_inr) = x1 p(Term_pair) = 1 + x1 + x2 p(Term_sub) = x1 + x1*x2 + x2 p(Term_var) = x1 p(Concat#) = x1*x2 + x1^2 p(Frozen#) = x1 + x1*x2 + x1*x4 + x1^2 + x2*x4 + x3 + x3*x4 + x3^2 p(Sum_sub#) = x2 p(Term_sub#) = x1 + x1*x2 + x1^2 + x2 p(c_1) = 0 p(c_2) = 0 p(c_3) = 0 p(c_4) = 0 p(c_5) = 0 p(c_6) = 0 p(c_7) = 0 p(c_8) = 0 p(c_9) = 1 + x1 p(c_10) = 1 + x1 p(c_11) = 0 p(c_12) = 0 p(c_13) = 0 p(c_14) = 0 p(c_15) = 0 p(c_16) = 0 p(c_17) = 0 p(c_18) = x1 p(c_19) = 0 p(c_20) = x1 p(c_21) = 0 Following rules are strictly oriented: Term_sub#(Term_var(x),Cons_sum(xi,k,s)) = 1 + s + s*x + 2*x + x*xi + x^2 + xi > s + s*x + x + x^2 = c_18(Term_sub#(Term_var(x),s)) Following rules are (at-least) weakly oriented: Concat#(Concat(s,t),u) = 2*s*t + s*t*u + 2*s*t^2 + s*u + s^2 + 2*s^2*t + s^2*t^2 + t*u + t^2 >= s*t + s*t*u + s*u + s^2 = Concat#(s,Concat(t,u)) Concat#(Concat(s,t),u) = 2*s*t + s*t*u + 2*s*t^2 + s*u + s^2 + 2*s^2*t + s^2*t^2 + t*u + t^2 >= t*u + t^2 = Concat#(t,u) Concat#(Cons_sum(xi,k,s),t) = 1 + 2*s + s*t + 2*s*xi + s^2 + t + t*xi + 2*xi + xi^2 >= s*t + s^2 = Concat#(s,t) Concat#(Cons_usual(x,m,s),t) = 1 + 2*m + 2*m*s + m*t + 2*m*x + m^2 + 2*s + s*t + 2*s*x + s^2 + t + t*x + 2*x + x^2 >= s*t + s^2 = Concat#(s,t) Concat#(Cons_usual(x,m,s),t) = 1 + 2*m + 2*m*s + m*t + 2*m*x + m^2 + 2*s + s*t + 2*s*x + s^2 + t + t*x + 2*x + x^2 >= m + m*t + m^2 + t = Term_sub#(m,t) Frozen#(m,Sum_constant(Left()),n,s) = 2*m + m*s + m^2 + n + n*s + n^2 + s >= m + m*s + m^2 + s = Term_sub#(m,s) Frozen#(m,Sum_constant(Right()),n,s) = 2*m + m*s + m^2 + n + n*s + n^2 + s >= n + n*s + n^2 + s = Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) = 2*m + m*s + m^2 + n + n*s + n^2 + s >= m + m*s + m^2 + s = Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) = 2*m + m*s + m^2 + n + n*s + n^2 + s >= n + n*s + n^2 + s = Term_sub#(n,s) Sum_sub#(xi,Cons_sum(psi,k,s)) = 1 + psi + s >= 1 + s = c_9(Sum_sub#(xi,s)) Sum_sub#(xi,Cons_usual(y,m,s)) = 1 + m + s + y >= 1 + s = c_10(Sum_sub#(xi,s)) Term_sub#(Case(m,xi,n),s) = 2 + 3*m + 2*m*n + m*s + m^2 + 3*n + n*s + n^2 + 2*s >= 2*m + m*s + m^2 + n + n*s + n^2 + s = Frozen#(m,Sum_sub(xi,s),n,s) Term_sub#(Case(m,xi,n),s) = 2 + 3*m + 2*m*n + m*s + m^2 + 3*n + n*s + n^2 + 2*s >= s = Sum_sub#(xi,s) Term_sub#(Term_app(m,n),s) = 2 + 3*m + 2*m*n + m*s + m^2 + 3*n + n*s + n^2 + 2*s >= m + m*s + m^2 + s = Term_sub#(m,s) Term_sub#(Term_app(m,n),s) = 2 + 3*m + 2*m*n + m*s + m^2 + 3*n + n*s + n^2 + 2*s >= n + n*s + n^2 + s = Term_sub#(n,s) Term_sub#(Term_inl(m),s) = m + m*s + m^2 + s >= m + m*s + m^2 + s = Term_sub#(m,s) Term_sub#(Term_inr(m),s) = m + m*s + m^2 + s >= m + m*s + m^2 + s = Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) = 2 + 3*m + 2*m*n + m*s + m^2 + 3*n + n*s + n^2 + 2*s >= m + m*s + m^2 + s = Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) = 2 + 3*m + 2*m*n + m*s + m^2 + 3*n + n*s + n^2 + 2*s >= n + n*s + n^2 + s = Term_sub#(n,s) Term_sub#(Term_sub(m,s),t) = m + 3*m*s + m*s*t + 2*m*s^2 + m*t + m^2 + 2*m^2*s + m^2*s^2 + s + s*t + s^2 + t >= s*t + s^2 = Concat#(s,t) Term_sub#(Term_sub(m,s),t) = m + 3*m*s + m*s*t + 2*m*s^2 + m*t + m^2 + 2*m^2*s + m^2*s^2 + s + s*t + s^2 + t >= m + m*s + m*s*t + m*t + m^2 + s + s*t + t = Term_sub#(m,Concat(s,t)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) = 1 + m + m*x + s + s*x + 2*x + x*y + x^2 + y >= s + s*x + x + x^2 = c_20(Term_sub#(Term_var(x),s)) Concat(Concat(s,t),u) = s + s*t + s*t*u + s*u + t + t*u + u >= s + s*t + s*t*u + s*u + t + t*u + u = Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) = 1 + s + s*t + 2*t + t*xi + xi >= 1 + s + s*t + t + xi = Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) = 1 + m + m*t + s + s*t + 2*t + t*x + x >= 1 + m + m*t + s + s*t + 2*t + x = Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) = s >= s = s Frozen(m,Sum_constant(Left()),n,s) = 1 + m + m*s + n + n*s + 2*s >= m + m*s + s = Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) = 1 + m + m*s + n + n*s + 2*s >= n + n*s + s = Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) = 1 >= 1 = Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) = 1 >= 1 = Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) = 1 >= 1 = Sum_sub(xi,s) Sum_sub(xi,Id()) = 1 >= 1 = Sum_term_var(xi) Term_sub(Case(m,xi,n),s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) = m + m*s + s >= m + m*s + s = Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) = m + m*s + s >= m + m*s + s = Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) = 1 + m + m*s + n + n*s + 2*s >= 1 + m + m*s + n + n*s + 2*s = Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) = m + m*s + m*s*t + m*t + s + s*t + t >= m + m*s + m*s*t + m*t + s + s*t + t = Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) = 1 + s + s*x + 2*x + x*xi + xi >= s + s*x + x = Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + m*x + s + s*x + 2*x + x*y + y >= m = m Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + m*x + s + s*x + 2*x + x*y + y >= s + s*x + x = Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) = x >= x = Term_var(x) *** Step 1.b:4.b:5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)) Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)) Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,s) Term_sub#(Term_app(m,n),s) -> Term_sub#(m,s) Term_sub#(Term_app(m,n),s) -> Term_sub#(n,s) Term_sub#(Term_inl(m),s) -> Term_sub#(m,s) Term_sub#(Term_inr(m),s) -> Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) -> Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) -> Term_sub#(n,s) Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) Term_sub#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)) Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)) - Weak TRS: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t)) Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Id(),s) -> s Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s)) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Sum_sub(xi,Id()) -> Sum_term_var(xi) Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s) Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s)) Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s) Term_sub(Term_var(x),Id()) -> Term_var(x) - Signature: {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3 ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2 ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/1 ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub# ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app ,Term_inl,Term_inr,Term_pair,Term_var} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^3))