WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
+ Considered Problem:
- Strict TRS:
a__c(X) -> c(X)
a__c(X) -> d(X)
a__f(X) -> f(X)
a__f(f(X)) -> a__c(f(g(f(X))))
a__h(X) -> a__c(d(X))
a__h(X) -> h(X)
mark(c(X)) -> a__c(X)
mark(d(X)) -> d(X)
mark(f(X)) -> a__f(mark(X))
mark(g(X)) -> g(X)
mark(h(X)) -> a__h(mark(X))
- Signature:
{a__c/1,a__f/1,a__h/1,mark/1} / {c/1,d/1,f/1,g/1,h/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__c,a__f,a__h,mark} and constructors {c,d,f,g,h}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
a__c(X) -> c(X)
a__c(X) -> d(X)
a__f(X) -> f(X)
a__f(f(X)) -> a__c(f(g(f(X))))
a__h(X) -> a__c(d(X))
a__h(X) -> h(X)
mark(c(X)) -> a__c(X)
mark(d(X)) -> d(X)
mark(f(X)) -> a__f(mark(X))
mark(g(X)) -> g(X)
mark(h(X)) -> a__h(mark(X))
- Signature:
{a__c/1,a__f/1,a__h/1,mark/1} / {c/1,d/1,f/1,g/1,h/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__c,a__f,a__h,mark} and constructors {c,d,f,g,h}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
mark(x){x -> f(x)} =
mark(f(x)) ->^+ a__f(mark(x))
= C[mark(x) = mark(x){}]
** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
a__c(X) -> c(X)
a__c(X) -> d(X)
a__f(X) -> f(X)
a__f(f(X)) -> a__c(f(g(f(X))))
a__h(X) -> a__c(d(X))
a__h(X) -> h(X)
mark(c(X)) -> a__c(X)
mark(d(X)) -> d(X)
mark(f(X)) -> a__f(mark(X))
mark(g(X)) -> g(X)
mark(h(X)) -> a__h(mark(X))
- Signature:
{a__c/1,a__f/1,a__h/1,mark/1} / {c/1,d/1,f/1,g/1,h/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__c,a__f,a__h,mark} and constructors {c,d,f,g,h}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(a__f) = {1},
uargs(a__h) = {1}
Following symbols are considered usable:
{a__c,a__f,a__h,mark}
TcT has computed the following interpretation:
p(a__c) = 0
p(a__f) = x1
p(a__h) = x1
p(c) = 0
p(d) = 0
p(f) = x1
p(g) = 0
p(h) = x1
p(mark) = 2
Following rules are strictly oriented:
mark(c(X)) = 2
> 0
= a__c(X)
mark(d(X)) = 2
> 0
= d(X)
mark(g(X)) = 2
> 0
= g(X)
Following rules are (at-least) weakly oriented:
a__c(X) = 0
>= 0
= c(X)
a__c(X) = 0
>= 0
= d(X)
a__f(X) = X
>= X
= f(X)
a__f(f(X)) = X
>= 0
= a__c(f(g(f(X))))
a__h(X) = X
>= 0
= a__c(d(X))
a__h(X) = X
>= X
= h(X)
mark(f(X)) = 2
>= 2
= a__f(mark(X))
mark(h(X)) = 2
>= 2
= a__h(mark(X))
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
a__c(X) -> c(X)
a__c(X) -> d(X)
a__f(X) -> f(X)
a__f(f(X)) -> a__c(f(g(f(X))))
a__h(X) -> a__c(d(X))
a__h(X) -> h(X)
mark(f(X)) -> a__f(mark(X))
mark(h(X)) -> a__h(mark(X))
- Weak TRS:
mark(c(X)) -> a__c(X)
mark(d(X)) -> d(X)
mark(g(X)) -> g(X)
- Signature:
{a__c/1,a__f/1,a__h/1,mark/1} / {c/1,d/1,f/1,g/1,h/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__c,a__f,a__h,mark} and constructors {c,d,f,g,h}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(a__f) = {1},
uargs(a__h) = {1}
Following symbols are considered usable:
{a__c,a__f,a__h,mark}
TcT has computed the following interpretation:
p(a__c) = 0
p(a__f) = 1 + x1
p(a__h) = 6 + x1
p(c) = 0
p(d) = 0
p(f) = 1 + x1
p(g) = x1
p(h) = 1 + x1
p(mark) = 1 + 8*x1
Following rules are strictly oriented:
a__f(f(X)) = 2 + X
> 0
= a__c(f(g(f(X))))
a__h(X) = 6 + X
> 0
= a__c(d(X))
a__h(X) = 6 + X
> 1 + X
= h(X)
mark(f(X)) = 9 + 8*X
> 2 + 8*X
= a__f(mark(X))
mark(h(X)) = 9 + 8*X
> 7 + 8*X
= a__h(mark(X))
Following rules are (at-least) weakly oriented:
a__c(X) = 0
>= 0
= c(X)
a__c(X) = 0
>= 0
= d(X)
a__f(X) = 1 + X
>= 1 + X
= f(X)
mark(c(X)) = 1
>= 0
= a__c(X)
mark(d(X)) = 1
>= 0
= d(X)
mark(g(X)) = 1 + 8*X
>= X
= g(X)
** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
a__c(X) -> c(X)
a__c(X) -> d(X)
a__f(X) -> f(X)
- Weak TRS:
a__f(f(X)) -> a__c(f(g(f(X))))
a__h(X) -> a__c(d(X))
a__h(X) -> h(X)
mark(c(X)) -> a__c(X)
mark(d(X)) -> d(X)
mark(f(X)) -> a__f(mark(X))
mark(g(X)) -> g(X)
mark(h(X)) -> a__h(mark(X))
- Signature:
{a__c/1,a__f/1,a__h/1,mark/1} / {c/1,d/1,f/1,g/1,h/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__c,a__f,a__h,mark} and constructors {c,d,f,g,h}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(a__f) = {1},
uargs(a__h) = {1}
Following symbols are considered usable:
{a__c,a__f,a__h,mark}
TcT has computed the following interpretation:
p(a__c) = 4
p(a__f) = 3 + x1
p(a__h) = 7 + x1
p(c) = 4
p(d) = 2
p(f) = 1 + x1
p(g) = 3 + x1
p(h) = 4 + x1
p(mark) = 2 + 4*x1
Following rules are strictly oriented:
a__c(X) = 4
> 2
= d(X)
a__f(X) = 3 + X
> 1 + X
= f(X)
Following rules are (at-least) weakly oriented:
a__c(X) = 4
>= 4
= c(X)
a__f(f(X)) = 4 + X
>= 4
= a__c(f(g(f(X))))
a__h(X) = 7 + X
>= 4
= a__c(d(X))
a__h(X) = 7 + X
>= 4 + X
= h(X)
mark(c(X)) = 18
>= 4
= a__c(X)
mark(d(X)) = 10
>= 2
= d(X)
mark(f(X)) = 6 + 4*X
>= 5 + 4*X
= a__f(mark(X))
mark(g(X)) = 14 + 4*X
>= 3 + X
= g(X)
mark(h(X)) = 18 + 4*X
>= 9 + 4*X
= a__h(mark(X))
** Step 1.b:4: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
a__c(X) -> c(X)
- Weak TRS:
a__c(X) -> d(X)
a__f(X) -> f(X)
a__f(f(X)) -> a__c(f(g(f(X))))
a__h(X) -> a__c(d(X))
a__h(X) -> h(X)
mark(c(X)) -> a__c(X)
mark(d(X)) -> d(X)
mark(f(X)) -> a__f(mark(X))
mark(g(X)) -> g(X)
mark(h(X)) -> a__h(mark(X))
- Signature:
{a__c/1,a__f/1,a__h/1,mark/1} / {c/1,d/1,f/1,g/1,h/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__c,a__f,a__h,mark} and constructors {c,d,f,g,h}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(a__f) = {1},
uargs(a__h) = {1}
Following symbols are considered usable:
{a__c,a__f,a__h,mark}
TcT has computed the following interpretation:
p(a__c) = 15
p(a__f) = 11 + x1
p(a__h) = 15 + x1
p(c) = 4
p(d) = 0
p(f) = 8 + x1
p(g) = 4
p(h) = 8 + x1
p(mark) = 6 + 3*x1
Following rules are strictly oriented:
a__c(X) = 15
> 4
= c(X)
Following rules are (at-least) weakly oriented:
a__c(X) = 15
>= 0
= d(X)
a__f(X) = 11 + X
>= 8 + X
= f(X)
a__f(f(X)) = 19 + X
>= 15
= a__c(f(g(f(X))))
a__h(X) = 15 + X
>= 15
= a__c(d(X))
a__h(X) = 15 + X
>= 8 + X
= h(X)
mark(c(X)) = 18
>= 15
= a__c(X)
mark(d(X)) = 6
>= 0
= d(X)
mark(f(X)) = 30 + 3*X
>= 17 + 3*X
= a__f(mark(X))
mark(g(X)) = 18
>= 4
= g(X)
mark(h(X)) = 30 + 3*X
>= 21 + 3*X
= a__h(mark(X))
** Step 1.b:5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
a__c(X) -> c(X)
a__c(X) -> d(X)
a__f(X) -> f(X)
a__f(f(X)) -> a__c(f(g(f(X))))
a__h(X) -> a__c(d(X))
a__h(X) -> h(X)
mark(c(X)) -> a__c(X)
mark(d(X)) -> d(X)
mark(f(X)) -> a__f(mark(X))
mark(g(X)) -> g(X)
mark(h(X)) -> a__h(mark(X))
- Signature:
{a__c/1,a__f/1,a__h/1,mark/1} / {c/1,d/1,f/1,g/1,h/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a__c,a__f,a__h,mark} and constructors {c,d,f,g,h}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^1))