*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
Weak DP Rules:
Weak TRS Rules:
Signature:
{a/0,activate/1,f/1,g/1} / {c/1,n__a/0,n__f/1,n__g/1}
Obligation:
Full
basic terms: {a,activate,f,g}/{c,n__a,n__f,n__g}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
We add the following weak dependency pairs:
Strict DPs
a#() -> c_1()
activate#(X) -> c_2(X)
activate#(n__a()) -> c_3(a#())
activate#(n__f(X)) -> c_4(f#(activate(X)))
activate#(n__g(X)) -> c_5(g#(activate(X)))
f#(X) -> c_6(X)
f#(f(a())) -> c_7()
g#(X) -> c_8(X)
Weak DPs
and mark the set of starting terms.
*** 1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
a#() -> c_1()
activate#(X) -> c_2(X)
activate#(n__a()) -> c_3(a#())
activate#(n__f(X)) -> c_4(f#(activate(X)))
activate#(n__g(X)) -> c_5(g#(activate(X)))
f#(X) -> c_6(X)
f#(f(a())) -> c_7()
g#(X) -> c_8(X)
Strict TRS Rules:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
Weak DP Rules:
Weak TRS Rules:
Signature:
{a/0,activate/1,f/1,g/1,a#/0,activate#/1,f#/1,g#/1} / {c/1,n__a/0,n__f/1,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1}
Obligation:
Full
basic terms: {a#,activate#,f#,g#}/{c,n__a,n__f,n__g}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{1,7}
by application of
Pre({1,7}) = {2,3,4,6,8}.
Here rules are labelled as follows:
1: a#() -> c_1()
2: activate#(X) -> c_2(X)
3: activate#(n__a()) -> c_3(a#())
4: activate#(n__f(X)) ->
c_4(f#(activate(X)))
5: activate#(n__g(X)) ->
c_5(g#(activate(X)))
6: f#(X) -> c_6(X)
7: f#(f(a())) -> c_7()
8: g#(X) -> c_8(X)
*** 1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_2(X)
activate#(n__a()) -> c_3(a#())
activate#(n__f(X)) -> c_4(f#(activate(X)))
activate#(n__g(X)) -> c_5(g#(activate(X)))
f#(X) -> c_6(X)
g#(X) -> c_8(X)
Strict TRS Rules:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
Weak DP Rules:
a#() -> c_1()
f#(f(a())) -> c_7()
Weak TRS Rules:
Signature:
{a/0,activate/1,f/1,g/1,a#/0,activate#/1,f#/1,g#/1} / {c/1,n__a/0,n__f/1,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1}
Obligation:
Full
basic terms: {a#,activate#,f#,g#}/{c,n__a,n__f,n__g}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{2}
by application of
Pre({2}) = {1,5,6}.
Here rules are labelled as follows:
1: activate#(X) -> c_2(X)
2: activate#(n__a()) -> c_3(a#())
3: activate#(n__f(X)) ->
c_4(f#(activate(X)))
4: activate#(n__g(X)) ->
c_5(g#(activate(X)))
5: f#(X) -> c_6(X)
6: g#(X) -> c_8(X)
7: a#() -> c_1()
8: f#(f(a())) -> c_7()
*** 1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_2(X)
activate#(n__f(X)) -> c_4(f#(activate(X)))
activate#(n__g(X)) -> c_5(g#(activate(X)))
f#(X) -> c_6(X)
g#(X) -> c_8(X)
Strict TRS Rules:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
Weak DP Rules:
a#() -> c_1()
activate#(n__a()) -> c_3(a#())
f#(f(a())) -> c_7()
Weak TRS Rules:
Signature:
{a/0,activate/1,f/1,g/1,a#/0,activate#/1,f#/1,g#/1} / {c/1,n__a/0,n__f/1,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1}
Obligation:
Full
basic terms: {a#,activate#,f#,g#}/{c,n__a,n__f,n__g}
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(f) = {1},
uargs(g) = {1},
uargs(n__f) = {1},
uargs(n__g) = {1},
uargs(f#) = {1},
uargs(g#) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [0]
p(activate) = [3] x1 + [0]
p(c) = [0]
p(f) = [1] x1 + [0]
p(g) = [1] x1 + [0]
p(n__a) = [0]
p(n__f) = [1] x1 + [0]
p(n__g) = [1] x1 + [1]
p(a#) = [0]
p(activate#) = [3] x1 + [0]
p(f#) = [1] x1 + [0]
p(g#) = [1] x1 + [3]
p(c_1) = [0]
p(c_2) = [3] x1 + [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [1] x1 + [0]
p(c_7) = [0]
p(c_8) = [1] x1 + [0]
Following rules are strictly oriented:
g#(X) = [1] X + [3]
> [1] X + [0]
= c_8(X)
activate(n__g(X)) = [3] X + [3]
> [3] X + [0]
= g(activate(X))
Following rules are (at-least) weakly oriented:
a#() = [0]
>= [0]
= c_1()
activate#(X) = [3] X + [0]
>= [3] X + [0]
= c_2(X)
activate#(n__a()) = [0]
>= [0]
= c_3(a#())
activate#(n__f(X)) = [3] X + [0]
>= [3] X + [0]
= c_4(f#(activate(X)))
activate#(n__g(X)) = [3] X + [3]
>= [3] X + [3]
= c_5(g#(activate(X)))
f#(X) = [1] X + [0]
>= [1] X + [0]
= c_6(X)
f#(f(a())) = [0]
>= [0]
= c_7()
a() = [0]
>= [0]
= n__a()
activate(X) = [3] X + [0]
>= [1] X + [0]
= X
activate(n__a()) = [0]
>= [0]
= a()
activate(n__f(X)) = [3] X + [0]
>= [3] X + [0]
= f(activate(X))
f(X) = [1] X + [0]
>= [1] X + [0]
= n__f(X)
f(f(a())) = [0]
>= [0]
= c(n__f(n__g(n__f(n__a()))))
g(X) = [1] X + [0]
>= [1] X + [1]
= n__g(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_2(X)
activate#(n__f(X)) -> c_4(f#(activate(X)))
activate#(n__g(X)) -> c_5(g#(activate(X)))
f#(X) -> c_6(X)
Strict TRS Rules:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
f(X) -> n__f(X)
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
Weak DP Rules:
a#() -> c_1()
activate#(n__a()) -> c_3(a#())
f#(f(a())) -> c_7()
g#(X) -> c_8(X)
Weak TRS Rules:
activate(n__g(X)) -> g(activate(X))
Signature:
{a/0,activate/1,f/1,g/1,a#/0,activate#/1,f#/1,g#/1} / {c/1,n__a/0,n__f/1,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1}
Obligation:
Full
basic terms: {a#,activate#,f#,g#}/{c,n__a,n__f,n__g}
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(f) = {1},
uargs(g) = {1},
uargs(n__f) = {1},
uargs(n__g) = {1},
uargs(f#) = {1},
uargs(g#) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [8]
p(activate) = [1] x1 + [1]
p(c) = [0]
p(f) = [1] x1 + [0]
p(g) = [1] x1 + [4]
p(n__a) = [7]
p(n__f) = [1] x1 + [0]
p(n__g) = [1] x1 + [15]
p(a#) = [2]
p(activate#) = [1] x1 + [0]
p(f#) = [1] x1 + [8]
p(g#) = [1] x1 + [1]
p(c_1) = [0]
p(c_2) = [1] x1 + [1]
p(c_3) = [1] x1 + [4]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [15]
p(c_6) = [1] x1 + [4]
p(c_7) = [8]
p(c_8) = [1] x1 + [0]
Following rules are strictly oriented:
f#(X) = [1] X + [8]
> [1] X + [4]
= c_6(X)
a() = [8]
> [7]
= n__a()
activate(X) = [1] X + [1]
> [1] X + [0]
= X
f(f(a())) = [8]
> [0]
= c(n__f(n__g(n__f(n__a()))))
Following rules are (at-least) weakly oriented:
a#() = [2]
>= [0]
= c_1()
activate#(X) = [1] X + [0]
>= [1] X + [1]
= c_2(X)
activate#(n__a()) = [7]
>= [6]
= c_3(a#())
activate#(n__f(X)) = [1] X + [0]
>= [1] X + [9]
= c_4(f#(activate(X)))
activate#(n__g(X)) = [1] X + [15]
>= [1] X + [17]
= c_5(g#(activate(X)))
f#(f(a())) = [16]
>= [8]
= c_7()
g#(X) = [1] X + [1]
>= [1] X + [0]
= c_8(X)
activate(n__a()) = [8]
>= [8]
= a()
activate(n__f(X)) = [1] X + [1]
>= [1] X + [1]
= f(activate(X))
activate(n__g(X)) = [1] X + [16]
>= [1] X + [5]
= g(activate(X))
f(X) = [1] X + [0]
>= [1] X + [0]
= n__f(X)
g(X) = [1] X + [4]
>= [1] X + [15]
= n__g(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_2(X)
activate#(n__f(X)) -> c_4(f#(activate(X)))
activate#(n__g(X)) -> c_5(g#(activate(X)))
Strict TRS Rules:
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
f(X) -> n__f(X)
g(X) -> n__g(X)
Weak DP Rules:
a#() -> c_1()
activate#(n__a()) -> c_3(a#())
f#(X) -> c_6(X)
f#(f(a())) -> c_7()
g#(X) -> c_8(X)
Weak TRS Rules:
a() -> n__a()
activate(X) -> X
activate(n__g(X)) -> g(activate(X))
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
Signature:
{a/0,activate/1,f/1,g/1,a#/0,activate#/1,f#/1,g#/1} / {c/1,n__a/0,n__f/1,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1}
Obligation:
Full
basic terms: {a#,activate#,f#,g#}/{c,n__a,n__f,n__g}
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(f) = {1},
uargs(g) = {1},
uargs(n__f) = {1},
uargs(n__g) = {1},
uargs(f#) = {1},
uargs(g#) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [0]
p(activate) = [3] x1 + [0]
p(c) = [1] x1 + [1]
p(f) = [1] x1 + [1]
p(g) = [1] x1 + [3]
p(n__a) = [0]
p(n__f) = [1] x1 + [0]
p(n__g) = [1] x1 + [1]
p(a#) = [0]
p(activate#) = [3] x1 + [0]
p(f#) = [1] x1 + [0]
p(g#) = [1] x1 + [0]
p(c_1) = [0]
p(c_2) = [3] x1 + [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [1] x1 + [0]
p(c_7) = [1]
p(c_8) = [1] x1 + [0]
Following rules are strictly oriented:
activate#(n__g(X)) = [3] X + [3]
> [3] X + [0]
= c_5(g#(activate(X)))
f(X) = [1] X + [1]
> [1] X + [0]
= n__f(X)
g(X) = [1] X + [3]
> [1] X + [1]
= n__g(X)
Following rules are (at-least) weakly oriented:
a#() = [0]
>= [0]
= c_1()
activate#(X) = [3] X + [0]
>= [3] X + [0]
= c_2(X)
activate#(n__a()) = [0]
>= [0]
= c_3(a#())
activate#(n__f(X)) = [3] X + [0]
>= [3] X + [0]
= c_4(f#(activate(X)))
f#(X) = [1] X + [0]
>= [1] X + [0]
= c_6(X)
f#(f(a())) = [1]
>= [1]
= c_7()
g#(X) = [1] X + [0]
>= [1] X + [0]
= c_8(X)
a() = [0]
>= [0]
= n__a()
activate(X) = [3] X + [0]
>= [1] X + [0]
= X
activate(n__a()) = [0]
>= [0]
= a()
activate(n__f(X)) = [3] X + [0]
>= [3] X + [1]
= f(activate(X))
activate(n__g(X)) = [3] X + [3]
>= [3] X + [3]
= g(activate(X))
f(f(a())) = [2]
>= [2]
= c(n__f(n__g(n__f(n__a()))))
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:
activate#(X) -> c_2(X)
activate#(n__f(X)) -> c_4(f#(activate(X)))
Strict TRS Rules:
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
Weak DP Rules:
a#() -> c_1()
activate#(n__a()) -> c_3(a#())
activate#(n__g(X)) -> c_5(g#(activate(X)))
f#(X) -> c_6(X)
f#(f(a())) -> c_7()
g#(X) -> c_8(X)
Weak TRS Rules:
a() -> n__a()
activate(X) -> X
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
Signature:
{a/0,activate/1,f/1,g/1,a#/0,activate#/1,f#/1,g#/1} / {c/1,n__a/0,n__f/1,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1}
Obligation:
Full
basic terms: {a#,activate#,f#,g#}/{c,n__a,n__f,n__g}
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(f) = {1},
uargs(g) = {1},
uargs(n__f) = {1},
uargs(n__g) = {1},
uargs(f#) = {1},
uargs(g#) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [1]
p(activate) = [2] x1 + [0]
p(c) = [1] x1 + [0]
p(f) = [1] x1 + [0]
p(g) = [1] x1 + [0]
p(n__a) = [1]
p(n__f) = [1] x1 + [0]
p(n__g) = [1] x1 + [0]
p(a#) = [3]
p(activate#) = [2] x1 + [1]
p(f#) = [1] x1 + [0]
p(g#) = [1] x1 + [0]
p(c_1) = [3]
p(c_2) = [2] x1 + [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [1]
p(c_6) = [1] x1 + [0]
p(c_7) = [1]
p(c_8) = [1] x1 + [0]
Following rules are strictly oriented:
activate#(X) = [2] X + [1]
> [2] X + [0]
= c_2(X)
activate#(n__f(X)) = [2] X + [1]
> [2] X + [0]
= c_4(f#(activate(X)))
activate(n__a()) = [2]
> [1]
= a()
Following rules are (at-least) weakly oriented:
a#() = [3]
>= [3]
= c_1()
activate#(n__a()) = [3]
>= [3]
= c_3(a#())
activate#(n__g(X)) = [2] X + [1]
>= [2] X + [1]
= c_5(g#(activate(X)))
f#(X) = [1] X + [0]
>= [1] X + [0]
= c_6(X)
f#(f(a())) = [1]
>= [1]
= c_7()
g#(X) = [1] X + [0]
>= [1] X + [0]
= c_8(X)
a() = [1]
>= [1]
= n__a()
activate(X) = [2] X + [0]
>= [1] X + [0]
= X
activate(n__f(X)) = [2] X + [0]
>= [2] X + [0]
= f(activate(X))
activate(n__g(X)) = [2] X + [0]
>= [2] X + [0]
= g(activate(X))
f(X) = [1] X + [0]
>= [1] X + [0]
= n__f(X)
f(f(a())) = [1]
>= [1]
= c(n__f(n__g(n__f(n__a()))))
g(X) = [1] X + [0]
>= [1] X + [0]
= n__g(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:
activate(n__f(X)) -> f(activate(X))
Weak DP Rules:
a#() -> c_1()
activate#(X) -> c_2(X)
activate#(n__a()) -> c_3(a#())
activate#(n__f(X)) -> c_4(f#(activate(X)))
activate#(n__g(X)) -> c_5(g#(activate(X)))
f#(X) -> c_6(X)
f#(f(a())) -> c_7()
g#(X) -> c_8(X)
Weak TRS Rules:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
Signature:
{a/0,activate/1,f/1,g/1,a#/0,activate#/1,f#/1,g#/1} / {c/1,n__a/0,n__f/1,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1}
Obligation:
Full
basic terms: {a#,activate#,f#,g#}/{c,n__a,n__f,n__g}
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(f) = {1},
uargs(g) = {1},
uargs(n__f) = {1},
uargs(n__g) = {1},
uargs(f#) = {1},
uargs(g#) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [1]
p(activate) = [4] x1 + [3]
p(c) = [0]
p(f) = [1] x1 + [3]
p(g) = [1] x1 + [0]
p(n__a) = [0]
p(n__f) = [1] x1 + [1]
p(n__g) = [1] x1 + [0]
p(a#) = [8]
p(activate#) = [9] x1 + [15]
p(f#) = [1] x1 + [4]
p(g#) = [1] x1 + [1]
p(c_1) = [8]
p(c_2) = [1] x1 + [1]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [4]
p(c_5) = [1] x1 + [1]
p(c_6) = [1] x1 + [0]
p(c_7) = [1]
p(c_8) = [1] x1 + [0]
Following rules are strictly oriented:
activate(n__f(X)) = [4] X + [7]
> [4] X + [6]
= f(activate(X))
Following rules are (at-least) weakly oriented:
a#() = [8]
>= [8]
= c_1()
activate#(X) = [9] X + [15]
>= [1] X + [1]
= c_2(X)
activate#(n__a()) = [15]
>= [8]
= c_3(a#())
activate#(n__f(X)) = [9] X + [24]
>= [4] X + [11]
= c_4(f#(activate(X)))
activate#(n__g(X)) = [9] X + [15]
>= [4] X + [5]
= c_5(g#(activate(X)))
f#(X) = [1] X + [4]
>= [1] X + [0]
= c_6(X)
f#(f(a())) = [8]
>= [1]
= c_7()
g#(X) = [1] X + [1]
>= [1] X + [0]
= c_8(X)
a() = [1]
>= [0]
= n__a()
activate(X) = [4] X + [3]
>= [1] X + [0]
= X
activate(n__a()) = [3]
>= [1]
= a()
activate(n__g(X)) = [4] X + [3]
>= [4] X + [3]
= g(activate(X))
f(X) = [1] X + [3]
>= [1] X + [1]
= n__f(X)
f(f(a())) = [7]
>= [0]
= c(n__f(n__g(n__f(n__a()))))
g(X) = [1] X + [0]
>= [1] X + [0]
= n__g(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:
a#() -> c_1()
activate#(X) -> c_2(X)
activate#(n__a()) -> c_3(a#())
activate#(n__f(X)) -> c_4(f#(activate(X)))
activate#(n__g(X)) -> c_5(g#(activate(X)))
f#(X) -> c_6(X)
f#(f(a())) -> c_7()
g#(X) -> c_8(X)
Weak TRS Rules:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
Signature:
{a/0,activate/1,f/1,g/1,a#/0,activate#/1,f#/1,g#/1} / {c/1,n__a/0,n__f/1,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/1}
Obligation:
Full
basic terms: {a#,activate#,f#,g#}/{c,n__a,n__f,n__g}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).