*** 1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y)))
b(y,z) -> z
f(c(a(),z,x)) -> b(a(),z)
Weak DP Rules:
Weak TRS Rules:
Signature:
{b/2,f/1} / {a/0,c/3}
Obligation:
Full
basic terms: {b,f}/{a,c}
Applied Processor:
DependencyPairs {dpKind_ = WIDP}
Proof:
We add the following weak dependency pairs:
Strict DPs
b#(x,b(z,y)) -> c_1(f#(b(f(f(z)),c(x,z,y))))
b#(y,z) -> c_2(z)
f#(c(a(),z,x)) -> c_3(b#(a(),z))
Weak DPs
and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
b#(x,b(z,y)) -> c_1(f#(b(f(f(z)),c(x,z,y))))
b#(y,z) -> c_2(z)
f#(c(a(),z,x)) -> c_3(b#(a(),z))
Strict TRS Rules:
b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y)))
b(y,z) -> z
f(c(a(),z,x)) -> b(a(),z)
Weak DP Rules:
Weak TRS Rules:
Signature:
{b/2,f/1,b#/2,f#/1} / {a/0,c/3,c_1/1,c_2/1,c_3/1}
Obligation:
Full
basic terms: {b#,f#}/{a,c}
Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any intersect of strict-rules and rewrite-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(b) = {1,2},
uargs(c) = {1,2,3},
uargs(f) = {1},
uargs(b#) = {2},
uargs(f#) = {1},
uargs(c_1) = {1},
uargs(c_2) = {1},
uargs(c_3) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [0]
[0]
p(b) = [1 0] x1 + [1 1] x2 + [0]
[2 4] [2 1] [3]
p(c) = [1 0] x1 + [1 1] x2 + [1
0] x3 + [2]
[0 0] [0 0] [0
0] [0]
p(f) = [1 0] x1 + [0]
[2 0] [0]
p(b#) = [4 4] x1 + [4 2] x2 + [4]
[0 5] [0 1] [0]
p(f#) = [4 0] x1 + [0]
[0 0] [7]
p(c_1) = [1 0] x1 + [0]
[0 0] [2]
p(c_2) = [4 0] x1 + [1]
[0 1] [0]
p(c_3) = [1 1] x1 + [4]
[0 0] [0]
Following rules are strictly oriented:
b#(x,b(z,y)) = [4 4] x + [8 6] y + [8
8] z + [10]
[0 5] [2 1] [2
4] [3]
> [4 0] x + [4 0] y + [8
4] z + [8]
[0 0] [0 0] [0
0] [2]
= c_1(f#(b(f(f(z)),c(x,z,y))))
b#(y,z) = [4 4] y + [4 2] z + [4]
[0 5] [0 1] [0]
> [4 0] z + [1]
[0 1] [0]
= c_2(z)
b(x,b(z,y)) = [1 0] x + [3 2] y + [3
4] z + [3]
[2 4] [4 3] [4
4] [6]
> [1 0] x + [1 0] y + [2
1] z + [2]
[2 0] [2 0] [4
2] [4]
= f(b(f(f(z)),c(x,z,y)))
f(c(a(),z,x)) = [1 0] x + [1 1] z + [2]
[2 0] [2 2] [4]
> [1 1] z + [0]
[2 1] [3]
= b(a(),z)
Following rules are (at-least) weakly oriented:
f#(c(a(),z,x)) = [4 0] x + [4 4] z + [8]
[0 0] [0 0] [7]
>= [4 3] z + [8]
[0 0] [0]
= c_3(b#(a(),z))
b(y,z) = [1 0] y + [1 1] z + [0]
[2 4] [2 1] [3]
>= [1 0] z + [0]
[0 1] [0]
= z
*** 1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
f#(c(a(),z,x)) -> c_3(b#(a(),z))
Strict TRS Rules:
b(y,z) -> z
Weak DP Rules:
b#(x,b(z,y)) -> c_1(f#(b(f(f(z)),c(x,z,y))))
b#(y,z) -> c_2(z)
Weak TRS Rules:
b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y)))
f(c(a(),z,x)) -> b(a(),z)
Signature:
{b/2,f/1,b#/2,f#/1} / {a/0,c/3,c_1/1,c_2/1,c_3/1}
Obligation:
Full
basic terms: {b#,f#}/{a,c}
Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any intersect of strict-rules and rewrite-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(b) = {1,2},
uargs(c) = {1,2,3},
uargs(f) = {1},
uargs(b#) = {2},
uargs(f#) = {1},
uargs(c_1) = {1},
uargs(c_2) = {1},
uargs(c_3) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [0]
[0]
p(b) = [1 1] x1 + [1 1] x2 + [2]
[4 0] [2 2] [2]
p(c) = [1 0] x1 + [1 1] x2 + [1
0] x3 + [3]
[0 0] [0 0] [0
0] [0]
p(f) = [1 0] x1 + [0]
[2 0] [0]
p(b#) = [1 0] x1 + [1 1] x2 + [5]
[5 0] [0 0] [4]
p(f#) = [1 0] x1 + [4]
[0 0] [1]
p(c_1) = [1 0] x1 + [0]
[0 4] [0]
p(c_2) = [1 1] x1 + [4]
[0 0] [2]
p(c_3) = [1 0] x1 + [2]
[0 0] [1]
Following rules are strictly oriented:
b(y,z) = [1 1] y + [1 1] z + [2]
[4 0] [2 2] [2]
> [1 0] z + [0]
[0 1] [0]
= z
Following rules are (at-least) weakly oriented:
b#(x,b(z,y)) = [1 0] x + [3 3] y + [5
1] z + [9]
[5 0] [0 0] [0
0] [4]
>= [1 0] x + [1 0] y + [4
1] z + [9]
[0 0] [0 0] [0
0] [4]
= c_1(f#(b(f(f(z)),c(x,z,y))))
b#(y,z) = [1 0] y + [1 1] z + [5]
[5 0] [0 0] [4]
>= [1 1] z + [4]
[0 0] [2]
= c_2(z)
f#(c(a(),z,x)) = [1 0] x + [1 1] z + [7]
[0 0] [0 0] [1]
>= [1 1] z + [7]
[0 0] [1]
= c_3(b#(a(),z))
b(x,b(z,y)) = [1 1] x + [3 3] y + [ 5
1] z + [6]
[4 0] [6 6] [10
2] [10]
>= [1 0] x + [1 0] y + [4
1] z + [5]
[2 0] [2 0] [8
2] [10]
= f(b(f(f(z)),c(x,z,y)))
f(c(a(),z,x)) = [1 0] x + [1 1] z + [3]
[2 0] [2 2] [6]
>= [1 1] z + [2]
[2 2] [2]
= b(a(),z)
*** 1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
f#(c(a(),z,x)) -> c_3(b#(a(),z))
Strict TRS Rules:
Weak DP Rules:
b#(x,b(z,y)) -> c_1(f#(b(f(f(z)),c(x,z,y))))
b#(y,z) -> c_2(z)
Weak TRS Rules:
b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y)))
b(y,z) -> z
f(c(a(),z,x)) -> b(a(),z)
Signature:
{b/2,f/1,b#/2,f#/1} / {a/0,c/3,c_1/1,c_2/1,c_3/1}
Obligation:
Full
basic terms: {b#,f#}/{a,c}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 3, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 3, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: f#(c(a(),z,x)) -> c_3(b#(a(),z))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
f#(c(a(),z,x)) -> c_3(b#(a(),z))
Strict TRS Rules:
Weak DP Rules:
b#(x,b(z,y)) -> c_1(f#(b(f(f(z)),c(x,z,y))))
b#(y,z) -> c_2(z)
Weak TRS Rules:
b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y)))
b(y,z) -> z
f(c(a(),z,x)) -> b(a(),z)
Signature:
{b/2,f/1,b#/2,f#/1} / {a/0,c/3,c_1/1,c_2/1,c_3/1}
Obligation:
Full
basic terms: {b#,f#}/{a,c}
Applied Processor:
NaturalMI {miDimension = 3, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(c_1) = {1},
uargs(c_2) = {1},
uargs(c_3) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [0]
[0]
[0]
p(b) = [0 0 0] [1 0 1] [0]
[0 0 0] x1 + [0 1 1] x2 + [0]
[1 1 1] [0 0 1] [1]
p(c) = [1 1 1] [0 0 0] [0]
[0 0 1] x2 + [0 0 1] x3 + [0]
[0 0 0] [0 0 0] [0]
p(f) = [1 0 0] [0]
[1 0 0] x1 + [0]
[0 1 0] [1]
p(b#) = [1 0 0] [1 1 1] [0]
[1 0 1] x1 + [0 1 0] x2 + [1]
[0 0 0] [0 0 0] [1]
p(f#) = [1 0 0] [1]
[0 0 0] x1 + [1]
[0 0 0] [1]
p(c_1) = [1 0 0] [0]
[0 0 1] x1 + [0]
[0 0 0] [1]
p(c_2) = [1 0 0] [0]
[0 1 0] x1 + [0]
[0 0 0] [0]
p(c_3) = [1 0 0] [0]
[0 0 1] x1 + [0]
[0 0 0] [1]
Following rules are strictly oriented:
f#(c(a(),z,x)) = [1 1 1] [1]
[0 0 0] z + [1]
[0 0 0] [1]
> [1 1 1] [0]
[0 0 0] z + [1]
[0 0 0] [1]
= c_3(b#(a(),z))
Following rules are (at-least) weakly oriented:
b#(x,b(z,y)) = [1 0 0] [1 1 3] [1 1
1] [1]
[1 0 1] x + [0 1 1] y + [0 0
0] z + [1]
[0 0 0] [0 0 0] [0 0
0] [1]
>= [1 1 1] [1]
[0 0 0] z + [1]
[0 0 0] [1]
= c_1(f#(b(f(f(z)),c(x,z,y))))
b#(y,z) = [1 0 0] [1 1 1] [0]
[1 0 1] y + [0 1 0] z + [1]
[0 0 0] [0 0 0] [1]
>= [1 0 0] [0]
[0 1 0] z + [0]
[0 0 0] [0]
= c_2(z)
b(x,b(z,y)) = [0 0 0] [1 0 2] [1 1
1] [1]
[0 0 0] x + [0 1 2] y + [1 1
1] z + [1]
[1 1 1] [0 0 1] [1 1
1] [2]
>= [0 0 0] [1 1 1] [0]
[0 0 0] y + [1 1 1] z + [0]
[0 0 1] [0 0 1] [1]
= f(b(f(f(z)),c(x,z,y)))
b(y,z) = [0 0 0] [1 0 1] [0]
[0 0 0] y + [0 1 1] z + [0]
[1 1 1] [0 0 1] [1]
>= [1 0 0] [0]
[0 1 0] z + [0]
[0 0 1] [0]
= z
f(c(a(),z,x)) = [0 0 0] [1 1 1] [0]
[0 0 0] x + [1 1 1] z + [0]
[0 0 1] [0 0 1] [1]
>= [1 0 1] [0]
[0 1 1] z + [0]
[0 0 1] [1]
= b(a(),z)
*** 1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
b#(x,b(z,y)) -> c_1(f#(b(f(f(z)),c(x,z,y))))
b#(y,z) -> c_2(z)
f#(c(a(),z,x)) -> c_3(b#(a(),z))
Weak TRS Rules:
b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y)))
b(y,z) -> z
f(c(a(),z,x)) -> b(a(),z)
Signature:
{b/2,f/1,b#/2,f#/1} / {a/0,c/3,c_1/1,c_2/1,c_3/1}
Obligation:
Full
basic terms: {b#,f#}/{a,c}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
b#(x,b(z,y)) -> c_1(f#(b(f(f(z)),c(x,z,y))))
b#(y,z) -> c_2(z)
f#(c(a(),z,x)) -> c_3(b#(a(),z))
Weak TRS Rules:
b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y)))
b(y,z) -> z
f(c(a(),z,x)) -> b(a(),z)
Signature:
{b/2,f/1,b#/2,f#/1} / {a/0,c/3,c_1/1,c_2/1,c_3/1}
Obligation:
Full
basic terms: {b#,f#}/{a,c}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:b#(x,b(z,y)) -> c_1(f#(b(f(f(z)),c(x,z,y))))
-->_1 f#(c(a(),z,x)) -> c_3(b#(a(),z)):3
2:W:b#(y,z) -> c_2(z)
-->_1 f#(c(a(),z,x)) -> c_3(b#(a(),z)):3
-->_1 b#(y,z) -> c_2(z):2
-->_1 b#(x,b(z,y)) -> c_1(f#(b(f(f(z)),c(x,z,y)))):1
3:W:f#(c(a(),z,x)) -> c_3(b#(a(),z))
-->_1 b#(y,z) -> c_2(z):2
-->_1 b#(x,b(z,y)) -> c_1(f#(b(f(f(z)),c(x,z,y)))):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: b#(x,b(z,y)) -> c_1(f#(b(f(f(z))
,c(x,z,y))))
3: f#(c(a(),z,x)) -> c_3(b#(a(),z))
2: b#(y,z) -> c_2(z)
*** 1.1.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y)))
b(y,z) -> z
f(c(a(),z,x)) -> b(a(),z)
Signature:
{b/2,f/1,b#/2,f#/1} / {a/0,c/3,c_1/1,c_2/1,c_3/1}
Obligation:
Full
basic terms: {b#,f#}/{a,c}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).