*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
f(k(a()),k(b()),X) -> f(X,X,X)
g(X) -> u(h(X),h(X),X)
h(d()) -> c(a())
h(d()) -> c(b())
u(d(),c(Y),X) -> k(Y)
Weak DP Rules:
Weak TRS Rules:
Signature:
{f/3,g/1,h/1,u/3} / {a/0,b/0,c/1,d/0,k/1}
Obligation:
Full
basic terms: {f,g,h,u}/{a,b,c,d,k}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
We add the following weak dependency pairs:
Strict DPs
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
g#(X) -> c_2(u#(h(X),h(X),X))
h#(d()) -> c_3()
h#(d()) -> c_4()
u#(d(),c(Y),X) -> c_5(Y)
Weak DPs
and mark the set of starting terms.
*** 1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
g#(X) -> c_2(u#(h(X),h(X),X))
h#(d()) -> c_3()
h#(d()) -> c_4()
u#(d(),c(Y),X) -> c_5(Y)
Strict TRS Rules:
f(k(a()),k(b()),X) -> f(X,X,X)
g(X) -> u(h(X),h(X),X)
h(d()) -> c(a())
h(d()) -> c(b())
u(d(),c(Y),X) -> k(Y)
Weak DP Rules:
Weak TRS Rules:
Signature:
{f/3,g/1,h/1,u/3,f#/3,g#/1,h#/1,u#/3} / {a/0,b/0,c/1,d/0,k/1,c_1/1,c_2/1,c_3/0,c_4/0,c_5/1}
Obligation:
Full
basic terms: {f#,g#,h#,u#}/{a,b,c,d,k}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
h(d()) -> c(a())
h(d()) -> c(b())
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
g#(X) -> c_2(u#(h(X),h(X),X))
h#(d()) -> c_3()
h#(d()) -> c_4()
u#(d(),c(Y),X) -> c_5(Y)
*** 1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
g#(X) -> c_2(u#(h(X),h(X),X))
h#(d()) -> c_3()
h#(d()) -> c_4()
u#(d(),c(Y),X) -> c_5(Y)
Strict TRS Rules:
h(d()) -> c(a())
h(d()) -> c(b())
Weak DP Rules:
Weak TRS Rules:
Signature:
{f/3,g/1,h/1,u/3,f#/3,g#/1,h#/1,u#/3} / {a/0,b/0,c/1,d/0,k/1,c_1/1,c_2/1,c_3/0,c_4/0,c_5/1}
Obligation:
Full
basic terms: {f#,g#,h#,u#}/{a,b,c,d,k}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{3,4}
by application of
Pre({3,4}) = {5}.
Here rules are labelled as follows:
1: f#(k(a()),k(b()),X) -> c_1(f#(X
,X
,X))
2: g#(X) -> c_2(u#(h(X),h(X),X))
3: h#(d()) -> c_3()
4: h#(d()) -> c_4()
5: u#(d(),c(Y),X) -> c_5(Y)
*** 1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
g#(X) -> c_2(u#(h(X),h(X),X))
u#(d(),c(Y),X) -> c_5(Y)
Strict TRS Rules:
h(d()) -> c(a())
h(d()) -> c(b())
Weak DP Rules:
h#(d()) -> c_3()
h#(d()) -> c_4()
Weak TRS Rules:
Signature:
{f/3,g/1,h/1,u/3,f#/3,g#/1,h#/1,u#/3} / {a/0,b/0,c/1,d/0,k/1,c_1/1,c_2/1,c_3/0,c_4/0,c_5/1}
Obligation:
Full
basic terms: {f#,g#,h#,u#}/{a,b,c,d,k}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
uargs(u#) = {1,2},
uargs(c_2) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [0]
p(b) = [0]
p(c) = [0]
p(d) = [0]
p(f) = [0]
p(g) = [0]
p(h) = [6]
p(k) = [1] x1 + [0]
p(u) = [0]
p(f#) = [0]
p(g#) = [2]
p(h#) = [0]
p(u#) = [1] x1 + [1] x2 + [0]
p(c_1) = [8] x1 + [0]
p(c_2) = [1] x1 + [0]
p(c_3) = [0]
p(c_4) = [0]
p(c_5) = [0]
Following rules are strictly oriented:
h(d()) = [6]
> [0]
= c(a())
h(d()) = [6]
> [0]
= c(b())
Following rules are (at-least) weakly oriented:
f#(k(a()),k(b()),X) = [0]
>= [0]
= c_1(f#(X,X,X))
g#(X) = [2]
>= [12]
= c_2(u#(h(X),h(X),X))
h#(d()) = [0]
>= [0]
= c_3()
h#(d()) = [0]
>= [0]
= c_4()
u#(d(),c(Y),X) = [0]
>= [0]
= c_5(Y)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
g#(X) -> c_2(u#(h(X),h(X),X))
u#(d(),c(Y),X) -> c_5(Y)
Strict TRS Rules:
Weak DP Rules:
h#(d()) -> c_3()
h#(d()) -> c_4()
Weak TRS Rules:
h(d()) -> c(a())
h(d()) -> c(b())
Signature:
{f/3,g/1,h/1,u/3,f#/3,g#/1,h#/1,u#/3} / {a/0,b/0,c/1,d/0,k/1,c_1/1,c_2/1,c_3/0,c_4/0,c_5/1}
Obligation:
Full
basic terms: {f#,g#,h#,u#}/{a,b,c,d,k}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(u#) = {1,2},
uargs(c_2) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [0]
p(b) = [0]
p(c) = [0]
p(d) = [7]
p(f) = [0]
p(g) = [0]
p(h) = [0]
p(k) = [0]
p(u) = [0]
p(f#) = [0]
p(g#) = [0]
p(h#) = [0]
p(u#) = [1] x1 + [1] x2 + [0]
p(c_1) = [0]
p(c_2) = [1] x1 + [0]
p(c_3) = [0]
p(c_4) = [0]
p(c_5) = [0]
Following rules are strictly oriented:
u#(d(),c(Y),X) = [7]
> [0]
= c_5(Y)
Following rules are (at-least) weakly oriented:
f#(k(a()),k(b()),X) = [0]
>= [0]
= c_1(f#(X,X,X))
g#(X) = [0]
>= [0]
= c_2(u#(h(X),h(X),X))
h#(d()) = [0]
>= [0]
= c_3()
h#(d()) = [0]
>= [0]
= c_4()
h(d()) = [0]
>= [0]
= c(a())
h(d()) = [0]
>= [0]
= c(b())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
g#(X) -> c_2(u#(h(X),h(X),X))
Strict TRS Rules:
Weak DP Rules:
h#(d()) -> c_3()
h#(d()) -> c_4()
u#(d(),c(Y),X) -> c_5(Y)
Weak TRS Rules:
h(d()) -> c(a())
h(d()) -> c(b())
Signature:
{f/3,g/1,h/1,u/3,f#/3,g#/1,h#/1,u#/3} / {a/0,b/0,c/1,d/0,k/1,c_1/1,c_2/1,c_3/0,c_4/0,c_5/1}
Obligation:
Full
basic terms: {f#,g#,h#,u#}/{a,b,c,d,k}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(u#) = {1,2},
uargs(c_2) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [0]
p(b) = [0]
p(c) = [8]
p(d) = [4]
p(f) = [1] x1 + [2] x2 + [1] x3 + [0]
p(g) = [2] x1 + [1]
p(h) = [2] x1 + [4]
p(k) = [3]
p(u) = [1] x3 + [1]
p(f#) = [6] x1 + [13]
p(g#) = [4] x1 + [1]
p(h#) = [6]
p(u#) = [1] x1 + [1] x2 + [8]
p(c_1) = [1]
p(c_2) = [1] x1 + [0]
p(c_3) = [6]
p(c_4) = [6]
p(c_5) = [1]
Following rules are strictly oriented:
f#(k(a()),k(b()),X) = [31]
> [1]
= c_1(f#(X,X,X))
Following rules are (at-least) weakly oriented:
g#(X) = [4] X + [1]
>= [4] X + [16]
= c_2(u#(h(X),h(X),X))
h#(d()) = [6]
>= [6]
= c_3()
h#(d()) = [6]
>= [6]
= c_4()
u#(d(),c(Y),X) = [20]
>= [1]
= c_5(Y)
h(d()) = [12]
>= [8]
= c(a())
h(d()) = [12]
>= [8]
= c(b())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
g#(X) -> c_2(u#(h(X),h(X),X))
Strict TRS Rules:
Weak DP Rules:
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
h#(d()) -> c_3()
h#(d()) -> c_4()
u#(d(),c(Y),X) -> c_5(Y)
Weak TRS Rules:
h(d()) -> c(a())
h(d()) -> c(b())
Signature:
{f/3,g/1,h/1,u/3,f#/3,g#/1,h#/1,u#/3} / {a/0,b/0,c/1,d/0,k/1,c_1/1,c_2/1,c_3/0,c_4/0,c_5/1}
Obligation:
Full
basic terms: {f#,g#,h#,u#}/{a,b,c,d,k}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(u#) = {1,2},
uargs(c_2) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [0]
p(b) = [0]
p(c) = [0]
p(d) = [0]
p(f) = [0]
p(g) = [0]
p(h) = [0]
p(k) = [0]
p(u) = [0]
p(f#) = [0]
p(g#) = [1]
p(h#) = [0]
p(u#) = [1] x1 + [1] x2 + [0]
p(c_1) = [0]
p(c_2) = [1] x1 + [0]
p(c_3) = [0]
p(c_4) = [0]
p(c_5) = [0]
Following rules are strictly oriented:
g#(X) = [1]
> [0]
= c_2(u#(h(X),h(X),X))
Following rules are (at-least) weakly oriented:
f#(k(a()),k(b()),X) = [0]
>= [0]
= c_1(f#(X,X,X))
h#(d()) = [0]
>= [0]
= c_3()
h#(d()) = [0]
>= [0]
= c_4()
u#(d(),c(Y),X) = [0]
>= [0]
= c_5(Y)
h(d()) = [0]
>= [0]
= c(a())
h(d()) = [0]
>= [0]
= c(b())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
g#(X) -> c_2(u#(h(X),h(X),X))
h#(d()) -> c_3()
h#(d()) -> c_4()
u#(d(),c(Y),X) -> c_5(Y)
Weak TRS Rules:
h(d()) -> c(a())
h(d()) -> c(b())
Signature:
{f/3,g/1,h/1,u/3,f#/3,g#/1,h#/1,u#/3} / {a/0,b/0,c/1,d/0,k/1,c_1/1,c_2/1,c_3/0,c_4/0,c_5/1}
Obligation:
Full
basic terms: {f#,g#,h#,u#}/{a,b,c,d,k}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).