Tool CaT
| Execution Time | Unknown |
|---|
| Answer | MAYBE |
|---|
| Input | Der95 08 |
|---|
stdout:
MAYBE
Problem:
D(t()) -> 1()
D(constant()) -> 0()
D(+(x,y)) -> +(D(x),D(y))
D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
D(-(x,y)) -> -(D(x),D(y))
Proof:
OpenTool IRC1
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | Der95 08 |
|---|
stdout:
YES(?,O(n^1))
Tool IRC2
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | Der95 08 |
|---|
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Proof Output:
'wdg' proved the best result:
Details:
--------
'wdg' succeeded with the following output:
'wdg'
-----
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Proof Output:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: D^#(t()) -> c_0()
, 2: D^#(constant()) -> c_1()
, 3: D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, 4: D^#(*(x, y)) -> c_3(D^#(x), D^#(y))
, 5: D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{3,5,4} [ YES(?,O(n^1)) ]
|
|->{1} [ YES(?,O(n^1)) ]
|
`->{2} [ YES(?,O(n^1)) ]
Sub-problems:
-------------
* Path {3,5,4}: YES(?,O(n^1))
---------------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {},
Uargs(D^#) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [0]
*(x1, x2) = [1] x1 + [1] x2 + [0]
-(x1, x2) = [1] x1 + [1] x2 + [0]
D^#(x1) = [3] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2) = [1] x1 + [1] x2 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules:
{ D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
Weak Rules: {}
Proof Output:
The following argument positions are usable:
Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {}, Uargs(D^#) = {},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
+(x1, x2) = [1] x1 + [1] x2 + [4]
*(x1, x2) = [1] x1 + [1] x2 + [1]
-(x1, x2) = [1] x1 + [1] x2 + [4]
D^#(x1) = [2] x1 + [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [7]
c_3(x1, x2) = [1] x1 + [1] x2 + [1]
c_4(x1, x2) = [1] x1 + [1] x2 + [7]
* Path {3,5,4}->{1}: YES(?,O(n^1))
--------------------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {},
Uargs(D^#) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [0] x1 + [0] x2 + [0]
*(x1, x2) = [0] x1 + [0] x2 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
D^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2) = [1] x1 + [1] x2 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {D^#(t()) -> c_0()}
Weak Rules:
{ D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
Proof Output:
The following argument positions are usable:
Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {}, Uargs(D^#) = {},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
t() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [2]
*(x1, x2) = [1] x1 + [1] x2 + [1]
-(x1, x2) = [1] x1 + [1] x2 + [4]
D^#(x1) = [2] x1 + [1]
c_0() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [1]
c_3(x1, x2) = [1] x1 + [1] x2 + [1]
c_4(x1, x2) = [1] x1 + [1] x2 + [5]
* Path {3,5,4}->{2}: YES(?,O(n^1))
--------------------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {},
Uargs(D^#) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [0] x1 + [0] x2 + [0]
*(x1, x2) = [0] x1 + [0] x2 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
D^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2) = [1] x1 + [1] x2 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {D^#(constant()) -> c_1()}
Weak Rules:
{ D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(D^#(x), D^#(y))}
Proof Output:
The following argument positions are usable:
Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {}, Uargs(D^#) = {},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
constant() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [2]
*(x1, x2) = [1] x1 + [1] x2 + [1]
-(x1, x2) = [1] x1 + [1] x2 + [4]
D^#(x1) = [2] x1 + [1]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [1]
c_3(x1, x2) = [1] x1 + [1] x2 + [1]
c_4(x1, x2) = [1] x1 + [1] x2 + [5]Tool RC1
| Execution Time | Unknown |
|---|
| Answer | MAYBE |
|---|
| Input | Der95 08 |
|---|
stdout:
MAYBE
Tool RC2
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | Der95 08 |
|---|
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Proof Output:
'wdg' proved the best result:
Details:
--------
'wdg' succeeded with the following output:
'wdg'
-----
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Proof Output:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: D^#(t()) -> c_0()
, 2: D^#(constant()) -> c_1()
, 3: D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, 4: D^#(*(x, y)) -> c_3(y, D^#(x), x, D^#(y))
, 5: D^#(-(x, y)) -> c_4(D^#(x), D^#(y))}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{3,5,4} [ YES(?,O(n^1)) ]
|
|->{1} [ YES(?,O(n^1)) ]
|
`->{2} [ YES(?,O(n^1)) ]
Sub-problems:
-------------
* Path {3,5,4}: YES(?,O(n^1))
---------------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {},
Uargs(D^#) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {2, 4},
Uargs(c_4) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [1] x1 + [1] x2 + [0]
*(x1, x2) = [1] x1 + [1] x2 + [0]
-(x1, x2) = [1] x1 + [1] x2 + [0]
D^#(x1) = [2] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2, x3, x4) = [0] x1 + [1] x2 + [0] x3 + [1] x4 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: DP runtime-complexity with respect to
Strict Rules:
{ D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(y, D^#(x), x, D^#(y))}
Weak Rules: {}
Proof Output:
The following argument positions are usable:
Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {}, Uargs(D^#) = {},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {2, 4}, Uargs(c_4) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
+(x1, x2) = [1] x1 + [1] x2 + [2]
*(x1, x2) = [1] x1 + [1] x2 + [3]
-(x1, x2) = [1] x1 + [1] x2 + [2]
D^#(x1) = [3] x1 + [2]
c_2(x1, x2) = [1] x1 + [1] x2 + [3]
c_3(x1, x2, x3, x4) = [0] x1 + [1] x2 + [0] x3 + [1] x4 + [3]
c_4(x1, x2) = [1] x1 + [1] x2 + [3]
* Path {3,5,4}->{1}: YES(?,O(n^1))
--------------------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {},
Uargs(D^#) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {2, 4},
Uargs(c_4) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [0] x1 + [0] x2 + [0]
*(x1, x2) = [0] x1 + [0] x2 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
D^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2, x3, x4) = [0] x1 + [1] x2 + [0] x3 + [1] x4 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: DP runtime-complexity with respect to
Strict Rules: {D^#(t()) -> c_0()}
Weak Rules:
{ D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(y, D^#(x), x, D^#(y))}
Proof Output:
The following argument positions are usable:
Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {}, Uargs(D^#) = {},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {2, 4}, Uargs(c_4) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
t() = [2]
+(x1, x2) = [1] x1 + [1] x2 + [0]
*(x1, x2) = [1] x1 + [1] x2 + [2]
-(x1, x2) = [1] x1 + [1] x2 + [2]
D^#(x1) = [2] x1 + [0]
c_0() = [1]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2, x3, x4) = [0] x1 + [1] x2 + [0] x3 + [1] x4 + [3]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
* Path {3,5,4}->{2}: YES(?,O(n^1))
--------------------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {},
Uargs(D^#) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {2, 4},
Uargs(c_4) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
D(x1) = [0] x1 + [0]
t() = [0]
1() = [0]
constant() = [0]
0() = [0]
+(x1, x2) = [0] x1 + [0] x2 + [0]
*(x1, x2) = [0] x1 + [0] x2 + [0]
-(x1, x2) = [0] x1 + [0] x2 + [0]
D^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2, x3, x4) = [0] x1 + [1] x2 + [0] x3 + [1] x4 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: DP runtime-complexity with respect to
Strict Rules: {D^#(constant()) -> c_1()}
Weak Rules:
{ D^#(+(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_3(y, D^#(x), x, D^#(y))}
Proof Output:
The following argument positions are usable:
Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {}, Uargs(D^#) = {},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {2, 4}, Uargs(c_4) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
constant() = [2]
+(x1, x2) = [1] x1 + [1] x2 + [0]
*(x1, x2) = [1] x1 + [1] x2 + [2]
-(x1, x2) = [1] x1 + [1] x2 + [2]
D^#(x1) = [2] x1 + [0]
c_1() = [1]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2, x3, x4) = [0] x1 + [1] x2 + [0] x3 + [1] x4 + [3]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]Tool pair1rc
| Execution Time | Unknown |
|---|
| Answer | MAYBE |
|---|
| Input | Der95 08 |
|---|
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
The processor is not applicable, reason is:
Input problem is not restricted to innermost rewriting
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
1) None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'dp' failed due to the following reason:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
We consider the following Problem:
Strict DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'Fastest':
-------------------------
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'pathanalysis' failed due to the following reason:
We use following congruence DG for path analysis
->{3,5,4} [ MAYBE ]
|
|->{1} [ ? ]
|
`->{2} [ ? ]
Here rules are as follows:
{ 1: D^#(t()) -> c_1()
, 2: D^#(constant()) -> c_2()
, 3: D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, 4: D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, 5: D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
* Path {3,5,4}: MAYBE
-------------------
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of the
input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ D(t()) -> 1()
, D(constant()) -> 0()}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0] x1 + [2]
[0 0] [1]
t() = [0]
[0]
1() = [1]
[1]
constant() = [0]
[0]
0() = [1]
[1]
+(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
*(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
-(x1, x2) = [1 2] x1 + [1 2] x2 + [0]
[0 0] [0 0] [0]
D^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_1() = [0]
[0]
c_2() = [0]
[0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
c_4(x1, x2, x3, x4) = [0 0] x1 + [1 0] x2 + [0 0] x3 + [1 0] x4 + [3]
[3 2] [0 1] [3 3] [0 1] [3]
c_5(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of the
input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs: {D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [1]
D^#(x1) = [0 0 1] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [3]
[0 0 1] [0 0 1] [3]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [3]
[3 0 0] [0 1 0] [0 0 2] [0 1 0] [2]
[3 0 3] [0 0 1] [0 0 2] [0 0 1] [3]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs: {D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of the
input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs: {D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs: {D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 0] x1 + [0]
[0 0 1] [0]
[0 0 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 3] [1]
[0 0 1] [0 0 0] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 3] [0 1 0] [0]
[0 0 0] [0 0 1] [3]
D^#(x1) = [0 1 3] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 1 0] [0 1 0] [2]
[0 0 1] [0 0 1] [3]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [0]
[0 0 0] [0 1 0] [0 0 0] [0 1 0] [0]
[0 0 0] [0 0 1] [0 0 0] [0 0 1] [0]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of
the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {D(-(x, y)) -> -(D(x), D(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {},
Uargs(c_3) = {1, 2}, Uargs(c_4) = {2, 4},
Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 2] x1 + [0]
[0 0 1] [0]
[0 0 1] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [2]
D^#(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 1 0] [0 1 0] [3]
[0 0 1] [0 0 1] [3]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [0]
[0 0 0] [0 1 0] [0 0 0] [0 1 0] [0]
[0 0 0] [0 0 1] [0 0 0] [0 0 1] [0]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict
component of the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2},
Uargs(*) = {2}, Uargs(-) = {1, 2},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 0] x1 + [0]
[0 0 1] [0]
[0 1 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 1 0] [0]
[0 0 1] [0 0 1] [2]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 1] [0]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [2]
[0 0 1] [0 0 1] [2]
D^#(x1) = [0 0 2] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [0]
[0 0 0] [0 1 0] [0 0 0] [0 1 0] [0]
[0 0 0] [0 0 1] [0 0 0] [0 0 1] [0]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict
component of the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {D(+(x, y)) -> +(D(x), D(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2},
Uargs(*) = {2}, Uargs(-) = {1, 2},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 1] x1 + [0]
[1 0 1] [0]
[0 1 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [1]
[0 0 1] [0 0 1] [1]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [1]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 1 0] [0 1 0] [2]
[0 0 1] [0 0 1] [1]
D^#(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 1 1] [1]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [1]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [0]
[0 0 0] [0 1 0] [0 0 0] [0 1 0] [0]
[0 0 0] [0 0 1] [0 0 0] [0 0 1] [0]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the
strict component of the input problem is not
empty
We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
Strict Trs:
{D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict Trs:
{D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
Strict Trs:
{D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle does not apply
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
* Path {3,5,4}->{1}: ?
--------------------
CANNOT find proof of path {3,5,4}->{1}. Propably computation has been aborted since some other path cannot be solved.
* Path {3,5,4}->{2}: ?
--------------------
CANNOT find proof of path {3,5,4}->{2}. Propably computation has been aborted since some other path cannot be solved.
2) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
Arrrr..Tool pair2rc
| Execution Time | Unknown |
|---|
| Answer | MAYBE |
|---|
| Input | Der95 08 |
|---|
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
The processor is not applicable, reason is:
Input problem is not restricted to innermost rewriting
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
1) None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'dp' failed due to the following reason:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
We consider the following Problem:
Strict DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'Fastest':
-------------------------
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'pathanalysis' failed due to the following reason:
We use following congruence DG for path analysis
->{3,5,4} [ MAYBE ]
|
|->{1} [ ? ]
|
`->{2} [ ? ]
Here rules are as follows:
{ 1: D^#(t()) -> c_1()
, 2: D^#(constant()) -> c_2()
, 3: D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, 4: D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, 5: D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
* Path {3,5,4}: MAYBE
-------------------
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of the
input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ D(t()) -> 1()
, D(constant()) -> 0()}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0] x1 + [2]
[0 0] [1]
t() = [0]
[0]
1() = [1]
[1]
constant() = [0]
[0]
0() = [1]
[1]
+(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
*(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
-(x1, x2) = [1 2] x1 + [1 2] x2 + [0]
[0 0] [0 0] [0]
D^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_1() = [0]
[0]
c_2() = [0]
[0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
c_4(x1, x2, x3, x4) = [0 0] x1 + [1 0] x2 + [0 0] x3 + [1 0] x4 + [3]
[3 2] [0 1] [3 3] [0 1] [3]
c_5(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of the
input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs: {D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [1]
D^#(x1) = [0 0 1] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [3]
[0 0 1] [0 0 1] [3]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [3]
[3 0 0] [0 1 0] [0 0 2] [0 1 0] [2]
[3 0 3] [0 0 1] [0 0 2] [0 0 1] [3]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs: {D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of the
input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs: {D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs: {D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 0] x1 + [0]
[0 0 1] [0]
[0 0 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 3] [1]
[0 0 1] [0 0 0] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 3] [0 1 0] [0]
[0 0 0] [0 0 1] [3]
D^#(x1) = [0 1 3] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 1 0] [0 1 0] [2]
[0 0 1] [0 0 1] [3]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [0]
[0 0 0] [0 1 0] [0 0 0] [0 1 0] [0]
[0 0 0] [0 0 1] [0 0 0] [0 0 1] [0]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of
the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {D(-(x, y)) -> -(D(x), D(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {},
Uargs(c_3) = {1, 2}, Uargs(c_4) = {2, 4},
Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 2] x1 + [0]
[0 0 1] [0]
[0 0 1] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [2]
D^#(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 1 0] [0 1 0] [3]
[0 0 1] [0 0 1] [3]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [0]
[0 0 0] [0 1 0] [0 0 0] [0 1 0] [0]
[0 0 0] [0 0 1] [0 0 0] [0 0 1] [0]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict
component of the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2},
Uargs(*) = {2}, Uargs(-) = {1, 2},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 0] x1 + [0]
[0 0 1] [0]
[0 1 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 1 0] [0]
[0 0 1] [0 0 1] [2]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 1] [0]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [2]
[0 0 1] [0 0 1] [2]
D^#(x1) = [0 0 2] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [0]
[0 0 0] [0 1 0] [0 0 0] [0 1 0] [0]
[0 0 0] [0 0 1] [0 0 0] [0 0 1] [0]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict
component of the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {D(+(x, y)) -> +(D(x), D(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2},
Uargs(*) = {2}, Uargs(-) = {1, 2},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 1] x1 + [0]
[1 0 1] [0]
[0 1 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [1]
[0 0 1] [0 0 1] [1]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [1]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 1 0] [0 1 0] [2]
[0 0 1] [0 0 1] [1]
D^#(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 1 1] [1]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [1]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [0]
[0 0 0] [0 1 0] [0 0 0] [0 1 0] [0]
[0 0 0] [0 0 1] [0 0 0] [0 0 1] [0]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the
strict component of the input problem is not
empty
We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
Strict Trs:
{D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict Trs:
{D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
Strict Trs:
{D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle does not apply
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'compose (statically using 'split first congruence from CWD', multiplication)' failed due to the following reason:
Compose is inapplicable since some weak rule is size increasing
No subproblems were generated.
* Path {3,5,4}->{1}: ?
--------------------
CANNOT find proof of path {3,5,4}->{1}. Propably computation has been aborted since some other path cannot be solved.
* Path {3,5,4}->{2}: ?
--------------------
CANNOT find proof of path {3,5,4}->{2}. Propably computation has been aborted since some other path cannot be solved.
2) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
Arrrr..Tool pair3irc
| Execution Time | Unknown |
|---|
| Answer | MAYBE |
|---|
| Input | Der95 08 |
|---|
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
The input problem contains no overlaps that give rise to inapplicable rules.
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: innermost
1) None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'dp' failed due to the following reason:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
We consider the following Problem:
Strict DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Application of 'Fastest':
-------------------------
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'compose (statically using 'split all congruence from CWD except leafs', multiplication)' failed due to the following reason:
Compose is inapplicable since some strict rule is size increasing
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: innermost
1) The processor is inapplicable since the strict component of the
input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: innermost
1) The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0] x1 + [0]
[0 0] [0]
t() = [0]
[0]
1() = [3]
[0]
constant() = [0]
[0]
0() = [3]
[0]
+(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
*(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
-(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
D^#(x1) = [0 0] x1 + [3]
[0 0] [0]
c_1() = [0]
[0]
c_2() = [0]
[0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 1] [0 1] [3]
c_4(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 1] [0 1] [2]
c_5(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 1] [0 1] [2]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of the
input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
StartTerms: basic terms
Strategy: innermost
1) The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ D(t()) -> 1()
, D(constant()) -> 0()}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0] x1 + [2]
[0 0] [0]
t() = [0]
[0]
1() = [1]
[0]
constant() = [0]
[0]
0() = [1]
[0]
+(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
*(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
-(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
D^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_1() = [0]
[0]
c_2() = [0]
[0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
c_4(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
c_5(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [2]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of the
input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {D(-(x, y)) -> -(D(x), D(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 2 0] x1 + [0]
[0 1 1] [0]
[0 0 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 0] [0 0 0] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 0] [0 0 0] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [1]
[0 0 1] [0 0 1] [0]
D^#(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [3]
[0 0 1] [0 0 1] [3]
c_4(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 1 0] [0 1 0] [3]
[0 0 1] [0 0 1] [3]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [2]
[0 0 1] [0 0 1] [3]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of
the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {},
Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2},
Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 1 2] [0]
[0 0 1] [0 0 1] [2]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 0 3] [0 0 0] [0]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [0]
D^#(x1) = [0 0 2] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_4(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [3]
[0 0 1] [0 0 1] [2]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 1 0] [0 1 0] [3]
[0 0 1] [0 0 1] [2]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component
of the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{ D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2},
Uargs(*) = {2}, Uargs(-) = {1, 2},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 0] x1 + [0]
[0 1 1] [0]
[0 2 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 0 2] [0]
[0 0 1] [0 0 1] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [2]
[0 0 1] [0 0 1] [1]
D^#(x1) = [0 0 1] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_4(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [3]
[0 0 1] [0 0 1] [3]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs: {D^#(*(x, y)) -> c_4(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict
component of the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs: {D^#(*(x, y)) -> c_4(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{D^#(*(x, y)) -> c_4(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {D(+(x, y)) -> +(D(x), D(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2},
Uargs(*) = {2}, Uargs(-) = {1, 2},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 2 0] x1 + [0]
[3 0 1] [0]
[0 0 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 2] [0 1 3] [2]
[0 0 1] [0 0 1] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 0] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
D^#(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_4(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [3]
[0 0 1] [0 0 1] [3]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{D^#(*(x, y)) -> c_4(D^#(x), D^#(y))}
Strict Trs:
{D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict
component of the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{D^#(*(x, y)) -> c_4(D^#(x), D^#(y))}
Strict Trs:
{D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{D^#(*(x, y)) -> c_4(D^#(x), D^#(y))}
Strict Trs:
{D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{D^#(*(x, y)) -> c_4(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2},
Uargs(*) = {2}, Uargs(-) = {1, 2},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2},
Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 2] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 0] [0 0 0] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [3]
[0 0 0] [0 0 0] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 0] [0 0 0] [2]
D^#(x1) = [0 3 0] x1 + [0]
[0 0 0] [0]
[0 3 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_4(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [3]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the
strict component of the input problem is
not empty
We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
Strict Trs:
{D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) ->
c_4(D^#(x), D^#(y))
, D^#(-(x, y)) ->
c_5(D^#(x), D^#(y))
, D^#(+(x, y)) ->
c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict Trs:
{D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) ->
c_4(D^#(x), D^#(y))
, D^#(-(x, y)) ->
c_5(D^#(x), D^#(y))
, D^#(+(x, y)) ->
c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
Strict Trs:
{D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) ->
c_4(D^#(x), D^#(y))
, D^#(-(x, y)) ->
c_5(D^#(x), D^#(y))
, D^#(+(x, y)) ->
c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
The weightgap principle does not apply
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: innermost
1) None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
Arrrr..Tool pair3rc
| Execution Time | Unknown |
|---|
| Answer | MAYBE |
|---|
| Input | Der95 08 |
|---|
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
The processor is not applicable, reason is:
Input problem is not restricted to innermost rewriting
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
1) None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'dp' failed due to the following reason:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
We consider the following Problem:
Strict DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'Fastest':
-------------------------
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'compose (statically using 'split all congruence from CWD except leafs', multiplication)' failed due to the following reason:
Compose is inapplicable since some strict rule is size increasing
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
1) The processor is inapplicable since the strict component of the
input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0] x1 + [0]
[0 0] [0]
t() = [0]
[0]
1() = [3]
[0]
constant() = [0]
[0]
0() = [3]
[0]
+(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
*(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
-(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
D^#(x1) = [0 0] x1 + [1]
[0 0] [0]
c_1() = [0]
[0]
c_2() = [0]
[0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [2]
c_4(x1, x2, x3, x4) = [0 0] x1 + [1 0] x2 + [0 0] x3 + [1 0] x4 + [3]
[3 0] [0 1] [3 3] [0 1] [3]
c_5(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [3]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of the
input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ D(t()) -> 1()
, D(constant()) -> 0()}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0] x1 + [2]
[0 0] [1]
t() = [0]
[0]
1() = [1]
[1]
constant() = [0]
[0]
0() = [1]
[1]
+(x1, x2) = [1 0] x1 + [1 2] x2 + [0]
[0 0] [0 0] [0]
*(x1, x2) = [0 0] x1 + [1 1] x2 + [1]
[0 0] [0 0] [2]
-(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
D^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_1() = [0]
[0]
c_2() = [0]
[0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
c_4(x1, x2, x3, x4) = [0 0] x1 + [1 0] x2 + [0 0] x3 + [1 0] x4 + [3]
[3 2] [0 1] [3 2] [0 1] [3]
c_5(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of the
input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 0] x1 + [0]
[0 0 1] [0]
[0 0 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 1 2] [0]
[0 0 1] [0 0 1] [1]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 1 2] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
D^#(x1) = [0 0 2] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [3]
[3 3 0] [0 1 0] [3 0 2] [0 1 0] [3]
[3 0 0] [0 0 1] [3 0 3] [0 0 1] [3]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 1 0] [0 1 0] [3]
[0 0 1] [0 0 1] [3]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component of
the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs: {D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2}, Uargs(*) = {2},
Uargs(-) = {1, 2}, Uargs(D^#) = {},
Uargs(c_3) = {1, 2}, Uargs(c_4) = {2, 4},
Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [1]
D^#(x1) = [0 0 1] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [3]
[3 0 0] [0 1 0] [3 3 0] [0 1 0] [3]
[3 0 0] [0 0 1] [3 0 0] [0 0 1] [3]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs: {D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict component
of the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict DPs: {D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict DPs:
{D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2},
Uargs(*) = {2}, Uargs(-) = {1, 2},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 2] [0 1 2] [0]
[0 0 0] [0 0 0] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 1 1] [0 1 2] [2]
[0 0 0] [0 0 0] [2]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
D^#(x1) = [0 2 2] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_4(x1, x2, x3, x4) = [0 0 1] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [3]
[0 0 0] [0 1 0] [0 0 0] [0 1 0] [0]
[0 0 0] [0 0 1] [0 0 0] [0 0 1] [0]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict
component of the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {D(-(x, y)) -> -(D(x), D(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2},
Uargs(*) = {2}, Uargs(-) = {1, 2},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4}, Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 1] x1 + [0]
[0 0 1] [0]
[0 2 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 0 0] [0]
[0 0 1] [0 0 1] [0]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [2]
[0 0 1] [0 0 1] [2]
D^#(x1) = [0 0 2] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [0]
[0 0 0] [0 1 0] [0 0 0] [0 1 0] [0]
[0 0 0] [0 0 1] [0 0 0] [0 0 1] [0]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [3]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the strict
component of the input problem is not empty
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{D(+(x, y)) -> +(D(x), D(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {1, 2},
Uargs(*) = {2}, Uargs(-) = {1, 2},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {2, 4},
Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0 1] x1 + [0]
[0 0 0] [0]
[2 0 0] [0]
t() = [0]
[0]
[0]
1() = [0]
[0]
[0]
constant() = [0]
[0]
[0]
0() = [0]
[0]
[0]
+(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [2]
*(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [0]
-(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 1] [0 0 1] [0]
D^#(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
c_1() = [0]
[0]
[0]
c_2() = [0]
[0]
[0]
c_3(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
c_4(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [0]
[0 0 0] [0 1 0] [0 0 0] [0 1 0] [0]
[0 0 0] [0 0 1] [0 0 0] [0 0 1] [0]
c_5(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [0]
[0 0 1] [0 0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
The processor is inapplicable since the
strict component of the input problem is
not empty
We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
Strict Trs:
{D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) ->
c_5(D^#(x), D^#(y))
, D^#(+(x, y)) ->
c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Strict Trs:
{D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) ->
c_5(D^#(x), D^#(y))
, D^#(+(x, y)) ->
c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
Strict Trs:
{D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) ->
c_5(D^#(x), D^#(y))
, D^#(+(x, y)) ->
c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
The weightgap principle does not apply
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{D(*(x, y)) ->
+(*(y, D(x)), *(x, D(y)))}
Weak DPs:
{ D^#(*(x, y)) ->
c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(t()) -> c_1()
, D^#(constant()) -> c_2()}
Weak Trs:
{ D(+(x, y)) -> +(D(x), D(y))
, D(-(x, y)) -> -(D(x), D(y))
, D(t()) -> 1()
, D(constant()) -> 0()}
StartTerms: basic terms
Strategy: none
1) None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
match-boundness of the problem could not be verified.
Arrrr..Tool rc
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | Der95 08 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
'dp' proved the goal fastest:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
We consider the following Problem:
Strict DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'usablerules':
-----------------------------
No rule is usable.
We consider the following Problem:
Strict DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'Fastest':
-------------------------
'removetails >>> ... >>> ... >>> ...' proved the goal fastest:
We consider the the dependency-graph
1: D^#(t()) -> c_1()
2: D^#(constant()) -> c_2()
3: D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
--> D^#(-(x, y)) -> c_5(D^#(x), D^#(y)): 5
--> D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y)): 4
--> D^#(+(x, y)) -> c_3(D^#(x), D^#(y)): 3
--> D^#(constant()) -> c_2(): 2
--> D^#(t()) -> c_1(): 1
4: D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
--> D^#(-(x, y)) -> c_5(D^#(x), D^#(y)): 5
--> D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y)): 4
--> D^#(+(x, y)) -> c_3(D^#(x), D^#(y)): 3
--> D^#(constant()) -> c_2(): 2
--> D^#(t()) -> c_1(): 1
5: D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
--> D^#(-(x, y)) -> c_5(D^#(x), D^#(y)): 5
--> D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y)): 4
--> D^#(+(x, y)) -> c_3(D^#(x), D^#(y)): 3
--> D^#(constant()) -> c_2(): 2
--> D^#(t()) -> c_1(): 1
together with the congruence-graph
->{3,5,4}
|
|->{1} Noncyclic, trivial, SCC
|
`->{2} Noncyclic, trivial, SCC
Here rules are as follows:
{ 1: D^#(t()) -> c_1()
, 2: D^#(constant()) -> c_2()
, 3: D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, 4: D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, 5: D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: D^#(constant()) -> c_2()
, 1: D^#(t()) -> c_1()}
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'simpDPRHS >>> ...':
-----------------------------------
The right-hand sides of following rules could be simplified:
{D^#(*(x, y)) -> c_4(y, D^#(x), x, D^#(y))}
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_1(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_3(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'usablerules':
-----------------------------
No rule is usable.
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_1(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_3(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs: {D^#(-(x, y)) -> c_3(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {},
Uargs(D^#) = {}, Uargs(c_3) = {}, Uargs(c_4) = {}, Uargs(c_5) = {},
Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0] x1 + [0]
[0 0] [0]
t() = [0]
[0]
1() = [0]
[0]
constant() = [0]
[0]
0() = [0]
[0]
+(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
*(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
-(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 0] [0 0] [0]
D^#(x1) = [1 0] x1 + [0]
[0 0] [0]
c_1() = [0]
[0]
c_2() = [0]
[0]
c_3(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
c_4(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0]
[0 0] [0 0] [0 0] [0 0] [0]
c_5(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
c_1(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
c_2(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_1(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_2(D^#(x), D^#(y))}
Weak DPs: {D^#(-(x, y)) -> c_3(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
No dependency-pair could be removed
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_1(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_2(D^#(x), D^#(y))}
Weak DPs: {D^#(-(x, y)) -> c_3(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs: {D^#(*(x, y)) -> c_2(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {},
Uargs(D^#) = {}, Uargs(c_3) = {}, Uargs(c_4) = {}, Uargs(c_5) = {},
Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0] x1 + [0]
[0 0] [0]
t() = [0]
[0]
1() = [0]
[0]
constant() = [0]
[0]
0() = [0]
[0]
+(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [0]
*(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [2]
-(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [0]
D^#(x1) = [0 1] x1 + [0]
[0 0] [0]
c_1() = [0]
[0]
c_2() = [0]
[0]
c_3(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
c_4(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0]
[0 0] [0 0] [0 0] [0 0] [0]
c_5(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
c_1(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [3]
c_2(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs: {D^#(+(x, y)) -> c_1(D^#(x), D^#(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_3(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
No dependency-pair could be removed
We abort the transformation and continue with the subprocessor on the problem
Strict DPs: {D^#(+(x, y)) -> c_1(D^#(x), D^#(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_3(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs: {D^#(+(x, y)) -> c_1(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {},
Uargs(D^#) = {}, Uargs(c_3) = {}, Uargs(c_4) = {}, Uargs(c_5) = {},
Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0] x1 + [0]
[0 0] [0]
t() = [0]
[0]
1() = [0]
[0]
constant() = [0]
[0]
0() = [0]
[0]
+(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [2]
*(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [2]
-(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [0]
D^#(x1) = [0 2] x1 + [0]
[0 0] [0]
c_1() = [0]
[0]
c_2() = [0]
[0]
c_3(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
c_4(x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0]
[0 0] [0 0] [0 0] [0 0] [0]
c_5(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
c_1(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [0]
c_2(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Weak DPs:
{ D^#(+(x, y)) -> c_1(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_2(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_3(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: none
Certificate: YES(O(1),O(1))
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
We consider the the dependency-graph
1: D^#(+(x, y)) -> c_1(D^#(x), D^#(y))
--> D^#(-(x, y)) -> c_3(D^#(x), D^#(y)): 3
--> D^#(*(x, y)) -> c_2(D^#(x), D^#(y)): 2
--> D^#(+(x, y)) -> c_1(D^#(x), D^#(y)): 1
2: D^#(*(x, y)) -> c_2(D^#(x), D^#(y))
--> D^#(-(x, y)) -> c_3(D^#(x), D^#(y)): 3
--> D^#(*(x, y)) -> c_2(D^#(x), D^#(y)): 2
--> D^#(+(x, y)) -> c_1(D^#(x), D^#(y)): 1
3: D^#(-(x, y)) -> c_3(D^#(x), D^#(y))
--> D^#(-(x, y)) -> c_3(D^#(x), D^#(y)): 3
--> D^#(*(x, y)) -> c_2(D^#(x), D^#(y)): 2
--> D^#(+(x, y)) -> c_1(D^#(x), D^#(y)): 1
together with the congruence-graph
->{1,3,2} Weak SCC
Here rules are as follows:
{ 1: D^#(+(x, y)) -> c_1(D^#(x), D^#(y))
, 2: D^#(*(x, y)) -> c_2(D^#(x), D^#(y))
, 3: D^#(-(x, y)) -> c_3(D^#(x), D^#(y))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 1: D^#(+(x, y)) -> c_1(D^#(x), D^#(y))
, 3: D^#(-(x, y)) -> c_3(D^#(x), D^#(y))
, 2: D^#(*(x, y)) -> c_2(D^#(x), D^#(y))}
We consider the following Problem:
StartTerms: basic terms
Strategy: none
Certificate: YES(O(1),O(1))
Application of 'simpDPRHS >>> ...':
-----------------------------------
No rule was simplified
We apply the transformation 'usablerules' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
StartTerms: basic terms
Strategy: none
The input problem is not a DP-problem.
We abort the transformation and continue with the subprocessor on the problem
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
StartTerms: basic terms
Strategy: none
All strict components are empty, nothing to further orient
We abort the transformation and continue with the subprocessor on the problem
StartTerms: basic terms
Strategy: none
1) No dependency-pair could be removed
We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
StartTerms: basic terms
Strategy: none
All strict components are empty, nothing to further orient
We abort the transformation and continue with the subprocessor on the problem
StartTerms: basic terms
Strategy: none
1) 'Sequentially' proved the goal fastest:
'empty' succeeded:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))Tool tup3irc
| Execution Time | 3.415903ms |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | Der95 08 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
The input problem contains no overlaps that give rise to inapplicable rules.
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: innermost
1) 'dp' proved the goal fastest:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
We consider the following Problem:
Strict DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Application of 'Fastest':
-------------------------
'compose (statically using 'split all congruence from CWD except leafs', multiplication)' proved the goal fastest:
Compose is inapplicable since some weak rule is size increasing
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(t()) -> c_1()
, D^#(constant()) -> c_2()
, D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: innermost
1) We consider the the dependency-graph
1: D^#(t()) -> c_1()
2: D^#(constant()) -> c_2()
3: D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
--> D^#(-(x, y)) -> c_5(D^#(x), D^#(y)): 5
--> D^#(*(x, y)) -> c_4(D^#(x), D^#(y)): 4
--> D^#(+(x, y)) -> c_3(D^#(x), D^#(y)): 3
--> D^#(constant()) -> c_2(): 2
--> D^#(t()) -> c_1(): 1
4: D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
--> D^#(-(x, y)) -> c_5(D^#(x), D^#(y)): 5
--> D^#(*(x, y)) -> c_4(D^#(x), D^#(y)): 4
--> D^#(+(x, y)) -> c_3(D^#(x), D^#(y)): 3
--> D^#(constant()) -> c_2(): 2
--> D^#(t()) -> c_1(): 1
5: D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
--> D^#(-(x, y)) -> c_5(D^#(x), D^#(y)): 5
--> D^#(*(x, y)) -> c_4(D^#(x), D^#(y)): 4
--> D^#(+(x, y)) -> c_3(D^#(x), D^#(y)): 3
--> D^#(constant()) -> c_2(): 2
--> D^#(t()) -> c_1(): 1
together with the congruence-graph
->{3,5,4}
|
|->{1} Noncyclic, trivial, SCC
|
`->{2} Noncyclic, trivial, SCC
Here rules are as follows:
{ 1: D^#(t()) -> c_1()
, 2: D^#(constant()) -> c_2()
, 3: D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, 4: D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, 5: D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: D^#(constant()) -> c_2()
, 1: D^#(t()) -> c_1()}
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Application of 'simpDPRHS >>> ...':
-----------------------------------
No rule was simplified
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Weak Trs:
{ D(t()) -> 1()
, D(constant()) -> 0()
, D(+(x, y)) -> +(D(x), D(y))
, D(*(x, y)) -> +(*(y, D(x)), *(x, D(y)))
, D(-(x, y)) -> -(D(x), D(y))}
StartTerms: basic terms
Strategy: innermost
1) No rule is usable.
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Application of 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...':
--------------------------------------------------------------------------------
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs: {D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2},
Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0] x1 + [0]
[0 0] [0]
t() = [0]
[0]
1() = [0]
[0]
constant() = [0]
[0]
0() = [0]
[0]
+(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
*(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
-(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 0] [0 0] [0]
D^#(x1) = [1 0] x1 + [0]
[0 0] [0]
c_1() = [0]
[0]
c_2() = [0]
[0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
c_4(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [3]
c_5(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))}
Weak DPs: {D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
No dependency-pair could be removed
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))}
Weak DPs: {D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: innermost
1) The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs: {D^#(*(x, y)) -> c_4(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2},
Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0] x1 + [0]
[0 0] [0]
t() = [0]
[0]
1() = [0]
[0]
constant() = [0]
[0]
0() = [0]
[0]
+(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [0]
*(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [2]
-(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [0]
D^#(x1) = [0 1] x1 + [0]
[0 0] [0]
c_1() = [0]
[0]
c_2() = [0]
[0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [3]
c_4(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [0]
c_5(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
No dependency-pair could be removed
We abort the transformation and continue with the subprocessor on the problem
Strict DPs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Weak DPs:
{ D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: innermost
1) The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs: {D^#(+(x, y)) -> c_3(D^#(x), D^#(y))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(D) = {}, Uargs(+) = {}, Uargs(*) = {}, Uargs(-) = {},
Uargs(D^#) = {}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2},
Uargs(c_5) = {1, 2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
D(x1) = [0 0] x1 + [0]
[0 0] [0]
t() = [0]
[0]
1() = [0]
[0]
constant() = [0]
[0]
0() = [0]
[0]
+(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [2]
*(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [2]
-(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [0]
D^#(x1) = [0 2] x1 + [0]
[0 0] [0]
c_1() = [0]
[0]
c_2() = [0]
[0]
c_3(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [0]
c_4(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [0]
c_5(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Weak DPs:
{ D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
We consider the the dependency-graph
1: D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
--> D^#(-(x, y)) -> c_5(D^#(x), D^#(y)): 3
--> D^#(*(x, y)) -> c_4(D^#(x), D^#(y)): 2
--> D^#(+(x, y)) -> c_3(D^#(x), D^#(y)): 1
2: D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
--> D^#(-(x, y)) -> c_5(D^#(x), D^#(y)): 3
--> D^#(*(x, y)) -> c_4(D^#(x), D^#(y)): 2
--> D^#(+(x, y)) -> c_3(D^#(x), D^#(y)): 1
3: D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
--> D^#(-(x, y)) -> c_5(D^#(x), D^#(y)): 3
--> D^#(*(x, y)) -> c_4(D^#(x), D^#(y)): 2
--> D^#(+(x, y)) -> c_3(D^#(x), D^#(y)): 1
together with the congruence-graph
->{1,3,2} Weak SCC
Here rules are as follows:
{ 1: D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, 2: D^#(*(x, y)) -> c_4(D^#(x), D^#(y))
, 3: D^#(-(x, y)) -> c_5(D^#(x), D^#(y))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 1: D^#(+(x, y)) -> c_3(D^#(x), D^#(y))
, 3: D^#(-(x, y)) -> c_5(D^#(x), D^#(y))
, 2: D^#(*(x, y)) -> c_4(D^#(x), D^#(y))}
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Application of 'simpDPRHS >>> ...':
-----------------------------------
No rule was simplified
We apply the transformation 'usablerules' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
StartTerms: basic terms
Strategy: innermost
The input problem is not a DP-problem.
We abort the transformation and continue with the subprocessor on the problem
StartTerms: basic terms
Strategy: innermost
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
StartTerms: basic terms
Strategy: innermost
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
StartTerms: basic terms
Strategy: innermost
All strict components are empty, nothing to further orient
We abort the transformation and continue with the subprocessor on the problem
StartTerms: basic terms
Strategy: innermost
1) No dependency-pair could be removed
We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
StartTerms: basic terms
Strategy: innermost
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
StartTerms: basic terms
Strategy: innermost
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
StartTerms: basic terms
Strategy: innermost
All strict components are empty, nothing to further orient
We abort the transformation and continue with the subprocessor on the problem
StartTerms: basic terms
Strategy: innermost
1) 'empty' succeeded:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))