* Step 1: Sum WORST_CASE(Omega(n^1),O(n^2))
+ 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: NaturalPI WORST_CASE(?,O(n^2))
+ 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:
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(Case) = {1,3},
uargs(Concat) = {2},
uargs(Cons_sum) = {3},
uargs(Cons_usual) = {2,3},
uargs(Frozen) = {2},
uargs(Term_app) = {1,2},
uargs(Term_inl) = {1},
uargs(Term_inr) = {1},
uargs(Term_pair) = {1,2},
uargs(Term_sub) = {2}
Following symbols are considered usable:
{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) = x2 + x3
p(Cons_usual) = 1 + x2 + x3
p(Frozen) = 1 + x1 + x1*x2 + x1*x4 + x2 + x3 + x3*x4 + 2*x4
p(Id) = 1
p(Left) = 0
p(Right) = 0
p(Sum_constant) = 0
p(Sum_sub) = 0
p(Sum_term_var) = 0
p(Term_app) = 1 + x1 + x2
p(Term_inl) = 1 + x1
p(Term_inr) = x1
p(Term_pair) = 1 + x1 + x2
p(Term_sub) = x1 + x1*x2 + x2
p(Term_var) = 0
Following rules are strictly oriented:
Concat(Id(),s) = 1 + 2*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)
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()) = 1
> 0
= Term_var(x)
Following rules are (at-least) weakly oriented:
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) = k + k*t + s + s*t + t
>= k + s + s*t + t
= 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))
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)) = 0
>= 0
= Sum_constant(k)
Sum_sub(xi,Cons_sum(psi,k,s)) = 0
>= 0
= Sum_sub(xi,s)
Sum_sub(xi,Cons_usual(y,m,s)) = 0
>= 0
= Sum_sub(xi,s)
Sum_sub(xi,Id()) = 0
>= 0
= 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) = 1 + m + m*s + 2*s
>= 1 + 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)) = k + s
>= s
= Term_sub(Term_var(x),s)
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^2))
+ 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))
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)
- Weak TRS:
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)
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:
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(Case) = {1,3},
uargs(Concat) = {2},
uargs(Cons_sum) = {3},
uargs(Cons_usual) = {2,3},
uargs(Frozen) = {2},
uargs(Term_app) = {1,2},
uargs(Term_inl) = {1},
uargs(Term_inr) = {1},
uargs(Term_pair) = {1,2},
uargs(Term_sub) = {2}
Following symbols are considered usable:
{Concat,Frozen,Sum_sub,Term_sub}
TcT has computed the following interpretation:
p(Case) = 1 + x1 + x3
p(Concat) = x1 + 2*x1*x2 + x2
p(Cons_sum) = 1 + x2 + x3
p(Cons_usual) = 1 + x1 + x2 + x3
p(Frozen) = 1 + x1 + 2*x1*x4 + x2 + x3 + 2*x3*x4 + 2*x4
p(Id) = 0
p(Left) = 0
p(Right) = 0
p(Sum_constant) = 0
p(Sum_sub) = 0
p(Sum_term_var) = 0
p(Term_app) = 1 + x1 + x2
p(Term_inl) = x1
p(Term_inr) = x1
p(Term_pair) = 1 + x1 + x2
p(Term_sub) = x1 + 2*x1*x2 + x2
p(Term_var) = x1
Following rules are strictly oriented:
Term_sub(Term_var(x),Cons_sum(xi,k,s)) = 1 + k + 2*k*x + s + 2*s*x + 3*x
> s + 2*s*x + x
= Term_sub(Term_var(x),s)
Following rules are (at-least) weakly oriented:
Concat(Concat(s,t),u) = s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u
>= s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u
= Concat(s,Concat(t,u))
Concat(Cons_sum(xi,k,s),t) = 1 + k + 2*k*t + s + 2*s*t + 3*t
>= 1 + k + s + 2*s*t + t
= Cons_sum(xi,k,Concat(s,t))
Concat(Cons_usual(x,m,s),t) = 1 + m + 2*m*t + s + 2*s*t + 3*t + 2*t*x + x
>= 1 + m + 2*m*t + s + 2*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 + 2*m*s + n + 2*n*s + 2*s
>= m + 2*m*s + s
= Term_sub(m,s)
Frozen(m,Sum_constant(Right()),n,s) = 1 + m + 2*m*s + n + 2*n*s + 2*s
>= n + 2*n*s + s
= Term_sub(n,s)
Frozen(m,Sum_term_var(xi),n,s) = 1 + m + 2*m*s + n + 2*n*s + 2*s
>= 1 + m + 2*m*s + n + 2*n*s + 2*s
= Case(Term_sub(m,s),xi,Term_sub(n,s))
Sum_sub(xi,Cons_sum(psi,k,s)) = 0
>= 0
= Sum_constant(k)
Sum_sub(xi,Cons_sum(psi,k,s)) = 0
>= 0
= Sum_sub(xi,s)
Sum_sub(xi,Cons_usual(y,m,s)) = 0
>= 0
= Sum_sub(xi,s)
Sum_sub(xi,Id()) = 0
>= 0
= Sum_term_var(xi)
Term_sub(Case(m,xi,n),s) = 1 + m + 2*m*s + n + 2*n*s + 3*s
>= 1 + m + 2*m*s + n + 2*n*s + 2*s
= Frozen(m,Sum_sub(xi,s),n,s)
Term_sub(Term_app(m,n),s) = 1 + m + 2*m*s + n + 2*n*s + 3*s
>= 1 + m + 2*m*s + n + 2*n*s + 2*s
= Term_app(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_inl(m),s) = m + 2*m*s + s
>= m + 2*m*s + s
= Term_inl(Term_sub(m,s))
Term_sub(Term_inr(m),s) = m + 2*m*s + s
>= m + 2*m*s + s
= Term_inr(Term_sub(m,s))
Term_sub(Term_pair(m,n),s) = 1 + m + 2*m*s + n + 2*n*s + 3*s
>= 1 + m + 2*m*s + n + 2*n*s + 2*s
= Term_pair(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_sub(m,s),t) = m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t
>= m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t
= Term_sub(m,Concat(s,t))
Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + 2*m*x + s + 2*s*x + 3*x + 2*x*y + y
>= m
= m
Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + 2*m*x + s + 2*s*x + 3*x + 2*x*y + y
>= s + 2*s*x + x
= Term_sub(Term_var(x),s)
Term_sub(Term_var(x),Id()) = x
>= x
= Term_var(x)
** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^2))
+ 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))
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))
- Weak TRS:
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)
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:
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(Case) = {1,3},
uargs(Concat) = {2},
uargs(Cons_sum) = {3},
uargs(Cons_usual) = {2,3},
uargs(Frozen) = {2},
uargs(Term_app) = {1,2},
uargs(Term_inl) = {1},
uargs(Term_inr) = {1},
uargs(Term_pair) = {1,2},
uargs(Term_sub) = {2}
Following symbols are considered usable:
{Concat,Frozen,Sum_sub,Term_sub}
TcT has computed the following interpretation:
p(Case) = 1 + x1 + x2 + x3
p(Concat) = 2*x1 + x1*x2 + x1^2 + x2
p(Cons_sum) = x3
p(Cons_usual) = 1 + x1 + x2 + x3
p(Frozen) = 2 + 2*x1 + x1*x4 + x1^2 + x2 + 3*x3 + x3*x4 + x3^2 + 2*x4
p(Id) = 1
p(Left) = 0
p(Right) = 0
p(Sum_constant) = 0
p(Sum_sub) = 2*x1 + x1*x2
p(Sum_term_var) = x1
p(Term_app) = 1 + x1 + x2
p(Term_inl) = x1
p(Term_inr) = 1 + x1
p(Term_pair) = 1 + x1 + x2
p(Term_sub) = 2*x1 + x1*x2 + x1^2 + x2
p(Term_var) = 0
Following rules are strictly oriented:
Concat(Cons_usual(x,m,s),t) = 3 + 4*m + 2*m*s + m*t + 2*m*x + m^2 + 4*s + s*t + 2*s*x + s^2 + 2*t + t*x + 4*x + x^2
> 1 + 2*m + m*t + m^2 + 2*s + s*t + s^2 + 2*t + x
= Cons_usual(x,Term_sub(m,t),Concat(s,t))
Frozen(m,Sum_term_var(xi),n,s) = 2 + 2*m + m*s + m^2 + 3*n + n*s + n^2 + 2*s + xi
> 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s + xi
= Case(Term_sub(m,s),xi,Term_sub(n,s))
Term_sub(Case(m,xi,n),s) = 3 + 4*m + 2*m*n + m*s + 2*m*xi + m^2 + 4*n + n*s + 2*n*xi + n^2 + 2*s + s*xi + 4*xi + xi^2
> 2 + 2*m + m*s + m^2 + 3*n + n*s + n^2 + 2*s + s*xi + 2*xi
= Frozen(m,Sum_sub(xi,s),n,s)
Term_sub(Term_app(m,n),s) = 3 + 4*m + 2*m*n + m*s + m^2 + 4*n + n*s + n^2 + 2*s
> 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s
= Term_app(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_inr(m),s) = 3 + 4*m + m*s + m^2 + 2*s
> 1 + 2*m + m*s + m^2 + s
= Term_inr(Term_sub(m,s))
Term_sub(Term_pair(m,n),s) = 3 + 4*m + 2*m*n + m*s + m^2 + 4*n + n*s + n^2 + 2*s
> 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s
= Term_pair(Term_sub(m,s),Term_sub(n,s))
Following rules are (at-least) weakly oriented:
Concat(Concat(s,t),u) = 4*s + 6*s*t + s*t*u + 2*s*t^2 + 2*s*u + 6*s^2 + 6*s^2*t + s^2*t^2 + s^2*u + 4*s^3 + 2*s^3*t + s^4 + 2*t + t*u + t^2 + u
>= 2*s + 2*s*t + s*t*u + s*t^2 + s*u + s^2 + 2*t + t*u + t^2 + u
= Concat(s,Concat(t,u))
Concat(Cons_sum(xi,k,s),t) = 2*s + s*t + s^2 + t
>= 2*s + s*t + s^2 + t
= Cons_sum(xi,k,Concat(s,t))
Concat(Id(),s) = 3 + 2*s
>= s
= s
Frozen(m,Sum_constant(Left()),n,s) = 2 + 2*m + m*s + m^2 + 3*n + n*s + n^2 + 2*s
>= 2*m + m*s + m^2 + s
= Term_sub(m,s)
Frozen(m,Sum_constant(Right()),n,s) = 2 + 2*m + m*s + m^2 + 3*n + n*s + n^2 + 2*s
>= 2*n + n*s + n^2 + s
= Term_sub(n,s)
Sum_sub(xi,Cons_sum(psi,k,s)) = s*xi + 2*xi
>= 0
= Sum_constant(k)
Sum_sub(xi,Cons_sum(psi,k,s)) = s*xi + 2*xi
>= s*xi + 2*xi
= Sum_sub(xi,s)
Sum_sub(xi,Cons_usual(y,m,s)) = m*xi + s*xi + 3*xi + xi*y
>= s*xi + 2*xi
= Sum_sub(xi,s)
Sum_sub(xi,Id()) = 3*xi
>= xi
= Sum_term_var(xi)
Term_sub(Term_inl(m),s) = 2*m + m*s + m^2 + s
>= 2*m + m*s + m^2 + s
= Term_inl(Term_sub(m,s))
Term_sub(Term_sub(m,s),t) = 4*m + 6*m*s + m*s*t + 2*m*s^2 + 2*m*t + 6*m^2 + 6*m^2*s + m^2*s^2 + m^2*t + 4*m^3 + 2*m^3*s + m^4 + 2*s + s*t + s^2 + t
>= 2*m + 2*m*s + m*s*t + m*s^2 + m*t + m^2 + 2*s + s*t + s^2 + t
= Term_sub(m,Concat(s,t))
Term_sub(Term_var(x),Cons_sum(xi,k,s)) = s
>= s
= Term_sub(Term_var(x),s)
Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + s + y
>= m
= m
Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + s + y
>= s
= Term_sub(Term_var(x),s)
Term_sub(Term_var(x),Id()) = 1
>= 0
= Term_var(x)
** Step 1.b:4: NaturalPI WORST_CASE(?,O(n^2))
+ 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))
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(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
- Weak TRS:
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))
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_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_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:
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(Case) = {1,3},
uargs(Concat) = {2},
uargs(Cons_sum) = {3},
uargs(Cons_usual) = {2,3},
uargs(Frozen) = {2},
uargs(Term_app) = {1,2},
uargs(Term_inl) = {1},
uargs(Term_inr) = {1},
uargs(Term_pair) = {1,2},
uargs(Term_sub) = {2}
Following symbols are considered usable:
{Concat,Frozen,Sum_sub,Term_sub}
TcT has computed the following interpretation:
p(Case) = 1 + x1 + x3
p(Concat) = x1 + 2*x1*x2 + x2
p(Cons_sum) = x2 + x3
p(Cons_usual) = 1 + x2 + x3
p(Frozen) = x1 + 2*x1*x4 + x2 + x2*x4 + x3 + 2*x3*x4 + x4
p(Id) = 0
p(Left) = 0
p(Right) = 1
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 + 2*x1*x2 + x2
p(Term_var) = 0
Following rules are strictly oriented:
Sum_sub(xi,Cons_sum(psi,k,s)) = 1
> 0
= Sum_constant(k)
Following rules are (at-least) weakly oriented:
Concat(Concat(s,t),u) = s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u
>= s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u
= Concat(s,Concat(t,u))
Concat(Cons_sum(xi,k,s),t) = k + 2*k*t + s + 2*s*t + t
>= k + s + 2*s*t + t
= Cons_sum(xi,k,Concat(s,t))
Concat(Cons_usual(x,m,s),t) = 1 + m + 2*m*t + s + 2*s*t + 3*t
>= 1 + m + 2*m*t + s + 2*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 + 2*m*s + n + 2*n*s + s
>= m + 2*m*s + s
= Term_sub(m,s)
Frozen(m,Sum_constant(Right()),n,s) = m + 2*m*s + n + 2*n*s + s
>= n + 2*n*s + s
= Term_sub(n,s)
Frozen(m,Sum_term_var(xi),n,s) = 1 + m + 2*m*s + n + 2*n*s + 2*s
>= 1 + m + 2*m*s + n + 2*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_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 + 2*m*s + n + 2*n*s + 3*s
>= 1 + m + 2*m*s + n + 2*n*s + 2*s
= Frozen(m,Sum_sub(xi,s),n,s)
Term_sub(Term_app(m,n),s) = 1 + m + 2*m*s + n + 2*n*s + 3*s
>= 1 + m + 2*m*s + n + 2*n*s + 2*s
= Term_app(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_inl(m),s) = m + 2*m*s + s
>= m + 2*m*s + s
= Term_inl(Term_sub(m,s))
Term_sub(Term_inr(m),s) = m + 2*m*s + s
>= m + 2*m*s + s
= Term_inr(Term_sub(m,s))
Term_sub(Term_pair(m,n),s) = 1 + m + 2*m*s + n + 2*n*s + 3*s
>= 1 + m + 2*m*s + n + 2*n*s + 2*s
= Term_pair(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_sub(m,s),t) = m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t
>= m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t
= Term_sub(m,Concat(s,t))
Term_sub(Term_var(x),Cons_sum(xi,k,s)) = k + s
>= 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:5: NaturalPI WORST_CASE(?,O(n^2))
+ 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))
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(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
- Weak TRS:
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)
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_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_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:
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(Case) = {1,3},
uargs(Concat) = {2},
uargs(Cons_sum) = {3},
uargs(Cons_usual) = {2,3},
uargs(Frozen) = {2},
uargs(Term_app) = {1,2},
uargs(Term_inl) = {1},
uargs(Term_inr) = {1},
uargs(Term_pair) = {1,2},
uargs(Term_sub) = {2}
Following symbols are considered usable:
{Concat,Frozen,Sum_sub,Term_sub}
TcT has computed the following interpretation:
p(Case) = 1 + x1 + x2 + x3
p(Concat) = x1 + 2*x1*x2 + x2
p(Cons_sum) = x1 + x3
p(Cons_usual) = 1 + x1 + x2 + x3
p(Frozen) = 1 + x1 + 2*x1*x4 + x2 + x3 + 2*x3*x4 + 2*x4
p(Id) = 1
p(Left) = 1
p(Right) = 0
p(Sum_constant) = 0
p(Sum_sub) = x1*x2 + x2
p(Sum_term_var) = 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 + 2*x1*x2 + x2
p(Term_var) = 0
Following rules are strictly oriented:
Sum_sub(xi,Cons_usual(y,m,s)) = 1 + m + m*xi + s + s*xi + xi + xi*y + y
> s + s*xi
= Sum_sub(xi,s)
Sum_sub(xi,Id()) = 1 + xi
> xi
= Sum_term_var(xi)
Following rules are (at-least) weakly oriented:
Concat(Concat(s,t),u) = s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u
>= s + 2*s*t + 4*s*t*u + 2*s*u + t + 2*t*u + u
= Concat(s,Concat(t,u))
Concat(Cons_sum(xi,k,s),t) = s + 2*s*t + t + 2*t*xi + xi
>= s + 2*s*t + t + xi
= Cons_sum(xi,k,Concat(s,t))
Concat(Cons_usual(x,m,s),t) = 1 + m + 2*m*t + s + 2*s*t + 3*t + 2*t*x + x
>= 1 + m + 2*m*t + s + 2*s*t + 2*t + x
= Cons_usual(x,Term_sub(m,t),Concat(s,t))
Concat(Id(),s) = 1 + 3*s
>= s
= s
Frozen(m,Sum_constant(Left()),n,s) = 1 + m + 2*m*s + n + 2*n*s + 2*s
>= m + 2*m*s + s
= Term_sub(m,s)
Frozen(m,Sum_constant(Right()),n,s) = 1 + m + 2*m*s + n + 2*n*s + 2*s
>= n + 2*n*s + s
= Term_sub(n,s)
Frozen(m,Sum_term_var(xi),n,s) = 1 + m + 2*m*s + n + 2*n*s + 2*s + xi
>= 1 + m + 2*m*s + n + 2*n*s + 2*s + xi
= Case(Term_sub(m,s),xi,Term_sub(n,s))
Sum_sub(xi,Cons_sum(psi,k,s)) = psi + psi*xi + s + s*xi
>= 0
= Sum_constant(k)
Sum_sub(xi,Cons_sum(psi,k,s)) = psi + psi*xi + s + s*xi
>= s + s*xi
= Sum_sub(xi,s)
Term_sub(Case(m,xi,n),s) = 1 + m + 2*m*s + n + 2*n*s + 3*s + 2*s*xi + xi
>= 1 + m + 2*m*s + n + 2*n*s + 3*s + s*xi
= Frozen(m,Sum_sub(xi,s),n,s)
Term_sub(Term_app(m,n),s) = 1 + m + 2*m*s + n + 2*n*s + 3*s
>= 1 + m + 2*m*s + n + 2*n*s + 2*s
= Term_app(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_inl(m),s) = m + 2*m*s + s
>= m + 2*m*s + s
= Term_inl(Term_sub(m,s))
Term_sub(Term_inr(m),s) = m + 2*m*s + s
>= m + 2*m*s + s
= Term_inr(Term_sub(m,s))
Term_sub(Term_pair(m,n),s) = 1 + m + 2*m*s + n + 2*n*s + 3*s
>= 1 + m + 2*m*s + n + 2*n*s + 2*s
= Term_pair(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_sub(m,s),t) = m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t
>= m + 2*m*s + 4*m*s*t + 2*m*t + s + 2*s*t + t
= Term_sub(m,Concat(s,t))
Term_sub(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 + y
>= m
= m
Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + s + y
>= s
= Term_sub(Term_var(x),s)
Term_sub(Term_var(x),Id()) = 1
>= 0
= Term_var(x)
** Step 1.b:6: NaturalPI WORST_CASE(?,O(n^2))
+ 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))
Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
- Weak TRS:
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_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_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_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:
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(Case) = {1,3},
uargs(Concat) = {2},
uargs(Cons_sum) = {3},
uargs(Cons_usual) = {2,3},
uargs(Frozen) = {2},
uargs(Term_app) = {1,2},
uargs(Term_inl) = {1},
uargs(Term_inr) = {1},
uargs(Term_pair) = {1,2},
uargs(Term_sub) = {2}
Following symbols are considered usable:
{Concat,Frozen,Sum_sub,Term_sub}
TcT has computed the following interpretation:
p(Case) = 1 + x1 + x3
p(Concat) = 2*x1 + x1*x2 + x2
p(Cons_sum) = x3
p(Cons_usual) = 1 + x1 + x2 + x3
p(Frozen) = 2 + 2*x1 + x1*x4 + 2*x2 + 2*x3 + x3*x4 + 2*x4
p(Id) = 0
p(Left) = 0
p(Right) = 0
p(Sum_constant) = 0
p(Sum_sub) = 0
p(Sum_term_var) = 0
p(Term_app) = 1 + x1 + x2
p(Term_inl) = 1 + x1
p(Term_inr) = x1
p(Term_pair) = 1 + x1 + x2
p(Term_sub) = 2*x1 + x1*x2 + x2
p(Term_var) = x1
Following rules are strictly oriented:
Term_sub(Term_inl(m),s) = 2 + 2*m + m*s + 2*s
> 1 + 2*m + m*s + s
= Term_inl(Term_sub(m,s))
Following rules are (at-least) weakly oriented:
Concat(Concat(s,t),u) = 4*s + 2*s*t + s*t*u + 2*s*u + 2*t + t*u + u
>= 2*s + 2*s*t + s*t*u + s*u + 2*t + t*u + u
= Concat(s,Concat(t,u))
Concat(Cons_sum(xi,k,s),t) = 2*s + s*t + t
>= 2*s + s*t + t
= Cons_sum(xi,k,Concat(s,t))
Concat(Cons_usual(x,m,s),t) = 2 + 2*m + m*t + 2*s + s*t + 2*t + t*x + 2*x
>= 1 + 2*m + m*t + 2*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) = 2 + 2*m + m*s + 2*n + n*s + 2*s
>= 2*m + m*s + s
= Term_sub(m,s)
Frozen(m,Sum_constant(Right()),n,s) = 2 + 2*m + m*s + 2*n + n*s + 2*s
>= 2*n + n*s + s
= Term_sub(n,s)
Frozen(m,Sum_term_var(xi),n,s) = 2 + 2*m + m*s + 2*n + n*s + 2*s
>= 1 + 2*m + m*s + 2*n + n*s + 2*s
= Case(Term_sub(m,s),xi,Term_sub(n,s))
Sum_sub(xi,Cons_sum(psi,k,s)) = 0
>= 0
= Sum_constant(k)
Sum_sub(xi,Cons_sum(psi,k,s)) = 0
>= 0
= Sum_sub(xi,s)
Sum_sub(xi,Cons_usual(y,m,s)) = 0
>= 0
= Sum_sub(xi,s)
Sum_sub(xi,Id()) = 0
>= 0
= Sum_term_var(xi)
Term_sub(Case(m,xi,n),s) = 2 + 2*m + m*s + 2*n + n*s + 2*s
>= 2 + 2*m + m*s + 2*n + n*s + 2*s
= Frozen(m,Sum_sub(xi,s),n,s)
Term_sub(Term_app(m,n),s) = 2 + 2*m + m*s + 2*n + n*s + 2*s
>= 1 + 2*m + m*s + 2*n + n*s + 2*s
= Term_app(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_inr(m),s) = 2*m + m*s + s
>= 2*m + m*s + s
= Term_inr(Term_sub(m,s))
Term_sub(Term_pair(m,n),s) = 2 + 2*m + m*s + 2*n + n*s + 2*s
>= 1 + 2*m + m*s + 2*n + n*s + 2*s
= Term_pair(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_sub(m,s),t) = 4*m + 2*m*s + m*s*t + 2*m*t + 2*s + s*t + t
>= 2*m + 2*m*s + m*s*t + m*t + 2*s + s*t + t
= Term_sub(m,Concat(s,t))
Term_sub(Term_var(x),Cons_sum(xi,k,s)) = s + s*x + 2*x
>= s + s*x + 2*x
= Term_sub(Term_var(x),s)
Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + m*x + s + s*x + 3*x + x*y + y
>= m
= m
Term_sub(Term_var(x),Cons_usual(y,m,s)) = 1 + m + m*x + s + s*x + 3*x + x*y + y
>= s + s*x + 2*x
= Term_sub(Term_var(x),s)
Term_sub(Term_var(x),Id()) = 2*x
>= x
= Term_var(x)
** Step 1.b:7: NaturalPI WORST_CASE(?,O(n^2))
+ 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))
Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
- Weak TRS:
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_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_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:
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(Case) = {1,3},
uargs(Concat) = {2},
uargs(Cons_sum) = {3},
uargs(Cons_usual) = {2,3},
uargs(Frozen) = {2},
uargs(Term_app) = {1,2},
uargs(Term_inl) = {1},
uargs(Term_inr) = {1},
uargs(Term_pair) = {1,2},
uargs(Term_sub) = {2}
Following symbols are considered usable:
{Concat,Frozen,Sum_sub,Term_sub}
TcT has computed the following interpretation:
p(Case) = 1 + x1 + x3
p(Concat) = 2*x1 + x1*x2 + x1^2 + x2
p(Cons_sum) = 1 + x1 + x3
p(Cons_usual) = 1 + x2 + x3
p(Frozen) = 1 + 2*x1 + x1*x4 + x1^2 + 2*x2 + 2*x3 + x3*x4 + x3^2 + 2*x4
p(Id) = 0
p(Left) = 1
p(Right) = 0
p(Sum_constant) = 0
p(Sum_sub) = 0
p(Sum_term_var) = 0
p(Term_app) = 1 + x1 + x2
p(Term_inl) = 1 + x1
p(Term_inr) = x1
p(Term_pair) = 1 + x1 + x2
p(Term_sub) = 2*x1 + x1*x2 + x1^2 + x2
p(Term_var) = 0
Following rules are strictly oriented:
Concat(Cons_sum(xi,k,s),t) = 3 + 4*s + s*t + 2*s*xi + s^2 + 2*t + t*xi + 4*xi + xi^2
> 1 + 2*s + s*t + s^2 + t + xi
= Cons_sum(xi,k,Concat(s,t))
Following rules are (at-least) weakly oriented:
Concat(Concat(s,t),u) = 4*s + 6*s*t + s*t*u + 2*s*t^2 + 2*s*u + 6*s^2 + 6*s^2*t + s^2*t^2 + s^2*u + 4*s^3 + 2*s^3*t + s^4 + 2*t + t*u + t^2 + u
>= 2*s + 2*s*t + s*t*u + s*t^2 + s*u + s^2 + 2*t + t*u + t^2 + u
= Concat(s,Concat(t,u))
Concat(Cons_usual(x,m,s),t) = 3 + 4*m + 2*m*s + m*t + m^2 + 4*s + s*t + s^2 + 2*t
>= 1 + 2*m + m*t + m^2 + 2*s + s*t + s^2 + 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 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s
>= 2*m + m*s + m^2 + s
= Term_sub(m,s)
Frozen(m,Sum_constant(Right()),n,s) = 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s
>= 2*n + n*s + n^2 + s
= Term_sub(n,s)
Frozen(m,Sum_term_var(xi),n,s) = 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s
>= 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s
= Case(Term_sub(m,s),xi,Term_sub(n,s))
Sum_sub(xi,Cons_sum(psi,k,s)) = 0
>= 0
= Sum_constant(k)
Sum_sub(xi,Cons_sum(psi,k,s)) = 0
>= 0
= Sum_sub(xi,s)
Sum_sub(xi,Cons_usual(y,m,s)) = 0
>= 0
= Sum_sub(xi,s)
Sum_sub(xi,Id()) = 0
>= 0
= Sum_term_var(xi)
Term_sub(Case(m,xi,n),s) = 3 + 4*m + 2*m*n + m*s + m^2 + 4*n + n*s + n^2 + 2*s
>= 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s
= Frozen(m,Sum_sub(xi,s),n,s)
Term_sub(Term_app(m,n),s) = 3 + 4*m + 2*m*n + m*s + m^2 + 4*n + n*s + n^2 + 2*s
>= 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s
= Term_app(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_inl(m),s) = 3 + 4*m + m*s + m^2 + 2*s
>= 1 + 2*m + m*s + m^2 + s
= Term_inl(Term_sub(m,s))
Term_sub(Term_inr(m),s) = 2*m + m*s + m^2 + s
>= 2*m + m*s + m^2 + s
= Term_inr(Term_sub(m,s))
Term_sub(Term_pair(m,n),s) = 3 + 4*m + 2*m*n + m*s + m^2 + 4*n + n*s + n^2 + 2*s
>= 1 + 2*m + m*s + m^2 + 2*n + n*s + n^2 + 2*s
= Term_pair(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_sub(m,s),t) = 4*m + 6*m*s + m*s*t + 2*m*s^2 + 2*m*t + 6*m^2 + 6*m^2*s + m^2*s^2 + m^2*t + 4*m^3 + 2*m^3*s + m^4 + 2*s + s*t + s^2 + t
>= 2*m + 2*m*s + m*s*t + m*s^2 + m*t + m^2 + 2*s + s*t + s^2 + 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:8: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
- Weak TRS:
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_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_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:
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(Case) = {1,3},
uargs(Concat) = {2},
uargs(Cons_sum) = {3},
uargs(Cons_usual) = {2,3},
uargs(Frozen) = {2},
uargs(Term_app) = {1,2},
uargs(Term_inl) = {1},
uargs(Term_inr) = {1},
uargs(Term_pair) = {1,2},
uargs(Term_sub) = {2}
Following symbols are considered usable:
{Concat,Frozen,Sum_sub,Term_sub}
TcT has computed the following interpretation:
p(Case) = 1 + x1 + x3
p(Concat) = 1 + x1 + x1*x2 + x1^2 + x2
p(Cons_sum) = x3
p(Cons_usual) = 1 + x2 + x3
p(Frozen) = 1 + x1*x2 + x1*x4 + x1^2 + 2*x2 + x2*x3 + x3*x4 + x3^2 + 2*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) = 1 + x1
p(Term_inr) = 1 + x1
p(Term_pair) = 1 + x1 + x2
p(Term_sub) = 1 + x1 + x1*x2 + x1^2 + x2
p(Term_var) = 1 + x1
Following rules are strictly oriented:
Concat(Concat(s,t),u) = 3 + 3*s + 5*s*t + s*t*u + 2*s*t^2 + s*u + 4*s^2 + 4*s^2*t + s^2*t^2 + s^2*u + 2*s^3 + 2*s^3*t + s^4 + 3*t + t*u + t^2 + 2*u
> 2 + 2*s + s*t + s*t*u + s*t^2 + s*u + s^2 + t + t*u + t^2 + u
= Concat(s,Concat(t,u))
Term_sub(Term_sub(m,s),t) = 3 + 3*m + 5*m*s + m*s*t + 2*m*s^2 + m*t + 4*m^2 + 4*m^2*s + m^2*s^2 + m^2*t + 2*m^3 + 2*m^3*s + m^4 + 3*s + s*t + s^2 + 2*t
> 2 + 2*m + m*s + m*s*t + m*s^2 + m*t + m^2 + s + s*t + s^2 + t
= Term_sub(m,Concat(s,t))
Following rules are (at-least) weakly oriented:
Concat(Cons_sum(xi,k,s),t) = 1 + s + s*t + s^2 + t
>= 1 + s + s*t + s^2 + t
= Cons_sum(xi,k,Concat(s,t))
Concat(Cons_usual(x,m,s),t) = 3 + 3*m + 2*m*s + m*t + m^2 + 3*s + s*t + s^2 + 2*t
>= 3 + m + m*t + m^2 + s + s*t + s^2 + 2*t
= Cons_usual(x,Term_sub(m,t),Concat(s,t))
Concat(Id(),s) = 1 + s
>= s
= s
Frozen(m,Sum_constant(Left()),n,s) = 3 + m + m*s + m^2 + n + n*s + n^2 + 2*s
>= 1 + m + m*s + m^2 + s
= Term_sub(m,s)
Frozen(m,Sum_constant(Right()),n,s) = 3 + m + m*s + m^2 + n + n*s + n^2 + 2*s
>= 1 + n + n*s + n^2 + s
= Term_sub(n,s)
Frozen(m,Sum_term_var(xi),n,s) = 3 + m + m*s + m^2 + n + n*s + n^2 + 2*s
>= 3 + m + m*s + m^2 + n + n*s + n^2 + 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) = 3 + 3*m + 2*m*n + m*s + m^2 + 3*n + n*s + n^2 + 2*s
>= 3 + m + m*s + m^2 + n + n*s + n^2 + 2*s
= Frozen(m,Sum_sub(xi,s),n,s)
Term_sub(Term_app(m,n),s) = 3 + 3*m + 2*m*n + m*s + m^2 + 3*n + n*s + n^2 + 2*s
>= 3 + m + m*s + m^2 + n + n*s + n^2 + 2*s
= Term_app(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_inl(m),s) = 3 + 3*m + m*s + m^2 + 2*s
>= 2 + m + m*s + m^2 + s
= Term_inl(Term_sub(m,s))
Term_sub(Term_inr(m),s) = 3 + 3*m + m*s + m^2 + 2*s
>= 2 + m + m*s + m^2 + s
= Term_inr(Term_sub(m,s))
Term_sub(Term_pair(m,n),s) = 3 + 3*m + 2*m*n + m*s + m^2 + 3*n + n*s + n^2 + 2*s
>= 3 + m + m*s + m^2 + n + n*s + n^2 + 2*s
= Term_pair(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_var(x),Cons_sum(xi,k,s)) = 3 + 2*s + s*x + 3*x + x^2
>= 3 + 2*s + s*x + 3*x + x^2
= Term_sub(Term_var(x),s)
Term_sub(Term_var(x),Cons_usual(y,m,s)) = 5 + 2*m + m*x + 2*s + s*x + 4*x + x^2
>= m
= m
Term_sub(Term_var(x),Cons_usual(y,m,s)) = 5 + 2*m + m*x + 2*s + s*x + 4*x + x^2
>= 3 + 2*s + s*x + 3*x + x^2
= Term_sub(Term_var(x),s)
Term_sub(Term_var(x),Id()) = 3 + 3*x + x^2
>= 1 + x
= Term_var(x)
** Step 1.b:9: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,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_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:
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(Case) = {1,3},
uargs(Concat) = {2},
uargs(Cons_sum) = {3},
uargs(Cons_usual) = {2,3},
uargs(Frozen) = {2},
uargs(Term_app) = {1,2},
uargs(Term_inl) = {1},
uargs(Term_inr) = {1},
uargs(Term_pair) = {1,2},
uargs(Term_sub) = {2}
Following symbols are considered usable:
{Concat,Frozen,Sum_sub,Term_sub}
TcT has computed the following interpretation:
p(Case) = 1 + x1 + x2 + x3
p(Concat) = x1 + 2*x1*x2 + x1^2 + x2
p(Cons_sum) = 1 + x2 + x3
p(Cons_usual) = 1 + x2 + x3
p(Frozen) = 2 + x1 + 2*x1*x4 + x1^2 + x2 + 2*x3 + 2*x3*x4 + x3^2 + 2*x4
p(Id) = 1
p(Left) = 1
p(Right) = 1
p(Sum_constant) = x1
p(Sum_sub) = 2*x1 + x2
p(Sum_term_var) = 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 + 2*x1*x2 + x1^2 + x2
p(Term_var) = 0
Following rules are strictly oriented:
Sum_sub(xi,Cons_sum(psi,k,s)) = 1 + k + s + 2*xi
> s + 2*xi
= Sum_sub(xi,s)
Following rules are (at-least) weakly oriented:
Concat(Concat(s,t),u) = s + 4*s*t + 4*s*t*u + 4*s*t^2 + 2*s*u + 2*s^2 + 6*s^2*t + 4*s^2*t^2 + 2*s^2*u + 2*s^3 + 4*s^3*t + s^4 + t + 2*t*u + t^2 + u
>= s + 2*s*t + 4*s*t*u + 2*s*t^2 + 2*s*u + s^2 + t + 2*t*u + t^2 + u
= Concat(s,Concat(t,u))
Concat(Cons_sum(xi,k,s),t) = 2 + 3*k + 2*k*s + 2*k*t + k^2 + 3*s + 2*s*t + s^2 + 3*t
>= 1 + k + s + 2*s*t + s^2 + t
= Cons_sum(xi,k,Concat(s,t))
Concat(Cons_usual(x,m,s),t) = 2 + 3*m + 2*m*s + 2*m*t + m^2 + 3*s + 2*s*t + s^2 + 3*t
>= 1 + m + 2*m*t + m^2 + s + 2*s*t + s^2 + 2*t
= Cons_usual(x,Term_sub(m,t),Concat(s,t))
Concat(Id(),s) = 2 + 3*s
>= s
= s
Frozen(m,Sum_constant(Left()),n,s) = 3 + m + 2*m*s + m^2 + 2*n + 2*n*s + n^2 + 2*s
>= m + 2*m*s + m^2 + s
= Term_sub(m,s)
Frozen(m,Sum_constant(Right()),n,s) = 3 + m + 2*m*s + m^2 + 2*n + 2*n*s + n^2 + 2*s
>= n + 2*n*s + n^2 + s
= Term_sub(n,s)
Frozen(m,Sum_term_var(xi),n,s) = 2 + m + 2*m*s + m^2 + 2*n + 2*n*s + n^2 + 2*s + xi
>= 1 + m + 2*m*s + m^2 + n + 2*n*s + n^2 + 2*s + xi
= Case(Term_sub(m,s),xi,Term_sub(n,s))
Sum_sub(xi,Cons_sum(psi,k,s)) = 1 + k + s + 2*xi
>= k
= Sum_constant(k)
Sum_sub(xi,Cons_usual(y,m,s)) = 1 + m + s + 2*xi
>= s + 2*xi
= Sum_sub(xi,s)
Sum_sub(xi,Id()) = 1 + 2*xi
>= xi
= Sum_term_var(xi)
Term_sub(Case(m,xi,n),s) = 2 + 3*m + 2*m*n + 2*m*s + 2*m*xi + m^2 + 3*n + 2*n*s + 2*n*xi + n^2 + 3*s + 2*s*xi + 3*xi + xi^2
>= 2 + m + 2*m*s + m^2 + 2*n + 2*n*s + n^2 + 3*s + 2*xi
= Frozen(m,Sum_sub(xi,s),n,s)
Term_sub(Term_app(m,n),s) = 2 + 3*m + 2*m*n + 2*m*s + m^2 + 3*n + 2*n*s + n^2 + 3*s
>= 1 + m + 2*m*s + m^2 + n + 2*n*s + n^2 + 2*s
= Term_app(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_inl(m),s) = m + 2*m*s + m^2 + s
>= m + 2*m*s + m^2 + s
= Term_inl(Term_sub(m,s))
Term_sub(Term_inr(m),s) = m + 2*m*s + m^2 + s
>= m + 2*m*s + m^2 + s
= Term_inr(Term_sub(m,s))
Term_sub(Term_pair(m,n),s) = 2 + 3*m + 2*m*n + 2*m*s + m^2 + 3*n + 2*n*s + n^2 + 3*s
>= 1 + m + 2*m*s + m^2 + n + 2*n*s + n^2 + 2*s
= Term_pair(Term_sub(m,s),Term_sub(n,s))
Term_sub(Term_sub(m,s),t) = m + 4*m*s + 4*m*s*t + 4*m*s^2 + 2*m*t + 2*m^2 + 6*m^2*s + 4*m^2*s^2 + 2*m^2*t + 2*m^3 + 4*m^3*s + m^4 + s + 2*s*t + s^2 + t
>= m + 2*m*s + 4*m*s*t + 2*m*s^2 + 2*m*t + m^2 + s + 2*s*t + s^2 + t
= Term_sub(m,Concat(s,t))
Term_sub(Term_var(x),Cons_sum(xi,k,s)) = 1 + k + s
>= 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()) = 1
>= 0
= Term_var(x)
** Step 1.b:10: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- 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} / {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:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^2))