Problem AG01 3.7

YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { half(0()) -> 0()
  , half(s(s(x))) -> s(half(x))
  , log(s(0())) -> 0()
  , log(s(s(x))) -> s(log(s(half(x)))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following argument positions are usable:
  Uargs(half) = {}, Uargs(s) = {1}, Uargs(log) = {1}

TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).

  [half](x1) = [1] x1 + [1]
                           
         [0] = [0]
                  
     [s](x1) = [1] x1 + [2]
                           
   [log](x1) = [3] x1 + [3]

This order satisfies following ordering constraints

      [half(0())] = [1]                 
                  > [0]                 
                  = [0()]               
                                        
  [half(s(s(x)))] = [1] x + [5]         
                  > [1] x + [3]         
                  = [s(half(x))]        
                                        
    [log(s(0()))] = [9]                 
                  > [0]                 
                  = [0()]               
                                        
   [log(s(s(x)))] = [3] x + [15]        
                  > [3] x + [14]        
                  = [s(log(s(half(x))))]
                                        

Hurray, we answered YES(?,O(n^1))

MAYBE

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

Strict Trs:
  { half(0()) -> 0()
  , half(s(s(x))) -> s(half(x))
  , log(s(0())) -> 0()
  , log(s(s(x))) -> s(log(s(half(x)))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

YES(?,PRIMREC)

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

Strict Trs:
  { half(0()) -> 0()
  , half(s(s(x))) -> s(half(x))
  , log(s(0())) -> 0()
  , log(s(s(x))) -> s(log(s(half(x)))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

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

 s > half, log > s .

Hurray, we answered YES(?,PRIMREC)

MAYBE

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

Strict Trs:
  { half(0()) -> 0()
  , half(s(s(x))) -> s(half(x))
  , log(s(0())) -> 0()
  , log(s(s(x))) -> s(log(s(half(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:
  { half(0()) -> 0()
  , half(s(s(x))) -> s(half(x))
  , log(s(0())) -> 0()
  , log(s(s(x))) -> s(log(s(half(x)))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..