*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(g(n__f(X))))
h(X) -> c(n__d(X))
Weak DP Rules:
Weak TRS Rules:
Signature:
{activate/1,c/1,d/1,f/1,h/1} / {g/1,n__d/1,n__f/1}
Obligation:
Full
basic terms: {activate,c,d,f,h}/{g,n__d,n__f}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
We add the following weak dependency pairs:
Strict DPs
activate#(X) -> c_1(X)
activate#(n__d(X)) -> c_2(d#(X))
activate#(n__f(X)) -> c_3(f#(X))
c#(X) -> c_4(d#(activate(X)))
d#(X) -> c_5(X)
f#(X) -> c_6(X)
f#(f(X)) -> c_7(c#(n__f(g(n__f(X)))))
h#(X) -> c_8(c#(n__d(X)))
Weak DPs
and mark the set of starting terms.
*** 1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_1(X)
activate#(n__d(X)) -> c_2(d#(X))
activate#(n__f(X)) -> c_3(f#(X))
c#(X) -> c_4(d#(activate(X)))
d#(X) -> c_5(X)
f#(X) -> c_6(X)
f#(f(X)) -> c_7(c#(n__f(g(n__f(X)))))
h#(X) -> c_8(c#(n__d(X)))
Strict TRS Rules:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(g(n__f(X))))
h(X) -> c(n__d(X))
Weak DP Rules:
Weak TRS Rules:
Signature:
{activate/1,c/1,d/1,f/1,h/1,activate#/1,c#/1,d#/1,f#/1,h#/1} / {g/1,n__d/1,n__f/1,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1}
Obligation:
Full
basic terms: {activate#,c#,d#,f#,h#}/{g,n__d,n__f}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(g(n__f(X))))
activate#(X) -> c_1(X)
activate#(n__d(X)) -> c_2(d#(X))
activate#(n__f(X)) -> c_3(f#(X))
c#(X) -> c_4(d#(activate(X)))
d#(X) -> c_5(X)
f#(X) -> c_6(X)
f#(f(X)) -> c_7(c#(n__f(g(n__f(X)))))
h#(X) -> c_8(c#(n__d(X)))
*** 1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_1(X)
activate#(n__d(X)) -> c_2(d#(X))
activate#(n__f(X)) -> c_3(f#(X))
c#(X) -> c_4(d#(activate(X)))
d#(X) -> c_5(X)
f#(X) -> c_6(X)
f#(f(X)) -> c_7(c#(n__f(g(n__f(X)))))
h#(X) -> c_8(c#(n__d(X)))
Strict TRS Rules:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(g(n__f(X))))
Weak DP Rules:
Weak TRS Rules:
Signature:
{activate/1,c/1,d/1,f/1,h/1,activate#/1,c#/1,d#/1,f#/1,h#/1} / {g/1,n__d/1,n__f/1,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1}
Obligation:
Full
basic terms: {activate#,c#,d#,f#,h#}/{g,n__d,n__f}
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(d) = {1},
uargs(n__d) = {1},
uargs(d#) = {1},
uargs(c_2) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(activate) = [3] x1 + [0]
p(c) = [3] x1 + [0]
p(d) = [1] x1 + [0]
p(f) = [0]
p(g) = [1] x1 + [0]
p(h) = [0]
p(n__d) = [1] x1 + [0]
p(n__f) = [0]
p(activate#) = [3] x1 + [0]
p(c#) = [3] x1 + [0]
p(d#) = [1] x1 + [0]
p(f#) = [0]
p(h#) = [3] x1 + [1]
p(c_1) = [3] x1 + [0]
p(c_2) = [1] x1 + [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [0]
p(c_7) = [1] x1 + [0]
p(c_8) = [1] x1 + [0]
Following rules are strictly oriented:
h#(X) = [3] X + [1]
> [3] X + [0]
= c_8(c#(n__d(X)))
Following rules are (at-least) weakly oriented:
activate#(X) = [3] X + [0]
>= [3] X + [0]
= c_1(X)
activate#(n__d(X)) = [3] X + [0]
>= [1] X + [0]
= c_2(d#(X))
activate#(n__f(X)) = [0]
>= [0]
= c_3(f#(X))
c#(X) = [3] X + [0]
>= [3] X + [0]
= c_4(d#(activate(X)))
d#(X) = [1] X + [0]
>= [1] X + [0]
= c_5(X)
f#(X) = [0]
>= [0]
= c_6(X)
f#(f(X)) = [0]
>= [0]
= c_7(c#(n__f(g(n__f(X)))))
activate(X) = [3] X + [0]
>= [1] X + [0]
= X
activate(n__d(X)) = [3] X + [0]
>= [1] X + [0]
= d(X)
activate(n__f(X)) = [0]
>= [0]
= f(X)
c(X) = [3] X + [0]
>= [3] X + [0]
= d(activate(X))
d(X) = [1] X + [0]
>= [1] X + [0]
= n__d(X)
f(X) = [0]
>= [0]
= n__f(X)
f(f(X)) = [0]
>= [0]
= c(n__f(g(n__f(X))))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_1(X)
activate#(n__d(X)) -> c_2(d#(X))
activate#(n__f(X)) -> c_3(f#(X))
c#(X) -> c_4(d#(activate(X)))
d#(X) -> c_5(X)
f#(X) -> c_6(X)
f#(f(X)) -> c_7(c#(n__f(g(n__f(X)))))
Strict TRS Rules:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(g(n__f(X))))
Weak DP Rules:
h#(X) -> c_8(c#(n__d(X)))
Weak TRS Rules:
Signature:
{activate/1,c/1,d/1,f/1,h/1,activate#/1,c#/1,d#/1,f#/1,h#/1} / {g/1,n__d/1,n__f/1,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1}
Obligation:
Full
basic terms: {activate#,c#,d#,f#,h#}/{g,n__d,n__f}
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(d) = {1},
uargs(n__d) = {1},
uargs(d#) = {1},
uargs(c_2) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(activate) = [3] x1 + [0]
p(c) = [3] x1 + [0]
p(d) = [1] x1 + [0]
p(f) = [0]
p(g) = [1] x1 + [3]
p(h) = [0]
p(n__d) = [1] x1 + [0]
p(n__f) = [2]
p(activate#) = [3] x1 + [0]
p(c#) = [3] x1 + [0]
p(d#) = [1] x1 + [0]
p(f#) = [7]
p(h#) = [3] x1 + [0]
p(c_1) = [3] x1 + [0]
p(c_2) = [1] x1 + [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [0]
p(c_7) = [1] x1 + [0]
p(c_8) = [1] x1 + [0]
Following rules are strictly oriented:
f#(X) = [7]
> [0]
= c_6(X)
f#(f(X)) = [7]
> [6]
= c_7(c#(n__f(g(n__f(X)))))
activate(n__f(X)) = [6]
> [0]
= f(X)
Following rules are (at-least) weakly oriented:
activate#(X) = [3] X + [0]
>= [3] X + [0]
= c_1(X)
activate#(n__d(X)) = [3] X + [0]
>= [1] X + [0]
= c_2(d#(X))
activate#(n__f(X)) = [6]
>= [7]
= c_3(f#(X))
c#(X) = [3] X + [0]
>= [3] X + [0]
= c_4(d#(activate(X)))
d#(X) = [1] X + [0]
>= [1] X + [0]
= c_5(X)
h#(X) = [3] X + [0]
>= [3] X + [0]
= c_8(c#(n__d(X)))
activate(X) = [3] X + [0]
>= [1] X + [0]
= X
activate(n__d(X)) = [3] X + [0]
>= [1] X + [0]
= d(X)
c(X) = [3] X + [0]
>= [3] X + [0]
= d(activate(X))
d(X) = [1] X + [0]
>= [1] X + [0]
= n__d(X)
f(X) = [0]
>= [2]
= n__f(X)
f(f(X)) = [0]
>= [6]
= c(n__f(g(n__f(X))))
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(n^1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_1(X)
activate#(n__d(X)) -> c_2(d#(X))
activate#(n__f(X)) -> c_3(f#(X))
c#(X) -> c_4(d#(activate(X)))
d#(X) -> c_5(X)
Strict TRS Rules:
activate(X) -> X
activate(n__d(X)) -> d(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(g(n__f(X))))
Weak DP Rules:
f#(X) -> c_6(X)
f#(f(X)) -> c_7(c#(n__f(g(n__f(X)))))
h#(X) -> c_8(c#(n__d(X)))
Weak TRS Rules:
activate(n__f(X)) -> f(X)
Signature:
{activate/1,c/1,d/1,f/1,h/1,activate#/1,c#/1,d#/1,f#/1,h#/1} / {g/1,n__d/1,n__f/1,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1}
Obligation:
Full
basic terms: {activate#,c#,d#,f#,h#}/{g,n__d,n__f}
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(d) = {1},
uargs(n__d) = {1},
uargs(d#) = {1},
uargs(c_2) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(activate) = [1] x1 + [2]
p(c) = [8] x1 + [4]
p(d) = [1] x1 + [14]
p(f) = [1]
p(g) = [0]
p(h) = [1]
p(n__d) = [1] x1 + [0]
p(n__f) = [1]
p(activate#) = [4] x1 + [0]
p(c#) = [8] x1 + [3]
p(d#) = [1] x1 + [0]
p(f#) = [13]
p(h#) = [8] x1 + [12]
p(c_1) = [8]
p(c_2) = [1] x1 + [0]
p(c_3) = [1] x1 + [8]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [4]
p(c_6) = [13]
p(c_7) = [1] x1 + [2]
p(c_8) = [1] x1 + [7]
Following rules are strictly oriented:
c#(X) = [8] X + [3]
> [1] X + [2]
= c_4(d#(activate(X)))
activate(X) = [1] X + [2]
> [1] X + [0]
= X
d(X) = [1] X + [14]
> [1] X + [0]
= n__d(X)
Following rules are (at-least) weakly oriented:
activate#(X) = [4] X + [0]
>= [8]
= c_1(X)
activate#(n__d(X)) = [4] X + [0]
>= [1] X + [0]
= c_2(d#(X))
activate#(n__f(X)) = [4]
>= [21]
= c_3(f#(X))
d#(X) = [1] X + [0]
>= [1] X + [4]
= c_5(X)
f#(X) = [13]
>= [13]
= c_6(X)
f#(f(X)) = [13]
>= [13]
= c_7(c#(n__f(g(n__f(X)))))
h#(X) = [8] X + [12]
>= [8] X + [10]
= c_8(c#(n__d(X)))
activate(n__d(X)) = [1] X + [2]
>= [1] X + [14]
= d(X)
activate(n__f(X)) = [3]
>= [1]
= f(X)
c(X) = [8] X + [4]
>= [1] X + [16]
= d(activate(X))
f(X) = [1]
>= [1]
= n__f(X)
f(f(X)) = [1]
>= [12]
= c(n__f(g(n__f(X))))
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(n^1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_1(X)
activate#(n__d(X)) -> c_2(d#(X))
activate#(n__f(X)) -> c_3(f#(X))
d#(X) -> c_5(X)
Strict TRS Rules:
activate(n__d(X)) -> d(X)
c(X) -> d(activate(X))
f(X) -> n__f(X)
f(f(X)) -> c(n__f(g(n__f(X))))
Weak DP Rules:
c#(X) -> c_4(d#(activate(X)))
f#(X) -> c_6(X)
f#(f(X)) -> c_7(c#(n__f(g(n__f(X)))))
h#(X) -> c_8(c#(n__d(X)))
Weak TRS Rules:
activate(X) -> X
activate(n__f(X)) -> f(X)
d(X) -> n__d(X)
Signature:
{activate/1,c/1,d/1,f/1,h/1,activate#/1,c#/1,d#/1,f#/1,h#/1} / {g/1,n__d/1,n__f/1,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1}
Obligation:
Full
basic terms: {activate#,c#,d#,f#,h#}/{g,n__d,n__f}
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(d) = {1},
uargs(n__d) = {1},
uargs(d#) = {1},
uargs(c_2) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(activate) = [2] x1 + [3]
p(c) = [2] x1 + [0]
p(d) = [1] x1 + [1]
p(f) = [1] x1 + [2]
p(g) = [0]
p(h) = [1] x1 + [0]
p(n__d) = [1] x1 + [0]
p(n__f) = [1] x1 + [1]
p(activate#) = [10] x1 + [12]
p(c#) = [3] x1 + [6]
p(d#) = [1] x1 + [0]
p(f#) = [8] x1 + [12]
p(h#) = [3] x1 + [6]
p(c_1) = [1]
p(c_2) = [1] x1 + [0]
p(c_3) = [1] x1 + [7]
p(c_4) = [1] x1 + [3]
p(c_5) = [1] x1 + [2]
p(c_6) = [8] x1 + [1]
p(c_7) = [1] x1 + [15]
p(c_8) = [1] x1 + [0]
Following rules are strictly oriented:
activate#(X) = [10] X + [12]
> [1]
= c_1(X)
activate#(n__d(X)) = [10] X + [12]
> [1] X + [0]
= c_2(d#(X))
activate#(n__f(X)) = [10] X + [22]
> [8] X + [19]
= c_3(f#(X))
activate(n__d(X)) = [2] X + [3]
> [1] X + [1]
= d(X)
f(X) = [1] X + [2]
> [1] X + [1]
= n__f(X)
f(f(X)) = [1] X + [4]
> [2]
= c(n__f(g(n__f(X))))
Following rules are (at-least) weakly oriented:
c#(X) = [3] X + [6]
>= [2] X + [6]
= c_4(d#(activate(X)))
d#(X) = [1] X + [0]
>= [1] X + [2]
= c_5(X)
f#(X) = [8] X + [12]
>= [8] X + [1]
= c_6(X)
f#(f(X)) = [8] X + [28]
>= [24]
= c_7(c#(n__f(g(n__f(X)))))
h#(X) = [3] X + [6]
>= [3] X + [6]
= c_8(c#(n__d(X)))
activate(X) = [2] X + [3]
>= [1] X + [0]
= X
activate(n__f(X)) = [2] X + [5]
>= [1] X + [2]
= f(X)
c(X) = [2] X + [0]
>= [2] X + [4]
= d(activate(X))
d(X) = [1] X + [1]
>= [1] X + [0]
= n__d(X)
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(n^1))] ***
Considered Problem:
Strict DP Rules:
d#(X) -> c_5(X)
Strict TRS Rules:
c(X) -> d(activate(X))
Weak DP Rules:
activate#(X) -> c_1(X)
activate#(n__d(X)) -> c_2(d#(X))
activate#(n__f(X)) -> c_3(f#(X))
c#(X) -> c_4(d#(activate(X)))
f#(X) -> c_6(X)
f#(f(X)) -> c_7(c#(n__f(g(n__f(X)))))
h#(X) -> c_8(c#(n__d(X)))
Weak TRS Rules:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(X)
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(g(n__f(X))))
Signature:
{activate/1,c/1,d/1,f/1,h/1,activate#/1,c#/1,d#/1,f#/1,h#/1} / {g/1,n__d/1,n__f/1,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1}
Obligation:
Full
basic terms: {activate#,c#,d#,f#,h#}/{g,n__d,n__f}
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(d) = {1},
uargs(n__d) = {1},
uargs(d#) = {1},
uargs(c_2) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(activate) = [4] x1 + [4]
p(c) = [4] x1 + [1]
p(d) = [1] x1 + [1]
p(f) = [4]
p(g) = [1] x1 + [2]
p(h) = [1] x1 + [0]
p(n__d) = [1] x1 + [0]
p(n__f) = [0]
p(activate#) = [1] x1 + [6]
p(c#) = [4] x1 + [6]
p(d#) = [1] x1 + [2]
p(f#) = [6]
p(h#) = [4] x1 + [7]
p(c_1) = [1] x1 + [1]
p(c_2) = [1] x1 + [4]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [1]
p(c_6) = [1]
p(c_7) = [1] x1 + [0]
p(c_8) = [1] x1 + [1]
Following rules are strictly oriented:
d#(X) = [1] X + [2]
> [1] X + [1]
= c_5(X)
Following rules are (at-least) weakly oriented:
activate#(X) = [1] X + [6]
>= [1] X + [1]
= c_1(X)
activate#(n__d(X)) = [1] X + [6]
>= [1] X + [6]
= c_2(d#(X))
activate#(n__f(X)) = [6]
>= [6]
= c_3(f#(X))
c#(X) = [4] X + [6]
>= [4] X + [6]
= c_4(d#(activate(X)))
f#(X) = [6]
>= [1]
= c_6(X)
f#(f(X)) = [6]
>= [6]
= c_7(c#(n__f(g(n__f(X)))))
h#(X) = [4] X + [7]
>= [4] X + [7]
= c_8(c#(n__d(X)))
activate(X) = [4] X + [4]
>= [1] X + [0]
= X
activate(n__d(X)) = [4] X + [4]
>= [1] X + [1]
= d(X)
activate(n__f(X)) = [4]
>= [4]
= f(X)
c(X) = [4] X + [1]
>= [4] X + [5]
= d(activate(X))
d(X) = [1] X + [1]
>= [1] X + [0]
= n__d(X)
f(X) = [4]
>= [0]
= n__f(X)
f(f(X)) = [4]
>= [1]
= c(n__f(g(n__f(X))))
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(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
c(X) -> d(activate(X))
Weak DP Rules:
activate#(X) -> c_1(X)
activate#(n__d(X)) -> c_2(d#(X))
activate#(n__f(X)) -> c_3(f#(X))
c#(X) -> c_4(d#(activate(X)))
d#(X) -> c_5(X)
f#(X) -> c_6(X)
f#(f(X)) -> c_7(c#(n__f(g(n__f(X)))))
h#(X) -> c_8(c#(n__d(X)))
Weak TRS Rules:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(X)
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(g(n__f(X))))
Signature:
{activate/1,c/1,d/1,f/1,h/1,activate#/1,c#/1,d#/1,f#/1,h#/1} / {g/1,n__d/1,n__f/1,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1}
Obligation:
Full
basic terms: {activate#,c#,d#,f#,h#}/{g,n__d,n__f}
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(d) = {1},
uargs(n__d) = {1},
uargs(d#) = {1},
uargs(c_2) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_7) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(activate) = [2] x1 + [0]
p(c) = [2] x1 + [1]
p(d) = [1] x1 + [0]
p(f) = [2] x1 + [2]
p(g) = [0]
p(h) = [4] x1 + [0]
p(n__d) = [1] x1 + [0]
p(n__f) = [1] x1 + [1]
p(activate#) = [5] x1 + [1]
p(c#) = [4] x1 + [2]
p(d#) = [1] x1 + [0]
p(f#) = [6]
p(h#) = [4] x1 + [3]
p(c_1) = [1]
p(c_2) = [1] x1 + [1]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [6]
p(c_7) = [1] x1 + [0]
p(c_8) = [1] x1 + [1]
Following rules are strictly oriented:
c(X) = [2] X + [1]
> [2] X + [0]
= d(activate(X))
Following rules are (at-least) weakly oriented:
activate#(X) = [5] X + [1]
>= [1]
= c_1(X)
activate#(n__d(X)) = [5] X + [1]
>= [1] X + [1]
= c_2(d#(X))
activate#(n__f(X)) = [5] X + [6]
>= [6]
= c_3(f#(X))
c#(X) = [4] X + [2]
>= [2] X + [0]
= c_4(d#(activate(X)))
d#(X) = [1] X + [0]
>= [1] X + [0]
= c_5(X)
f#(X) = [6]
>= [6]
= c_6(X)
f#(f(X)) = [6]
>= [6]
= c_7(c#(n__f(g(n__f(X)))))
h#(X) = [4] X + [3]
>= [4] X + [3]
= c_8(c#(n__d(X)))
activate(X) = [2] X + [0]
>= [1] X + [0]
= X
activate(n__d(X)) = [2] X + [0]
>= [1] X + [0]
= d(X)
activate(n__f(X)) = [2] X + [2]
>= [2] X + [2]
= f(X)
d(X) = [1] X + [0]
>= [1] X + [0]
= n__d(X)
f(X) = [2] X + [2]
>= [1] X + [1]
= n__f(X)
f(f(X)) = [4] X + [6]
>= [3]
= c(n__f(g(n__f(X))))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
activate#(X) -> c_1(X)
activate#(n__d(X)) -> c_2(d#(X))
activate#(n__f(X)) -> c_3(f#(X))
c#(X) -> c_4(d#(activate(X)))
d#(X) -> c_5(X)
f#(X) -> c_6(X)
f#(f(X)) -> c_7(c#(n__f(g(n__f(X)))))
h#(X) -> c_8(c#(n__d(X)))
Weak TRS Rules:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(g(n__f(X))))
Signature:
{activate/1,c/1,d/1,f/1,h/1,activate#/1,c#/1,d#/1,f#/1,h#/1} / {g/1,n__d/1,n__f/1,c_1/1,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1}
Obligation:
Full
basic terms: {activate#,c#,d#,f#,h#}/{g,n__d,n__f}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).