LMPO
| Execution Time (secs) | 0.106 |
| Answer | YES(?,ELEMENTARY) |
| Input | SK90 4.16 |
YES(?,ELEMENTARY)
We consider the following Problem:
Strict Trs:
{ f(0()) -> s(0())
, f(s(0())) -> s(s(0()))
, f(s(0())) -> *(s(s(0())), f(0()))
, f(+(x, s(0()))) -> +(s(s(0())), f(x))
, f(+(x, y)) -> *(f(x), f(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,ELEMENTARY)
Proof:
The input was oriented with the instance of
Lightweight Multiset Path Order () as induced by the safe mapping
safe(f) = {}, safe(0) = {}, safe(s) = {1}, safe(*) = {1, 2},
safe(+) = {1, 2}
and precedence
empty .
Following symbols are considered recursive:
{f}
The recursion depth is 1 .
For your convenience, here are the oriented rules in predicative
notation (possibly applying argument filtering):
Strict DPs: {}
Weak DPs : {}
Strict Trs:
{ f(0();) -> s(; 0())
, f(s(; 0());) -> s(; s(; 0()))
, f(s(; 0());) -> *(; s(; s(; 0())), f(0();))
, f(+(; x, s(; 0()));) -> +(; s(; s(; 0())), f(x;))
, f(+(; x, y);) -> *(; f(x;), f(y;))}
Weak Trs : {}
Hurray, we answered YES(?,ELEMENTARY)
MPO
| Execution Time (secs) | 0.084 |
| Answer | YES(?,PRIMREC) |
| Input | SK90 4.16 |
YES(?,PRIMREC)
We consider the following Problem:
Strict Trs:
{ f(0()) -> s(0())
, f(s(0())) -> s(s(0()))
, f(s(0())) -> *(s(s(0())), f(0()))
, f(+(x, s(0()))) -> +(s(s(0())), f(x))
, f(+(x, y)) -> *(f(x), f(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,PRIMREC)
Proof:
The input was oriented with the instance of
'multiset path orders' as induced by the precedence
f > s, f > *, f > + .
Hurray, we answered YES(?,PRIMREC)
POP*
| Execution Time (secs) | 0.071 |
| Answer | MAYBE |
| Input | SK90 4.16 |
MAYBE
We consider the following Problem:
Strict Trs:
{ f(0()) -> s(0())
, f(s(0())) -> s(s(0()))
, f(s(0())) -> *(s(s(0())), f(0()))
, f(+(x, s(0()))) -> +(s(s(0())), f(x))
, f(+(x, y)) -> *(f(x), f(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP* (PS)
| Execution Time (secs) | 0.065 |
| Answer | MAYBE |
| Input | SK90 4.16 |
MAYBE
We consider the following Problem:
Strict Trs:
{ f(0()) -> s(0())
, f(s(0())) -> s(s(0()))
, f(s(0())) -> *(s(s(0())), f(0()))
, f(+(x, s(0()))) -> +(s(s(0())), f(x))
, f(+(x, y)) -> *(f(x), f(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP*
| Execution Time (secs) | 0.051 |
| Answer | MAYBE |
| Input | SK90 4.16 |
MAYBE
We consider the following Problem:
Strict Trs:
{ f(0()) -> s(0())
, f(s(0())) -> s(s(0()))
, f(s(0())) -> *(s(s(0())), f(0()))
, f(+(x, s(0()))) -> +(s(s(0())), f(x))
, f(+(x, y)) -> *(f(x), f(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP* (PS)
| Execution Time (secs) | 0.055 |
| Answer | MAYBE |
| Input | SK90 4.16 |
MAYBE
We consider the following Problem:
Strict Trs:
{ f(0()) -> s(0())
, f(s(0())) -> s(s(0()))
, f(s(0())) -> *(s(s(0())), f(0()))
, f(+(x, s(0()))) -> +(s(s(0())), f(x))
, f(+(x, y)) -> *(f(x), f(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..