Tool Bounds
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ h(cons(X, Y)) -> h(g(cons(X, Y)))
, g(cons(s(X), Y)) -> s(X)
, g(cons(0(), Y)) -> g(Y)
, f(s(X)) -> f(X)}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ s_0(1) -> 1
, s_1(1) -> 1
, s_1(1) -> 2
, s_2(1) -> 2
, f_0(1) -> 1
, f_1(1) -> 1
, f_2(1) -> 1
, 0_0() -> 1
, cons_0(1, 1) -> 1
, cons_1(1, 1) -> 3
, g_0(1) -> 1
, g_1(1) -> 1
, g_1(1) -> 2
, g_1(3) -> 2
, h_0(1) -> 1
, h_1(2) -> 1}
Hurray, we answered YES(?,O(n^1))Tool CDI
stdout:
YES(?,O(n^2))
QUADRATIC upper bound on the derivational complexity
This TRS is terminating using the deltarestricted interpretation
h(delta, X0) = + 0*X0 + 0 + 2*X0*delta + 0*delta
0(delta) = + 0 + 0*delta
cons(delta, X1, X0) = + 0*X0 + 0*X1 + 2 + 1*X0*delta + 2*X1*delta + 2*delta
g(delta, X0) = + 0*X0 + 0 + 1*X0*delta + 0*delta
s(delta, X0) = + 0*X0 + 0 + 3*X0*delta + 3*delta
f(delta, X0) = + 0*X0 + 0 + 3*X0*delta + 0*delta
h_tau_1(delta) = delta/(0 + 2 * delta)
cons_tau_1(delta) = delta/(0 + 2 * delta)
cons_tau_2(delta) = delta/(0 + 1 * delta)
g_tau_1(delta) = delta/(0 + 1 * delta)
s_tau_1(delta) = delta/(0 + 3 * delta)
f_tau_1(delta) = delta/(0 + 3 * delta)
Time: 0.400463 seconds
Statistics:
Number of monomials: 239
Last formula building started for bound 3
Last SAT solving started for bound 3Tool EDA
stdout:
YES(?,O(n^2))
We consider the following Problem:
Strict Trs:
{ h(cons(X, Y)) -> h(g(cons(X, Y)))
, g(cons(s(X), Y)) -> s(X)
, g(cons(0(), Y)) -> g(Y)
, f(s(X)) -> f(X)}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^2))
Proof:
We have the following EDA-non-satisfying matrix interpretation:
Interpretation Functions:
s(x1) = [1 0] x1 + [3]
[0 0] [0]
f(x1) = [1 0] x1 + [0]
[0 0] [3]
0() = [2]
[2]
cons(x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 0] [2]
g(x1) = [1 0] x1 + [1]
[0 0] [0]
h(x1) = [1 2] x1 + [0]
[0 0] [1]
Hurray, we answered YES(?,O(n^2))Tool IDA
stdout:
YES(?,O(n^2))
We consider the following Problem:
Strict Trs:
{ h(cons(X, Y)) -> h(g(cons(X, Y)))
, g(cons(s(X), Y)) -> s(X)
, g(cons(0(), Y)) -> g(Y)
, f(s(X)) -> f(X)}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^2))
Proof:
We have the following EDA-non-satisfying and IDA(2)-non-satisfying matrix interpretation:
Interpretation Functions:
s(x1) = [1 0] x1 + [3]
[0 0] [0]
f(x1) = [1 0] x1 + [0]
[0 0] [3]
0() = [2]
[0]
cons(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [2]
g(x1) = [1 0] x1 + [1]
[0 0] [0]
h(x1) = [1 2] x1 + [0]
[0 0] [1]
Hurray, we answered YES(?,O(n^2))Tool TRI
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ h(cons(X, Y)) -> h(g(cons(X, Y)))
, g(cons(s(X), Y)) -> s(X)
, g(cons(0(), Y)) -> g(Y)
, f(s(X)) -> f(X)}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
We have the following triangular matrix interpretation:
Interpretation Functions:
s(x1) = [1 3] x1 + [3]
[0 0] [0]
f(x1) = [1 3] x1 + [3]
[0 0] [3]
0() = [0]
[0]
cons(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [3]
g(x1) = [1 0] x1 + [0]
[0 0] [0]
h(x1) = [1 1] x1 + [0]
[0 0] [1]
Hurray, we answered YES(?,O(n^1))Tool TRI2
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ h(cons(X, Y)) -> h(g(cons(X, Y)))
, g(cons(s(X), Y)) -> s(X)
, g(cons(0(), Y)) -> g(Y)
, f(s(X)) -> f(X)}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
We have the following triangular matrix interpretation:
Interpretation Functions:
s(x1) = [1 0] x1 + [1]
[0 0] [0]
f(x1) = [1 0] x1 + [1]
[0 0] [3]
0() = [0]
[0]
cons(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 0] [0 0] [2]
g(x1) = [1 0] x1 + [0]
[0 0] [0]
h(x1) = [1 1] x1 + [3]
[0 0] [1]
Hurray, we answered YES(?,O(n^1))