Tool Bounds
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ f(X, X) -> c(X)
, f(X, c(X)) -> f(s(X), X)
, f(s(X), X) -> f(X, a(X))}
StartTerms: all
Strategy: none
Certificate: MAYBE
Proof:
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 CDI
stdout:
YES(?,O(n^2))
QUADRATIC upper bound on the derivational complexity
This TRS is terminating using the deltarestricted interpretation
c(delta, X0) = + 0*X0 + 3 + 2*X0*delta + 0*delta
s(delta, X0) = + 0*X0 + 2 + 2*X0*delta + 0*delta
a(delta, X0) = + 1*X0 + 0 + 0*X0*delta + 0*delta
f(delta, X1, X0) = + 0*X0 + 0*X1 + 3 + 2*X0*delta + 2*X1*delta + 2*delta
c_tau_1(delta) = delta/(0 + 2 * delta)
s_tau_1(delta) = delta/(0 + 2 * delta)
a_tau_1(delta) = delta/(1 + 0 * delta)
f_tau_1(delta) = delta/(0 + 2 * delta)
f_tau_2(delta) = delta/(0 + 2 * delta)
Time: 0.143764 seconds
Statistics:
Number of monomials: 210
Last formula building started for bound 3
Last SAT solving started for bound 3Tool EDA
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(X, X) -> c(X)
, f(X, c(X)) -> f(s(X), X)
, f(s(X), X) -> f(X, a(X))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
We have the following EDA-non-satisfying matrix interpretation:
Interpretation Functions:
s(x1) = [1] x1 + [1]
f(x1, x2) = [1] x1 + [1] x2 + [3]
a(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [2]
Hurray, we answered YES(?,O(n^1))Tool IDA
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(X, X) -> c(X)
, f(X, c(X)) -> f(s(X), X)
, f(s(X), X) -> f(X, a(X))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
s(x1) = [1] x1 + [1]
f(x1, x2) = [1] x1 + [1] x2 + [3]
a(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [2]
Hurray, we answered YES(?,O(n^1))Tool TRI
| Execution Time | 8.7790966e-2ms |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | Rubio 04 koen |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(X, X) -> c(X)
, f(X, c(X)) -> f(s(X), X)
, f(s(X), X) -> f(X, a(X))}
StartTerms: all
Strategy: none
Certificate: YES(?,O(n^1))
Proof:
We have the following triangular matrix interpretation:
Interpretation Functions:
s(x1) = [1] x1 + [1]
f(x1, x2) = [1] x1 + [1] x2 + [3]
a(x1) = [1] x1 + [0]
c(x1) = [1] x1 + [2]
Hurray, we answered YES(?,O(n^1))Tool TRI2
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(X, X) -> c(X)
, f(X, c(X)) -> f(s(X), X)
, f(s(X), X) -> f(X, a(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] [3]
f(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 0] [0 0] [0]
a(x1) = [1 0] x1 + [0]
[0 1] [3]
c(x1) = [1 0] x1 + [2]
[0 0] [0]
Hurray, we answered YES(?,O(n^1))