* Step 1: DependencyPairs WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
0() -> 1()
f(s(x)) -> f(g(x,x))
g(0(),1()) -> s(0())
- Signature:
{0/0,f/1,g/2} / {1/0,s/1}
- Obligation:
runtime complexity wrt. defined symbols {0,f,g} and constructors {1,s}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following weak dependency pairs:
Strict DPs
0#() -> c_1()
f#(s(x)) -> c_2(f#(g(x,x)))
g#(0(),1()) -> c_3(0#())
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
0#() -> c_1()
f#(s(x)) -> c_2(f#(g(x,x)))
g#(0(),1()) -> c_3(0#())
- Strict TRS:
0() -> 1()
f(s(x)) -> f(g(x,x))
g(0(),1()) -> s(0())
- Signature:
{0/0,f/1,g/2,0#/0,f#/1,g#/2} / {1/0,s/1,c_1/0,c_2/1,c_3/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,f#,g#} and constructors {1,s}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
0() -> 1()
g(0(),1()) -> s(0())
0#() -> c_1()
f#(s(x)) -> c_2(f#(g(x,x)))
* Step 3: PredecessorEstimation WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
0#() -> c_1()
f#(s(x)) -> c_2(f#(g(x,x)))
- Strict TRS:
0() -> 1()
g(0(),1()) -> s(0())
- Signature:
{0/0,f/1,g/2,0#/0,f#/1,g#/2} / {1/0,s/1,c_1/0,c_2/1,c_3/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,f#,g#} and constructors {1,s}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1}
by application of
Pre({1}) = {}.
Here rules are labelled as follows:
1: 0#() -> c_1()
2: f#(s(x)) -> c_2(f#(g(x,x)))
* Step 4: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
f#(s(x)) -> c_2(f#(g(x,x)))
- Strict TRS:
0() -> 1()
g(0(),1()) -> s(0())
- Weak DPs:
0#() -> c_1()
- Signature:
{0/0,f/1,g/2,0#/0,f#/1,g#/2} / {1/0,s/1,c_1/0,c_2/1,c_3/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,f#,g#} and constructors {1,s}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
none
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(1) = [5]
p(f) = [0]
p(g) = [1] x2 + [0]
p(s) = [1] x1 + [0]
p(0#) = [0]
p(f#) = [3]
p(g#) = [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [0]
Following rules are strictly oriented:
f#(s(x)) = [3]
> [0]
= c_2(f#(g(x,x)))
g(0(),1()) = [5]
> [0]
= s(0())
Following rules are (at-least) weakly oriented:
0#() = [0]
>= [0]
= c_1()
0() = [0]
>= [5]
= 1()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: MI WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
0() -> 1()
- Weak DPs:
0#() -> c_1()
f#(s(x)) -> c_2(f#(g(x,x)))
- Weak TRS:
g(0(),1()) -> s(0())
- Signature:
{0/0,f/1,g/2,0#/0,f#/1,g#/2} / {1/0,s/1,c_1/0,c_2/1,c_3/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,f#,g#} and constructors {1,s}
+ Applied Processor:
MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity (Just 0))), miDimension = 1, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity (Just 0))):
The following argument positions are considered usable:
none
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [8]
p(1) = [0]
p(f) = [0]
p(g) = [0]
p(s) = [0]
p(0#) = [1]
p(f#) = [0]
p(g#) = [0]
p(c_1) = [1]
p(c_2) = [8] x_1 + [0]
p(c_3) = [1] x_1 + [1]
Following rules are strictly oriented:
0() = [8]
> [0]
= 1()
Following rules are (at-least) weakly oriented:
0#() = [1]
>= [1]
= c_1()
f#(s(x)) = [0]
>= [0]
= c_2(f#(g(x,x)))
g(0(),1()) = [0]
>= [0]
= s(0())
* Step 6: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
0#() -> c_1()
f#(s(x)) -> c_2(f#(g(x,x)))
- Weak TRS:
0() -> 1()
g(0(),1()) -> s(0())
- Signature:
{0/0,f/1,g/2,0#/0,f#/1,g#/2} / {1/0,s/1,c_1/0,c_2/1,c_3/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,f#,g#} and constructors {1,s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))