We consider the following Problem:
Strict Trs:
{ g(X) -> h(activate(X))
, c() -> d()
, h(n__d()) -> g(n__c())
, d() -> n__d()
, c() -> n__c()
, activate(n__d()) -> d()
, activate(n__c()) -> c()
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ g(X) -> h(activate(X))
, c() -> d()
, h(n__d()) -> g(n__c())
, d() -> n__d()
, c() -> n__c()
, activate(n__d()) -> d()
, activate(n__c()) -> c()
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ c() -> d()
, c() -> n__c()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(g) = {}, Uargs(h) = {1}, Uargs(activate) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
g(x1) = [1 0] x1 + [1]
[1 0] [1]
h(x1) = [1 0] x1 + [1]
[1 0] [1]
activate(x1) = [1 0] x1 + [0]
[0 0] [1]
c() = [2]
[0]
d() = [0]
[0]
n__d() = [0]
[0]
n__c() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ g(X) -> h(activate(X))
, h(n__d()) -> g(n__c())
, d() -> n__d()
, activate(n__d()) -> d()
, activate(n__c()) -> c()
, activate(X) -> X}
Weak Trs:
{ c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {d() -> n__d()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(g) = {}, Uargs(h) = {1}, Uargs(activate) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
g(x1) = [1 0] x1 + [1]
[1 0] [1]
h(x1) = [1 0] x1 + [1]
[1 0] [1]
activate(x1) = [1 0] x1 + [0]
[0 0] [1]
c() = [2]
[0]
d() = [2]
[0]
n__d() = [0]
[0]
n__c() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ g(X) -> h(activate(X))
, h(n__d()) -> g(n__c())
, activate(n__d()) -> d()
, activate(n__c()) -> c()
, activate(X) -> X}
Weak Trs:
{ d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {g(X) -> h(activate(X))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(g) = {}, Uargs(h) = {1}, Uargs(activate) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
g(x1) = [1 0] x1 + [3]
[1 0] [1]
h(x1) = [1 0] x1 + [1]
[1 0] [1]
activate(x1) = [1 0] x1 + [0]
[0 0] [1]
c() = [0]
[0]
d() = [0]
[0]
n__d() = [0]
[0]
n__c() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ h(n__d()) -> g(n__c())
, activate(n__d()) -> d()
, activate(n__c()) -> c()
, activate(X) -> X}
Weak Trs:
{ g(X) -> h(activate(X))
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {h(n__d()) -> g(n__c())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(g) = {}, Uargs(h) = {1}, Uargs(activate) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
g(x1) = [1 0] x1 + [0]
[0 0] [1]
h(x1) = [1 0] x1 + [0]
[0 0] [1]
activate(x1) = [1 0] x1 + [0]
[0 0] [1]
c() = [1]
[0]
d() = [1]
[0]
n__d() = [1]
[0]
n__c() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ activate(n__d()) -> d()
, activate(n__c()) -> c()
, activate(X) -> X}
Weak Trs:
{ h(n__d()) -> g(n__c())
, g(X) -> h(activate(X))
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ activate(n__d()) -> d()
, activate(X) -> X}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(g) = {}, Uargs(h) = {1}, Uargs(activate) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
g(x1) = [1 2] x1 + [1]
[0 0] [1]
h(x1) = [1 2] x1 + [0]
[0 0] [1]
activate(x1) = [1 0] x1 + [1]
[0 1] [0]
c() = [1]
[2]
d() = [1]
[2]
n__d() = [1]
[2]
n__c() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, h(n__d()) -> g(n__c())
, g(X) -> h(activate(X))
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, h(n__d()) -> g(n__c())
, g(X) -> h(activate(X))
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We have computed the following dependency pairs
Strict DPs: {activate^#(n__c()) -> c^#()}
Weak DPs:
{ activate^#(n__d()) -> d^#()
, activate^#(X) -> c_3()
, h^#(n__d()) -> g^#(n__c())
, g^#(X) -> h^#(activate(X))
, d^#() -> c_6()
, c^#() -> d^#()
, c^#() -> c_8()}
We consider the following Problem:
Strict DPs: {activate^#(n__c()) -> c^#()}
Strict Trs: {activate(n__c()) -> c()}
Weak DPs:
{ activate^#(n__d()) -> d^#()
, activate^#(X) -> c_3()
, h^#(n__d()) -> g^#(n__c())
, g^#(X) -> h^#(activate(X))
, d^#() -> c_6()
, c^#() -> d^#()
, c^#() -> c_8()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, h(n__d()) -> g(n__c())
, g(X) -> h(activate(X))
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We replace strict/weak-rules by the corresponding usable rules:
Strict Usable Rules: {activate(n__c()) -> c()}
Weak Usable Rules:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
We consider the following Problem:
Strict DPs: {activate^#(n__c()) -> c^#()}
Strict Trs: {activate(n__c()) -> c()}
Weak DPs:
{ activate^#(n__d()) -> d^#()
, activate^#(X) -> c_3()
, h^#(n__d()) -> g^#(n__c())
, g^#(X) -> h^#(activate(X))
, d^#() -> c_6()
, c^#() -> d^#()
, c^#() -> c_8()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict DPs: {activate^#(n__c()) -> c^#()}
Strict Trs: {activate(n__c()) -> c()}
Weak DPs:
{ activate^#(n__d()) -> d^#()
, activate^#(X) -> c_3()
, h^#(n__d()) -> g^#(n__c())
, g^#(X) -> h^#(activate(X))
, d^#() -> c_6()
, c^#() -> d^#()
, c^#() -> c_8()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We use following congruence DG for path analysis
->4:{1} [ YES(?,O(n^1)) ]
|
|->6:{7} [ subsumed ]
| |
| `->7:{6} [ YES(O(1),O(1)) ]
|
`->5:{8} [ YES(O(1),O(1)) ]
->3:{2} [ subsumed ]
|
`->7:{6} [ YES(O(1),O(1)) ]
->2:{3} [ YES(O(1),O(1)) ]
->1:{4,5} [ YES(O(1),O(1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{1: activate^#(n__c()) -> c^#()}
WeakDPs DPs:
{ 2: activate^#(n__d()) -> d^#()
, 3: activate^#(X) -> c_3()
, 4: h^#(n__d()) -> g^#(n__c())
, 5: g^#(X) -> h^#(activate(X))
, 6: d^#() -> c_6()
, 7: c^#() -> d^#()
, 8: c^#() -> c_8()}
* Path 4:{1}: YES(?,O(n^1))
-------------------------
We consider the following Problem:
Strict DPs: {activate^#(n__c()) -> c^#()}
Strict Trs: {activate(n__c()) -> c()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict DPs: {activate^#(n__c()) -> c^#()}
Strict Trs: {activate(n__c()) -> c()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict DPs: {activate^#(n__c()) -> c^#()}
Strict Trs: {activate(n__c()) -> c()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
No rule is usable.
We consider the following Problem:
Strict DPs: {activate^#(n__c()) -> c^#()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ n__c_0() -> 2
, activate^#_0(2) -> 1
, c^#_0() -> 1
, c^#_1() -> 1}
* Path 4:{1}->6:{7}: subsumed
---------------------------
This path is subsumed by the proof of paths 4:{1}->6:{7}->7:{6}.
* Path 4:{1}->6:{7}->7:{6}: YES(O(1),O(1))
----------------------------------------
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak DPs:
{ activate^#(n__c()) -> c^#()
, c^#() -> d^#()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak DPs:
{ activate^#(n__c()) -> c^#()
, c^#() -> d^#()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak DPs:
{ activate^#(n__c()) -> c^#()
, c^#() -> d^#()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
Weak DPs:
{ activate^#(n__c()) -> c^#()
, c^#() -> d^#()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 4:{1}->5:{8}: YES(O(1),O(1))
---------------------------------
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak DPs: {activate^#(n__c()) -> c^#()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak DPs: {activate^#(n__c()) -> c^#()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak DPs: {activate^#(n__c()) -> c^#()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
Weak DPs: {activate^#(n__c()) -> c^#()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 3:{2}: subsumed
--------------------
This path is subsumed by the proof of paths 3:{2}->7:{6}.
* Path 3:{2}->7:{6}: YES(O(1),O(1))
---------------------------------
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak DPs: {activate^#(n__d()) -> d^#()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak DPs: {activate^#(n__d()) -> d^#()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak DPs: {activate^#(n__d()) -> d^#()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
Weak DPs: {activate^#(n__d()) -> d^#()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 2:{3}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 1:{4,5}: YES(O(1),O(1))
----------------------------
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {activate(n__c()) -> c()}
Weak Trs:
{ activate(n__d()) -> d()
, activate(X) -> X
, d() -> n__d()
, c() -> d()
, c() -> n__c()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))