WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
+ Considered Problem:
- Strict TRS:
f(x) -> x
f(c(s(x),y)) -> f(c(x,s(y)))
f(f(x)) -> f(d(f(x)))
g(c(x,s(y))) -> g(c(s(x),y))
- Signature:
{f/1,g/1} / {c/2,d/1,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,g} and constructors {c,d,s}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
f(x) -> x
f(c(s(x),y)) -> f(c(x,s(y)))
f(f(x)) -> f(d(f(x)))
g(c(x,s(y))) -> g(c(s(x),y))
- Signature:
{f/1,g/1} / {c/2,d/1,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,g} and constructors {c,d,s}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
f(c(x,y)){x -> s(x)} =
f(c(s(x),y)) ->^+ f(c(x,s(y)))
= C[f(c(x,s(y))) = f(c(x,y)){y -> s(y)}]
** Step 1.b:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
f(x) -> x
f(c(s(x),y)) -> f(c(x,s(y)))
f(f(x)) -> f(d(f(x)))
g(c(x,s(y))) -> g(c(s(x),y))
- Signature:
{f/1,g/1} / {c/2,d/1,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,g} and constructors {c,d,s}
+ 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:
none
Following symbols are considered usable:
{f,g}
TcT has computed the following interpretation:
p(c) = [0]
p(d) = [4]
p(f) = [2] x1 + [4]
p(g) = [0]
p(s) = [1]
Following rules are strictly oriented:
f(x) = [2] x + [4]
> [1] x + [0]
= x
Following rules are (at-least) weakly oriented:
f(c(s(x),y)) = [4]
>= [4]
= f(c(x,s(y)))
f(f(x)) = [4] x + [12]
>= [12]
= f(d(f(x)))
g(c(x,s(y))) = [0]
>= [0]
= g(c(s(x),y))
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
f(c(s(x),y)) -> f(c(x,s(y)))
f(f(x)) -> f(d(f(x)))
g(c(x,s(y))) -> g(c(s(x),y))
- Weak TRS:
f(x) -> x
- Signature:
{f/1,g/1} / {c/2,d/1,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,g} and constructors {c,d,s}
+ 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:
none
Following symbols are considered usable:
{f,g}
TcT has computed the following interpretation:
p(c) = x1
p(d) = 0
p(f) = 2*x1
p(g) = 10
p(s) = 8 + x1
Following rules are strictly oriented:
f(c(s(x),y)) = 16 + 2*x
> 2*x
= f(c(x,s(y)))
Following rules are (at-least) weakly oriented:
f(x) = 2*x
>= x
= x
f(f(x)) = 4*x
>= 0
= f(d(f(x)))
g(c(x,s(y))) = 10
>= 10
= g(c(s(x),y))
** Step 1.b:3: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
f(f(x)) -> f(d(f(x)))
g(c(x,s(y))) -> g(c(s(x),y))
- Weak TRS:
f(x) -> x
f(c(s(x),y)) -> f(c(x,s(y)))
- Signature:
{f/1,g/1} / {c/2,d/1,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,g} and constructors {c,d,s}
+ 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:
none
Following symbols are considered usable:
{f,g}
TcT has computed the following interpretation:
p(c) = [1] x1 + [5]
p(d) = [2]
p(f) = [1] x1 + [6]
p(g) = [1] x1 + [0]
p(s) = [1] x1 + [0]
Following rules are strictly oriented:
f(f(x)) = [1] x + [12]
> [8]
= f(d(f(x)))
Following rules are (at-least) weakly oriented:
f(x) = [1] x + [6]
>= [1] x + [0]
= x
f(c(s(x),y)) = [1] x + [11]
>= [1] x + [11]
= f(c(x,s(y)))
g(c(x,s(y))) = [1] x + [5]
>= [1] x + [5]
= g(c(s(x),y))
** Step 1.b:4: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
g(c(x,s(y))) -> g(c(s(x),y))
- Weak TRS:
f(x) -> x
f(c(s(x),y)) -> f(c(x,s(y)))
f(f(x)) -> f(d(f(x)))
- Signature:
{f/1,g/1} / {c/2,d/1,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,g} and constructors {c,d,s}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
c :: ["A"(0) x "A"(3)] -(3)-> "A"(3)
c :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
d :: ["A"(0)] -(0)-> "A"(4)
f :: ["A"(0)] -(3)-> "A"(0)
g :: ["A"(3)] -(7)-> "A"(14)
s :: ["A"(3)] -(3)-> "A"(3)
s :: ["A"(0)] -(0)-> "A"(0)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"c_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
"d_A" :: ["A"(0)] -(0)-> "A"(1)
"s_A" :: ["A"(1)] -(1)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
g(c(x,s(y))) -> g(c(s(x),y))
2. Weak:
WORST_CASE(Omega(n^1),O(n^1))