Problem SK90 2.15

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { f(0()) -> 1()
  , f(s(x)) -> g(f(x))
  , f(s(x)) -> +(f(x), s(f(x)))
  , g(x) -> +(x, s(x)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'matrix interpretation of dimension 3' failed due to the
   following reason:
   
   The input cannot be shown compatible

2) 'custom shape polynomial interpretation' failed due to the
   following reason:
   
   The input cannot be shown compatible

3) 'custom shape polynomial interpretation' failed due to the
   following reason:
   
   The input cannot be shown compatible

4) 'matrix interpretation of dimension 1' failed due to the
   following reason:
   
   The input cannot be shown compatible


Arrrr..

YES(?,ELEMENTARY)

We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).

Strict Trs:
  { f(0()) -> 1()
  , f(s(x)) -> g(f(x))
  , g(x) -> +(x, s(x))
  , f(s(x)) -> +(f(x), s(f(x))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,ELEMENTARY)

The input was oriented with the instance of 'Lightweight Multiset
Path Order' as induced by the safe mapping

 safe(f) = {}, safe(0) = {}, safe(1) = {}, safe(s) = {1},
 safe(g) = {1}, safe(+) = {1, 2}

and precedence

 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(; f(x;))
   , g(; x) -> +(; x,  s(; x))
   , f(s(; x);) -> +(; f(x;),  s(; f(x;))) }
 Weak Trs  : 

Hurray, we answered YES(?,ELEMENTARY)

YES(?,PRIMREC)

We are left with following problem, upon which TcT provides the
certificate YES(?,PRIMREC).

Strict Trs:
  { f(0()) -> 1()
  , f(s(x)) -> g(f(x))
  , g(x) -> +(x, s(x))
  , f(s(x)) -> +(f(x), s(f(x))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

The input was oriented with the instance of'multiset path orders'
as induced by the precedence

 f > s, f > g, f > +, 0 > 1, g > s, g > + .

Hurray, we answered YES(?,PRIMREC)

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { f(0()) -> 1()
  , f(s(x)) -> g(f(x))
  , g(x) -> +(x, s(x))
  , f(s(x)) -> +(f(x), s(f(x))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { f(0()) -> 1()
  , f(s(x)) -> g(f(x))
  , g(x) -> +(x, s(x))
  , f(s(x)) -> +(f(x), s(f(x))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..