Tool CaT
| Execution Time | Unknown |
|---|
| Answer | MAYBE |
|---|
| Input | SK90 2.39 |
|---|
stdout:
MAYBE
Problem:
rev(nil()) -> nil()
rev(.(x,y)) -> ++(rev(y),.(x,nil()))
car(.(x,y)) -> x
cdr(.(x,y)) -> y
null(nil()) -> true()
null(.(x,y)) -> false()
++(nil(),y) -> y
++(.(x,y),z) -> .(x,++(y,z))
Proof:
Complexity Transformation Processor:
strict:
rev(nil()) -> nil()
rev(.(x,y)) -> ++(rev(y),.(x,nil()))
car(.(x,y)) -> x
cdr(.(x,y)) -> y
null(nil()) -> true()
null(.(x,y)) -> false()
++(nil(),y) -> y
++(.(x,y),z) -> .(x,++(y,z))
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[false] = 0,
[true] = 0,
[null](x0) = x0 + 16,
[cdr](x0) = x0 + 68,
[car](x0) = x0,
[++](x0, x1) = x0 + x1 + 36,
[.](x0, x1) = x0 + x1 + 16,
[rev](x0) = x0 + 106,
[nil] = 33
orientation:
rev(nil()) = 139 >= 33 = nil()
rev(.(x,y)) = x + y + 122 >= x + y + 191 = ++(rev(y),.(x,nil()))
car(.(x,y)) = x + y + 16 >= x = x
cdr(.(x,y)) = x + y + 84 >= y = y
null(nil()) = 49 >= 0 = true()
null(.(x,y)) = x + y + 32 >= 0 = false()
++(nil(),y) = y + 69 >= y = y
++(.(x,y),z) = x + y + z + 52 >= x + y + z + 52 = .(x,++(y,z))
problem:
strict:
rev(.(x,y)) -> ++(rev(y),.(x,nil()))
++(.(x,y),z) -> .(x,++(y,z))
weak:
rev(nil()) -> nil()
car(.(x,y)) -> x
cdr(.(x,y)) -> y
null(nil()) -> true()
null(.(x,y)) -> false()
++(nil(),y) -> y
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {9,8,7,6,5}
transitions:
++1(10,11) -> 10*
++1(12,11) -> 12,5
rev1(2) -> 12*
rev1(4) -> 12*
rev1(1) -> 12*
rev1(3) -> 12*
.1(2,10) -> 11*
.1(4,10) -> 11*
.1(1,10) -> 11*
.1(3,10) -> 11*
nil1() -> 12,10
rev0(2) -> 5*
rev0(4) -> 5*
rev0(1) -> 5*
rev0(3) -> 5*
.0(3,1) -> 1*
.0(3,3) -> 1*
.0(4,2) -> 1*
.0(4,4) -> 1*
.0(4,6) -> 6*
.0(1,2) -> 1*
.0(1,4) -> 1*
.0(1,6) -> 6*
.0(2,1) -> 1*
.0(2,3) -> 1*
.0(3,2) -> 1*
.0(3,4) -> 1*
.0(3,6) -> 6*
.0(4,1) -> 1*
.0(4,3) -> 1*
.0(1,1) -> 1*
.0(1,3) -> 1*
.0(2,2) -> 1*
.0(2,4) -> 1*
.0(2,6) -> 6*
++0(3,1) -> 6*
++0(3,3) -> 6*
++0(4,2) -> 6*
++0(4,4) -> 6*
++0(1,2) -> 6*
++0(1,4) -> 6*
++0(2,1) -> 6*
++0(2,3) -> 6*
++0(3,2) -> 6*
++0(3,4) -> 6*
++0(4,1) -> 6*
++0(4,3) -> 6*
++0(1,1) -> 6*
++0(1,3) -> 6*
++0(2,2) -> 6*
++0(2,4) -> 6*
nil0() -> 5,2
car0(2) -> 7*
car0(4) -> 7*
car0(1) -> 7*
car0(3) -> 7*
cdr0(2) -> 8*
cdr0(4) -> 8*
cdr0(1) -> 8*
cdr0(3) -> 8*
null0(2) -> 9*
null0(4) -> 9*
null0(1) -> 9*
null0(3) -> 9*
true0() -> 9,3
false0() -> 9,4
1 -> 6,8,7
2 -> 6,8,7
3 -> 6,8,7
4 -> 6,8,7
11 -> 10,5,12
problem:
strict:
++(.(x,y),z) -> .(x,++(y,z))
weak:
rev(.(x,y)) -> ++(rev(y),.(x,nil()))
rev(nil()) -> nil()
car(.(x,y)) -> x
cdr(.(x,y)) -> y
null(nil()) -> true()
null(.(x,y)) -> false()
++(nil(),y) -> y
Open
Tool IRC1
| Execution Time | Unknown |
|---|
| Answer | MAYBE |
|---|
| Input | SK90 2.39 |
|---|
stdout:
MAYBE
Tool IRC2
| Execution Time | Unknown |
|---|
| Answer | TIMEOUT |
|---|
| Input | SK90 2.39 |
|---|
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, car(.(x, y)) -> x
, cdr(.(x, y)) -> y
, null(nil()) -> true()
, null(.(x, y)) -> false()
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
| Execution Time | Unknown |
|---|
| Answer | MAYBE |
|---|
| Input | SK90 2.39 |
|---|
stdout:
MAYBE
Tool RC2
| Execution Time | Unknown |
|---|
| Answer | TIMEOUT |
|---|
| Input | SK90 2.39 |
|---|
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, car(.(x, y)) -> x
, cdr(.(x, y)) -> y
, null(nil()) -> true()
, null(.(x, y)) -> false()
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool pair1rc
| Execution Time | Unknown |
|---|
| Answer | TIMEOUT |
|---|
| Input | SK90 2.39 |
|---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, car(.(x, y)) -> x
, cdr(.(x, y)) -> y
, null(nil()) -> true()
, null(.(x, y)) -> false()
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
StartTerms: basic terms
Strategy: none
Certificate: TIMEOUT
Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool pair2rc
| Execution Time | Unknown |
|---|
| Answer | TIMEOUT |
|---|
| Input | SK90 2.39 |
|---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, car(.(x, y)) -> x
, cdr(.(x, y)) -> y
, null(nil()) -> true()
, null(.(x, y)) -> false()
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
StartTerms: basic terms
Strategy: none
Certificate: TIMEOUT
Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool pair3irc
| Execution Time | Unknown |
|---|
| Answer | TIMEOUT |
|---|
| Input | SK90 2.39 |
|---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, car(.(x, y)) -> x
, cdr(.(x, y)) -> y
, null(nil()) -> true()
, null(.(x, y)) -> false()
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
StartTerms: basic terms
Strategy: innermost
Certificate: TIMEOUT
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool pair3rc
| Execution Time | Unknown |
|---|
| Answer | TIMEOUT |
|---|
| Input | SK90 2.39 |
|---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, car(.(x, y)) -> x
, cdr(.(x, y)) -> y
, null(nil()) -> true()
, null(.(x, y)) -> false()
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
StartTerms: basic terms
Strategy: none
Certificate: TIMEOUT
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..Tool rc
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | SK90 2.39 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, car(.(x, y)) -> x
, cdr(.(x, y)) -> y
, null(nil()) -> true()
, null(.(x, y)) -> false()
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
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:
{ rev^#(nil()) -> c_1()
, rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)
, ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
We consider the following Problem:
Strict DPs:
{ rev^#(nil()) -> c_1()
, rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)
, ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, car(.(x, y)) -> x
, cdr(.(x, y)) -> y
, null(nil()) -> true()
, null(.(x, y)) -> false()
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'usablerules':
-----------------------------
We replace strict/weak-rules by the corresponding usable rules:
Strict Usable Rules:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
We consider the following Problem:
Strict DPs:
{ rev^#(nil()) -> c_1()
, rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)
, ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'Fastest':
-------------------------
'removetails >>> ... >>> ... >>> ...' proved the goal fastest:
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:
{ rev^#(nil()) -> c_1()
, rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)
, ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{ rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
Interpretation:
---------------
The following argument positions are usable:
Uargs(rev) = {}, Uargs(.) = {2}, Uargs(++) = {1}, Uargs(car) = {},
Uargs(cdr) = {}, Uargs(null) = {}, Uargs(rev^#) = {},
Uargs(c_2) = {1}, Uargs(++^#) = {1}, Uargs(car^#) = {},
Uargs(c_3) = {}, Uargs(cdr^#) = {}, Uargs(c_4) = {},
Uargs(null^#) = {}, Uargs(c_7) = {}, Uargs(c_8) = {2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
rev(x1) = [1 0] x1 + [0]
[0 0] [0]
nil() = [0]
[0]
.(x1, x2) = [1 2] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
++(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 0] [0 0] [3]
car(x1) = [0 0] x1 + [0]
[0 0] [0]
cdr(x1) = [0 0] x1 + [0]
[0 0] [0]
null(x1) = [0 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
false() = [0]
[0]
rev^#(x1) = [2 3] x1 + [3]
[0 0] [3]
c_1() = [0]
[1]
c_2(x1) = [1 0] x1 + [3]
[0 1] [3]
++^#(x1, x2) = [2 0] x1 + [0 0] x2 + [3]
[0 0] [0 0] [0]
car^#(x1) = [3 3] x1 + [3]
[3 3] [3]
c_3(x1) = [1 0] x1 + [0]
[1 0] [1]
cdr^#(x1) = [3 3] x1 + [3]
[0 0] [3]
c_4(x1) = [1 0] x1 + [0]
[0 0] [1]
null^#(x1) = [3 3] x1 + [3]
[0 0] [3]
c_5() = [0]
[1]
c_6() = [0]
[1]
c_7(x1) = [0 0] x1 + [0]
[0 0] [0]
c_8(x1, x2) = [0 0] x1 + [1 0] x2 + [3]
[0 0] [0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
Weak DPs:
{ rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
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:
{ rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
Weak DPs:
{ rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {rev(nil()) -> nil()}
Interpretation:
---------------
The following argument positions are usable:
Uargs(rev) = {}, Uargs(.) = {2}, Uargs(++) = {1}, Uargs(car) = {},
Uargs(cdr) = {}, Uargs(null) = {}, Uargs(rev^#) = {},
Uargs(c_2) = {1}, Uargs(++^#) = {1}, Uargs(car^#) = {},
Uargs(c_3) = {}, Uargs(cdr^#) = {}, Uargs(c_4) = {},
Uargs(null^#) = {}, Uargs(c_7) = {}, Uargs(c_8) = {2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
rev(x1) = [2 0] x1 + [0]
[2 0] [0]
nil() = [2]
[0]
.(x1, x2) = [1 2] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
++(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
car(x1) = [0 0] x1 + [0]
[0 0] [0]
cdr(x1) = [0 0] x1 + [0]
[0 0] [0]
null(x1) = [0 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
false() = [0]
[0]
rev^#(x1) = [2 0] x1 + [1]
[2 0] [0]
c_1() = [1]
[0]
c_2(x1) = [1 0] x1 + [3]
[0 1] [2]
++^#(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
car^#(x1) = [0 0] x1 + [3]
[0 0] [3]
c_3(x1) = [0 0] x1 + [1]
[0 0] [1]
cdr^#(x1) = [0 0] x1 + [3]
[3 3] [3]
c_4(x1) = [0 0] x1 + [1]
[1 0] [1]
null^#(x1) = [0 0] x1 + [3]
[0 0] [3]
c_5() = [1]
[1]
c_6() = [1]
[1]
c_7(x1) = [0 0] x1 + [0]
[0 0] [0]
c_8(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 0] [0 1] [3]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
Weak DPs:
{ rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
Weak Trs: {rev(nil()) -> nil()}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
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:
{ rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
Weak DPs:
{ rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
Weak Trs: {rev(nil()) -> nil()}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {++(nil(), y) -> y}
Interpretation:
---------------
The following argument positions are usable:
Uargs(rev) = {}, Uargs(.) = {2}, Uargs(++) = {1}, Uargs(car) = {},
Uargs(cdr) = {}, Uargs(null) = {}, Uargs(rev^#) = {},
Uargs(c_2) = {1}, Uargs(++^#) = {1}, Uargs(car^#) = {},
Uargs(c_3) = {}, Uargs(cdr^#) = {}, Uargs(c_4) = {},
Uargs(null^#) = {}, Uargs(c_7) = {}, Uargs(c_8) = {2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
rev(x1) = [2 0] x1 + [0]
[2 0] [0]
nil() = [2]
[0]
.(x1, x2) = [1 2] x1 + [1 0] x2 + [0]
[0 0] [0 0] [2]
++(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 2] [0 2] [0]
car(x1) = [0 0] x1 + [0]
[0 0] [0]
cdr(x1) = [0 0] x1 + [0]
[0 0] [0]
null(x1) = [0 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
false() = [0]
[0]
rev^#(x1) = [2 0] x1 + [1]
[0 0] [0]
c_1() = [1]
[0]
c_2(x1) = [1 0] x1 + [3]
[0 1] [2]
++^#(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
car^#(x1) = [3 3] x1 + [3]
[0 0] [3]
c_3(x1) = [1 0] x1 + [1]
[0 0] [1]
cdr^#(x1) = [3 3] x1 + [3]
[3 3] [3]
c_4(x1) = [1 0] x1 + [1]
[1 0] [1]
null^#(x1) = [0 0] x1 + [3]
[0 0] [3]
c_5() = [1]
[1]
c_6() = [1]
[1]
c_7(x1) = [0 0] x1 + [0]
[0 0] [0]
c_8(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 0] [0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))}
Weak DPs:
{ rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
Weak Trs:
{ ++(nil(), y) -> y
, rev(nil()) -> nil()}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
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:
{ rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))}
Weak DPs:
{ rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
Weak Trs:
{ ++(nil(), y) -> y
, rev(nil()) -> nil()}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(rev) = {}, Uargs(.) = {2}, Uargs(++) = {1}, Uargs(car) = {},
Uargs(cdr) = {}, Uargs(null) = {}, Uargs(rev^#) = {},
Uargs(c_2) = {1}, Uargs(++^#) = {1}, Uargs(car^#) = {},
Uargs(c_3) = {}, Uargs(cdr^#) = {}, Uargs(c_4) = {},
Uargs(null^#) = {}, Uargs(c_7) = {}, Uargs(c_8) = {2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
rev(x1) = [1 0] x1 + [0]
[0 0] [0]
nil() = [0]
[0]
.(x1, x2) = [1 2] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
++(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 2] [0]
car(x1) = [0 0] x1 + [0]
[0 0] [0]
cdr(x1) = [0 0] x1 + [0]
[0 0] [0]
null(x1) = [0 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
false() = [0]
[0]
rev^#(x1) = [2 0] x1 + [1]
[2 0] [0]
c_1() = [1]
[0]
c_2(x1) = [1 0] x1 + [0]
[0 1] [0]
++^#(x1, x2) = [2 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
car^#(x1) = [0 0] x1 + [3]
[3 3] [3]
c_3(x1) = [0 0] x1 + [1]
[1 0] [1]
cdr^#(x1) = [3 3] x1 + [3]
[3 3] [3]
c_4(x1) = [1 0] x1 + [1]
[1 0] [1]
null^#(x1) = [0 0] x1 + [3]
[0 0] [3]
c_5() = [1]
[1]
c_6() = [1]
[1]
c_7(x1) = [0 0] x1 + [0]
[0 0] [0]
c_8(x1, x2) = [0 0] x1 + [1 0] x2 + [3]
[0 0] [0 1] [3]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs: {++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))}
Weak DPs:
{ rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
Weak Trs:
{ ++(nil(), y) -> y
, rev(nil()) -> nil()}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
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: {++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))}
Weak DPs:
{ rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
Weak Trs:
{ ++(nil(), y) -> y
, rev(nil()) -> nil()}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {++(.(x, y), z) -> .(x, ++(y, z))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(rev) = {}, Uargs(.) = {2}, Uargs(++) = {1}, Uargs(car) = {},
Uargs(cdr) = {}, Uargs(null) = {}, Uargs(rev^#) = {},
Uargs(c_2) = {1}, Uargs(++^#) = {1}, Uargs(car^#) = {},
Uargs(c_3) = {}, Uargs(cdr^#) = {}, Uargs(c_4) = {},
Uargs(null^#) = {}, Uargs(c_7) = {}, Uargs(c_8) = {2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
rev(x1) = [0 0] x1 + [0]
[0 0] [0]
nil() = [0]
[0]
.(x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[0 0] [0 0] [0]
++(x1, x2) = [2 0] x1 + [2 0] x2 + [0]
[0 0] [0 2] [0]
car(x1) = [0 0] x1 + [0]
[0 0] [0]
cdr(x1) = [0 0] x1 + [0]
[0 0] [0]
null(x1) = [0 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
false() = [0]
[0]
rev^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_1() = [0]
[0]
c_2(x1) = [1 0] x1 + [0]
[0 1] [0]
++^#(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
car^#(x1) = [0 0] x1 + [3]
[0 0] [3]
c_3(x1) = [0 0] x1 + [1]
[0 0] [1]
cdr^#(x1) = [3 3] x1 + [3]
[0 0] [3]
c_4(x1) = [1 0] x1 + [1]
[0 0] [1]
null^#(x1) = [0 0] x1 + [3]
[0 0] [3]
c_5() = [1]
[1]
c_6() = [1]
[1]
c_7(x1) = [0 0] x1 + [0]
[0 0] [0]
c_8(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [3]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs: {++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs: {rev(.(x, y)) -> ++(rev(y), .(x, nil()))}
Weak DPs:
{ rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
Weak Trs:
{ ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
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: {++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Strict Trs: {rev(.(x, y)) -> ++(rev(y), .(x, nil()))}
Weak DPs:
{ rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
Weak Trs:
{ ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs: {++^#(.(x, y), z) -> c_8(x, ++^#(y, z))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(rev) = {}, Uargs(.) = {2}, Uargs(++) = {1},
Uargs(car) = {}, Uargs(cdr) = {}, Uargs(null) = {},
Uargs(rev^#) = {}, Uargs(c_2) = {1}, Uargs(++^#) = {1},
Uargs(car^#) = {}, Uargs(c_3) = {}, Uargs(cdr^#) = {},
Uargs(c_4) = {}, Uargs(null^#) = {}, Uargs(c_7) = {},
Uargs(c_8) = {2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
rev(x1) = [0 0] x1 + [0]
[0 0] [0]
nil() = [0]
[0]
.(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [0]
++(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 2] [0]
car(x1) = [0 0] x1 + [0]
[0 0] [0]
cdr(x1) = [0 0] x1 + [0]
[0 0] [0]
null(x1) = [0 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
false() = [0]
[0]
rev^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_1() = [0]
[0]
c_2(x1) = [1 0] x1 + [0]
[0 1] [0]
++^#(x1, x2) = [2 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
car^#(x1) = [0 0] x1 + [3]
[3 3] [3]
c_3(x1) = [0 0] x1 + [1]
[0 0] [0]
cdr^#(x1) = [3 3] x1 + [3]
[0 0] [3]
c_4(x1) = [1 0] x1 + [0]
[0 0] [1]
null^#(x1) = [0 0] x1 + [3]
[0 0] [3]
c_5() = [1]
[1]
c_6() = [1]
[1]
c_7(x1) = [0 0] x1 + [0]
[0 0] [0]
c_8(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {rev(.(x, y)) -> ++(rev(y), .(x, nil()))}
Weak DPs:
{ ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))
, rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
Weak Trs:
{ ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
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: {rev(.(x, y)) -> ++(rev(y), .(x, nil()))}
Weak DPs:
{ ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))
, rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
Weak Trs:
{ ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
StartTerms: basic terms
Strategy: none
1) The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {rev(.(x, y)) -> ++(rev(y), .(x, nil()))}
Interpretation:
---------------
The following argument positions are usable:
Uargs(rev) = {}, Uargs(.) = {2}, Uargs(++) = {1},
Uargs(car) = {}, Uargs(cdr) = {}, Uargs(null) = {},
Uargs(rev^#) = {}, Uargs(c_2) = {1}, Uargs(++^#) = {1},
Uargs(car^#) = {}, Uargs(c_3) = {}, Uargs(cdr^#) = {},
Uargs(c_4) = {}, Uargs(null^#) = {}, Uargs(c_7) = {},
Uargs(c_8) = {2}
We have the following constructor-restricted (at most 1 in the main diagonals) matrix interpretation:
Interpretation Functions:
rev(x1) = [3 0] x1 + [2]
[2 0] [2]
nil() = [1]
[2]
.(x1, x2) = [1 2] x1 + [1 0] x2 + [1]
[0 0] [0 0] [2]
++(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [0]
car(x1) = [0 0] x1 + [0]
[0 0] [0]
cdr(x1) = [0 0] x1 + [0]
[0 0] [0]
null(x1) = [0 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
false() = [0]
[0]
rev^#(x1) = [3 1] x1 + [0]
[2 3] [0]
c_1() = [1]
[0]
c_2(x1) = [1 0] x1 + [1]
[0 1] [2]
++^#(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
car^#(x1) = [3 3] x1 + [3]
[0 0] [3]
c_3(x1) = [1 0] x1 + [0]
[0 0] [1]
cdr^#(x1) = [0 0] x1 + [3]
[0 0] [3]
c_4(x1) = [0 0] x1 + [1]
[0 0] [1]
null^#(x1) = [0 0] x1 + [3]
[0 0] [3]
c_5() = [1]
[1]
c_6() = [1]
[1]
c_7(x1) = [0 0] x1 + [1]
[0 0] [0]
c_8(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Weak DPs:
{ ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))
, rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, rev^#(nil()) -> c_1()
, car^#(.(x, y)) -> c_3(x)
, cdr^#(.(x, y)) -> c_4(y)
, null^#(nil()) -> c_5()
, null^#(.(x, y)) -> c_6()
, ++^#(nil(), y) -> c_7(y)}
Weak Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
StartTerms: basic terms
Strategy: none
Certificate: YES(O(1),O(1))
Application of 'removetails >>> ... >>> ... >>> ...':
-----------------------------------------------------
We consider the the dependency-graph
1: ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))
--> ++^#(nil(), y) -> c_7(y): 8
--> ++^#(.(x, y), z) -> c_8(x, ++^#(y, z)): 1
2: rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
--> ++^#(nil(), y) -> c_7(y): 8
--> ++^#(.(x, y), z) -> c_8(x, ++^#(y, z)): 1
3: rev^#(nil()) -> c_1()
4: car^#(.(x, y)) -> c_3(x)
5: cdr^#(.(x, y)) -> c_4(y)
6: null^#(nil()) -> c_5()
7: null^#(.(x, y)) -> c_6()
8: ++^#(nil(), y) -> c_7(y)
together with the congruence-graph
->{2} Weak SCC
|
|->{1} Weak SCC
| |
| `->{8} Weak SCC
|
`->{8} Weak SCC
->{3} Weak SCC
->{4} Weak SCC
->{5} Weak SCC
->{6} Weak SCC
->{7} Weak SCC
Here rules are as follows:
{ 1: ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))
, 2: rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, 3: rev^#(nil()) -> c_1()
, 4: car^#(.(x, y)) -> c_3(x)
, 5: cdr^#(.(x, y)) -> c_4(y)
, 6: null^#(nil()) -> c_5()
, 7: null^#(.(x, y)) -> c_6()
, 8: ++^#(nil(), y) -> c_7(y)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 7: null^#(.(x, y)) -> c_6()
, 6: null^#(nil()) -> c_5()
, 5: cdr^#(.(x, y)) -> c_4(y)
, 4: car^#(.(x, y)) -> c_3(x)
, 3: rev^#(nil()) -> c_1()
, 2: rev^#(.(x, y)) -> c_2(++^#(rev(y), .(x, nil())))
, 1: ++^#(.(x, y), z) -> c_8(x, ++^#(y, z))
, 8: ++^#(nil(), y) -> c_7(y)}
We consider the following Problem:
Weak Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
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
Weak Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
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
Weak Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
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
Weak Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
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
Weak Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
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
Weak Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
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
Weak Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
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
Weak Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
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
Weak Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
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
Weak Trs:
{ rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, ++(.(x, y), z) -> .(x, ++(y, z))
, ++(nil(), y) -> y
, rev(nil()) -> nil()}
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 | 60.061115ms |
|---|
| Answer | TIMEOUT |
|---|
| Input | SK90 2.39 |
|---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ rev(nil()) -> nil()
, rev(.(x, y)) -> ++(rev(y), .(x, nil()))
, car(.(x, y)) -> x
, cdr(.(x, y)) -> y
, null(nil()) -> true()
, null(.(x, y)) -> false()
, ++(nil(), y) -> y
, ++(.(x, y), z) -> .(x, ++(y, z))}
StartTerms: basic terms
Strategy: innermost
Certificate: TIMEOUT
Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
Computation stopped due to timeout after 60.0 seconds
Arrrr..