* Step 1: Sum WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
b(y,z) -> f(c(c(y,z,z),a(),a()))
b(b(z,y),a()) -> z
c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
- Signature:
{b/2,c/3} / {a/0,f/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {b,c} and constructors {a,f}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: InnermostRuleRemoval WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
b(y,z) -> f(c(c(y,z,z),a(),a()))
b(b(z,y),a()) -> z
c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
- Signature:
{b/2,c/3} / {a/0,f/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {b,c} and constructors {a,f}
+ Applied Processor:
InnermostRuleRemoval
+ Details:
Arguments of following rules are not normal-forms.
b(b(z,y),a()) -> z
All above mentioned rules can be savely removed.
* Step 3: DependencyPairs WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
b(y,z) -> f(c(c(y,z,z),a(),a()))
c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
- Signature:
{b/2,c/3} / {a/0,f/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {b,c} and constructors {a,f}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
b#(y,z) -> c_1(c#(c(y,z,z),a(),a()),c#(y,z,z))
c#(f(z),f(c(a(),x,a())),y) -> c_2(c#(f(b(x,z)),c(z,y,a()),a()),b#(x,z),c#(z,y,a()))
Weak DPs
and mark the set of starting terms.
* Step 4: MI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
b#(y,z) -> c_1(c#(c(y,z,z),a(),a()),c#(y,z,z))
c#(f(z),f(c(a(),x,a())),y) -> c_2(c#(f(b(x,z)),c(z,y,a()),a()),b#(x,z),c#(z,y,a()))
- Weak TRS:
b(y,z) -> f(c(c(y,z,z),a(),a()))
c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
- Signature:
{b/2,c/3,b#/2,c#/3} / {a/0,f/1,c_1/2,c_2/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {b#,c#} and constructors {a,f}
+ Applied Processor:
MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 3, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
The following argument positions are considered usable:
uargs(c_1) = {1,2},
uargs(c_2) = {1,2,3}
Following symbols are considered usable:
{b,c,b#,c#}
TcT has computed the following interpretation:
p(a) = [1]
[0]
[0]
p(b) = [0 0 0] [0]
[0 0 0] x_1 + [2]
[3 2 0] [2]
p(c) = [0 0 0] [0 0 0] [0 0 0] [0]
[0 0 0] x_1 + [0 0 0] x_2 + [0 1 2] x_3 + [0]
[3 0 0] [1 1 0] [0 0 0] [0]
p(f) = [1 1 0] [0]
[0 1 2] x_1 + [0]
[0 0 0] [0]
p(b#) = [2 0 0] [0 2 0] [1]
[2 0 0] x_1 + [0 0 0] x_2 + [0]
[0 0 0] [2 0 2] [1]
p(c#) = [2 0 0] [0 1 0] [0 1 0] [0]
[0 0 0] x_1 + [0 0 0] x_2 + [0 2 0] x_3 + [1]
[0 0 0] [1 1 2] [0 0 3] [0]
p(c_1) = [2 0 0] [1 0 0] [0]
[0 0 0] x_1 + [0 0 0] x_2 + [0]
[0 0 0] [0 0 0] [1]
p(c_2) = [1 0 0] [1 0 0] [1 1 0] [0]
[0 0 0] x_1 + [0 0 0] x_2 + [0 0 0] x_3 + [1]
[1 0 0] [0 1 0] [0 2 0] [0]
Following rules are strictly oriented:
b#(y,z) = [2 0 0] [0 2 0] [1]
[2 0 0] y + [0 0 0] z + [0]
[0 0 0] [2 0 2] [1]
> [2 0 0] [0 2 0] [0]
[0 0 0] y + [0 0 0] z + [0]
[0 0 0] [0 0 0] [1]
= c_1(c#(c(y,z,z),a(),a()),c#(y,z,z))
Following rules are (at-least) weakly oriented:
c#(f(z),f(c(a(),x,a())),y) = [2 2 0] [0 1 0] [2 2 0] [6]
[0 0 0] x + [0 2 0] y + [0 0 0] z + [1]
[2 2 0] [0 0 3] [0 0 0] [6]
>= [2 0 0] [0 1 0] [2 2 0] [6]
[0 0 0] x + [0 0 0] y + [0 0 0] z + [1]
[2 0 0] [0 0 0] [0 0 0] [6]
= c_2(c#(f(b(x,z)),c(z,y,a()),a()),b#(x,z),c#(z,y,a()))
b(y,z) = [0 0 0] [0]
[0 0 0] y + [2]
[3 2 0] [2]
>= [0]
[2]
[0]
= f(c(c(y,z,z),a(),a()))
c(f(z),f(c(a(),x,a())),y) = [0 0 0] [0 0 0] [0 0 0] [0]
[0 0 0] x + [0 1 2] y + [0 0 0] z + [0]
[2 2 0] [0 0 0] [3 3 0] [6]
>= [0]
[0]
[6]
= c(f(b(x,z)),c(z,y,a()),a())
* Step 5: MI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
c#(f(z),f(c(a(),x,a())),y) -> c_2(c#(f(b(x,z)),c(z,y,a()),a()),b#(x,z),c#(z,y,a()))
- Weak DPs:
b#(y,z) -> c_1(c#(c(y,z,z),a(),a()),c#(y,z,z))
- Weak TRS:
b(y,z) -> f(c(c(y,z,z),a(),a()))
c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
- Signature:
{b/2,c/3,b#/2,c#/3} / {a/0,f/1,c_1/2,c_2/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {b#,c#} and constructors {a,f}
+ Applied Processor:
MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 3, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
The following argument positions are considered usable:
uargs(c_1) = {1,2},
uargs(c_2) = {1,2,3}
Following symbols are considered usable:
{b,c,b#,c#}
TcT has computed the following interpretation:
p(a) = [0]
[1]
[1]
p(b) = [0]
[0]
[0]
p(c) = [0 0 0] [0 0 0] [0]
[0 0 0] x_1 + [0 0 0] x_2 + [0]
[0 3 0] [2 0 0] [0]
p(f) = [1 2 1] [0]
[0 0 2] x_1 + [0]
[0 0 1] [0]
p(b#) = [3 0 0] [0 2 1] [2]
[1 0 0] x_1 + [0 0 0] x_2 + [0]
[0 0 0] [1 0 0] [0]
p(c#) = [1 0 0] [0 1 0] [0 1 0] [0]
[2 0 0] x_1 + [0 0 1] x_2 + [2 0 0] x_3 + [2]
[2 0 0] [0 0 0] [0 0 1] [0]
p(c_1) = [1 0 0] [1 0 1] [0]
[0 0 0] x_1 + [0 0 0] x_2 + [0]
[0 0 0] [0 0 0] [0]
p(c_2) = [2 0 0] [1 1 0] [1 0 0] [0]
[1 0 3] x_1 + [0 0 2] x_2 + [0 0 0] x_3 + [1]
[0 0 0] [0 0 1] [0 0 0] [0]
Following rules are strictly oriented:
c#(f(z),f(c(a(),x,a())),y) = [4 0 0] [0 1 0] [1 2 1] [6]
[2 0 0] x + [2 0 0] y + [2 4 2] z + [5]
[0 0 0] [0 0 1] [2 4 2] [0]
> [4 0 0] [0 1 0] [1 2 1] [5]
[0 0 0] x + [0 0 0] y + [2 0 0] z + [5]
[0 0 0] [0 0 0] [1 0 0] [0]
= c_2(c#(f(b(x,z)),c(z,y,a()),a()),b#(x,z),c#(z,y,a()))
Following rules are (at-least) weakly oriented:
b#(y,z) = [3 0 0] [0 2 1] [2]
[1 0 0] y + [0 0 0] z + [0]
[0 0 0] [1 0 0] [0]
>= [3 0 0] [0 2 1] [2]
[0 0 0] y + [0 0 0] z + [0]
[0 0 0] [0 0 0] [0]
= c_1(c#(c(y,z,z),a(),a()),c#(y,z,z))
b(y,z) = [0]
[0]
[0]
>= [0]
[0]
[0]
= f(c(c(y,z,z),a(),a()))
c(f(z),f(c(a(),x,a())),y) = [0 0 0] [0 0 0] [0]
[0 0 0] x + [0 0 0] z + [0]
[4 0 0] [0 0 6] [6]
>= [0]
[0]
[0]
= c(f(b(x,z)),c(z,y,a()),a())
* Step 6: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
b#(y,z) -> c_1(c#(c(y,z,z),a(),a()),c#(y,z,z))
c#(f(z),f(c(a(),x,a())),y) -> c_2(c#(f(b(x,z)),c(z,y,a()),a()),b#(x,z),c#(z,y,a()))
- Weak TRS:
b(y,z) -> f(c(c(y,z,z),a(),a()))
c(f(z),f(c(a(),x,a())),y) -> c(f(b(x,z)),c(z,y,a()),a())
- Signature:
{b/2,c/3,b#/2,c#/3} / {a/0,f/1,c_1/2,c_2/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {b#,c#} and constructors {a,f}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))