*** 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))
f(X) -> n__f(X)
f(f(a())) -> f(g(n__f(n__a())))
Weak DP Rules:
Weak TRS Rules:
Signature:
{a/0,activate/1,f/1} / {g/1,n__a/0,n__f/1}
Obligation:
Full
basic terms: {a,activate,f}/{g,n__a,n__f}
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)))
f#(X) -> c_5(X)
f#(f(a())) -> c_6(f#(g(n__f(n__a()))))
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)))
f#(X) -> c_5(X)
f#(f(a())) -> c_6(f#(g(n__f(n__a()))))
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())) -> f(g(n__f(n__a())))
Weak DP Rules:
Weak TRS Rules:
Signature:
{a/0,activate/1,f/1,a#/0,activate#/1,f#/1} / {g/1,n__a/0,n__f/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1}
Obligation:
Full
basic terms: {a#,activate#,f#}/{g,n__a,n__f}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{1}
by application of
Pre({1}) = {2,3,5}.
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: f#(X) -> c_5(X)
6: f#(f(a())) ->
c_6(f#(g(n__f(n__a()))))
*** 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)))
f#(X) -> c_5(X)
f#(f(a())) -> c_6(f#(g(n__f(n__a()))))
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())) -> f(g(n__f(n__a())))
Weak DP Rules:
a#() -> c_1()
Weak TRS Rules:
Signature:
{a/0,activate/1,f/1,a#/0,activate#/1,f#/1} / {g/1,n__a/0,n__f/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1}
Obligation:
Full
basic terms: {a#,activate#,f#}/{g,n__a,n__f}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{2}
by application of
Pre({2}) = {1,4}.
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: f#(X) -> c_5(X)
5: f#(f(a())) ->
c_6(f#(g(n__f(n__a()))))
6: a#() -> c_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)))
f#(X) -> c_5(X)
f#(f(a())) -> c_6(f#(g(n__f(n__a()))))
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())) -> f(g(n__f(n__a())))
Weak DP Rules:
a#() -> c_1()
activate#(n__a()) -> c_3(a#())
Weak TRS Rules:
Signature:
{a/0,activate/1,f/1,a#/0,activate#/1,f#/1} / {g/1,n__a/0,n__f/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1}
Obligation:
Full
basic terms: {a#,activate#,f#}/{g,n__a,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(f) = {1},
uargs(n__f) = {1},
uargs(f#) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [0]
p(activate) = [2] x1 + [9]
p(f) = [1] x1 + [0]
p(g) = [1] x1 + [0]
p(n__a) = [2]
p(n__f) = [1] x1 + [0]
p(a#) = [0]
p(activate#) = [8] x1 + [8]
p(f#) = [1] x1 + [0]
p(c_1) = [0]
p(c_2) = [8] x1 + [2]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [1] x1 + [0]
Following rules are strictly oriented:
activate#(X) = [8] X + [8]
> [8] X + [2]
= c_2(X)
activate(X) = [2] X + [9]
> [1] X + [0]
= X
activate(n__a()) = [13]
> [0]
= a()
Following rules are (at-least) weakly oriented:
a#() = [0]
>= [0]
= c_1()
activate#(n__a()) = [24]
>= [0]
= c_3(a#())
activate#(n__f(X)) = [8] X + [8]
>= [2] X + [9]
= c_4(f#(activate(X)))
f#(X) = [1] X + [0]
>= [1] X + [0]
= c_5(X)
f#(f(a())) = [0]
>= [2]
= c_6(f#(g(n__f(n__a()))))
a() = [0]
>= [2]
= n__a()
activate(n__f(X)) = [2] X + [9]
>= [2] X + [9]
= f(activate(X))
f(X) = [1] X + [0]
>= [1] X + [0]
= n__f(X)
f(f(a())) = [0]
>= [2]
= f(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 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
activate#(n__f(X)) -> c_4(f#(activate(X)))
f#(X) -> c_5(X)
f#(f(a())) -> c_6(f#(g(n__f(n__a()))))
Strict TRS Rules:
a() -> n__a()
activate(n__f(X)) -> f(activate(X))
f(X) -> n__f(X)
f(f(a())) -> f(g(n__f(n__a())))
Weak DP Rules:
a#() -> c_1()
activate#(X) -> c_2(X)
activate#(n__a()) -> c_3(a#())
Weak TRS Rules:
activate(X) -> X
activate(n__a()) -> a()
Signature:
{a/0,activate/1,f/1,a#/0,activate#/1,f#/1} / {g/1,n__a/0,n__f/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1}
Obligation:
Full
basic terms: {a#,activate#,f#}/{g,n__a,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(f) = {1},
uargs(n__f) = {1},
uargs(f#) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [6]
p(activate) = [3] x1 + [0]
p(f) = [1] x1 + [3]
p(g) = [0]
p(n__a) = [2]
p(n__f) = [1] x1 + [6]
p(a#) = [6]
p(activate#) = [3] x1 + [0]
p(f#) = [1] x1 + [2]
p(c_1) = [6]
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]
Following rules are strictly oriented:
activate#(n__f(X)) = [3] X + [18]
> [3] X + [2]
= c_4(f#(activate(X)))
f#(X) = [1] X + [2]
> [1] X + [0]
= c_5(X)
f#(f(a())) = [11]
> [2]
= c_6(f#(g(n__f(n__a()))))
a() = [6]
> [2]
= n__a()
activate(n__f(X)) = [3] X + [18]
> [3] X + [3]
= f(activate(X))
f(f(a())) = [12]
> [3]
= f(g(n__f(n__a())))
Following rules are (at-least) weakly oriented:
a#() = [6]
>= [6]
= c_1()
activate#(X) = [3] X + [0]
>= [3] X + [0]
= c_2(X)
activate#(n__a()) = [6]
>= [6]
= c_3(a#())
activate(X) = [3] X + [0]
>= [1] X + [0]
= X
activate(n__a()) = [6]
>= [6]
= a()
f(X) = [1] X + [3]
>= [1] X + [6]
= 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:
Strict TRS Rules:
f(X) -> n__f(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)))
f#(X) -> c_5(X)
f#(f(a())) -> c_6(f#(g(n__f(n__a()))))
Weak TRS Rules:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
f(f(a())) -> f(g(n__f(n__a())))
Signature:
{a/0,activate/1,f/1,a#/0,activate#/1,f#/1} / {g/1,n__a/0,n__f/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1}
Obligation:
Full
basic terms: {a#,activate#,f#}/{g,n__a,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(f) = {1},
uargs(n__f) = {1},
uargs(f#) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(a) = [0]
p(activate) = [3] x1 + [0]
p(f) = [1] x1 + [9]
p(g) = [1] x1 + [6]
p(n__a) = [0]
p(n__f) = [1] x1 + [3]
p(a#) = [0]
p(activate#) = [3] x1 + [0]
p(f#) = [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]
Following rules are strictly oriented:
f(X) = [1] X + [9]
> [1] X + [3]
= n__f(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 + [9]
>= [3] X + [0]
= c_4(f#(activate(X)))
f#(X) = [1] X + [0]
>= [1] X + [0]
= c_5(X)
f#(f(a())) = [9]
>= [9]
= c_6(f#(g(n__f(n__a()))))
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 + [9]
>= [3] X + [9]
= f(activate(X))
f(f(a())) = [18]
>= [18]
= f(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(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)))
f#(X) -> c_5(X)
f#(f(a())) -> c_6(f#(g(n__f(n__a()))))
Weak 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())) -> f(g(n__f(n__a())))
Signature:
{a/0,activate/1,f/1,a#/0,activate#/1,f#/1} / {g/1,n__a/0,n__f/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1}
Obligation:
Full
basic terms: {a#,activate#,f#}/{g,n__a,n__f}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).