LMPO
| Execution Time (secs) | 0.045 |
| Answer | MAYBE |
| Input | SK90 2.16 |
MAYBE
We consider the following Problem:
Strict Trs:
{ f(0()) -> 1()
, f(s(x)) -> g(x, s(x))
, g(0(), y) -> y
, g(s(x), y) -> g(x, +(y, s(x)))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, g(s(x), y) -> g(x, s(+(y, x)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
| Execution Time (secs) | 0.047 |
| Answer | MAYBE |
| Input | SK90 2.16 |
MAYBE
We consider the following Problem:
Strict Trs:
{ f(0()) -> 1()
, f(s(x)) -> g(x, s(x))
, g(0(), y) -> y
, g(s(x), y) -> g(x, +(y, s(x)))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, g(s(x), y) -> g(x, s(+(y, x)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP*
| Execution Time (secs) | 0.040 |
| Answer | MAYBE |
| Input | SK90 2.16 |
MAYBE
We consider the following Problem:
Strict Trs:
{ f(0()) -> 1()
, f(s(x)) -> g(x, s(x))
, g(0(), y) -> y
, g(s(x), y) -> g(x, +(y, s(x)))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, g(s(x), y) -> g(x, s(+(y, x)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP* (PS)
| Execution Time (secs) | 0.059 |
| Answer | YES(?,POLY) |
| Input | SK90 2.16 |
YES(?,POLY)
We consider the following Problem:
Strict Trs:
{ f(0()) -> 1()
, f(s(x)) -> g(x, s(x))
, g(0(), y) -> y
, g(s(x), y) -> g(x, +(y, s(x)))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, g(s(x), y) -> g(x, s(+(y, x)))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,POLY)
Proof:
The input was oriented with the instance of
Polynomial Path Order (PS) as induced by the safe mapping
safe(f) = {}, safe(0) = {}, safe(1) = {}, safe(s) = {1},
safe(g) = {2}, safe(+) = {1}
and precedence
g > +, f ~ g .
Following symbols are considered recursive:
{f, g, +}
The recursion depth is 2 .
For your convenience, here are the oriented rules in predicative
notation (possibly applying argument filtering):
Strict DPs: {}
Weak DPs : {}
Strict Trs:
{ f(0();) -> 1()
, f(s(; x);) -> g(x; s(; x))
, g(0(); y) -> y
, g(s(; x); y) -> g(x; +(s(; x); y))
, +(0(); x) -> x
, +(s(; y); x) -> s(; +(y; x))
, g(s(; x); y) -> g(x; s(; +(x; y)))}
Weak Trs : {}
Hurray, we answered YES(?,POLY)
Small POP*
| Execution Time (secs) | 0.040 |
| Answer | MAYBE |
| Input | SK90 2.16 |
MAYBE
We consider the following Problem:
Strict Trs:
{ f(0()) -> 1()
, f(s(x)) -> g(x, s(x))
, g(0(), y) -> y
, g(s(x), y) -> g(x, +(y, s(x)))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, g(s(x), y) -> g(x, s(+(y, x)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP* (PS)
| Execution Time (secs) | 0.117 |
| Answer | YES(?,O(n^2)) |
| Input | SK90 2.16 |
YES(?,O(n^2))
We consider the following Problem:
Strict Trs:
{ f(0()) -> 1()
, f(s(x)) -> g(x, s(x))
, g(0(), y) -> y
, g(s(x), y) -> g(x, +(y, s(x)))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, g(s(x), y) -> g(x, s(+(y, x)))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The input was oriented with the instance of
Small Polynomial Path Order (WSC,
PS) as induced by the safe mapping
safe(f) = {}, safe(0) = {}, safe(1) = {}, safe(s) = {1},
safe(g) = {2}, safe(+) = {1}
and precedence
g > +, f ~ g .
Following symbols are considered recursive:
{f, g, +}
The recursion depth is 2 .
For your convenience, here are the oriented rules in predicative
notation (possibly applying argument filtering):
Strict DPs: {}
Weak DPs : {}
Strict Trs:
{ f(0();) -> 1()
, f(s(; x);) -> g(x; s(; x))
, g(0(); y) -> y
, g(s(; x); y) -> g(x; +(s(; x); y))
, +(0(); x) -> x
, +(s(; y); x) -> s(; +(y; x))
, g(s(; x); y) -> g(x; s(; +(x; y)))}
Weak Trs : {}
Hurray, we answered YES(?,O(n^2))