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))