Problem TCT 09 ma3

YES(?,O(n^1))

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

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

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

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

          [p](x1) = [1] x1 + [1]
                                
              [0] = [0]
                       
          [s](x1) = [1] x1 + [3]
                                
  [minus](x1, x2) = [2] x1 + [1] x2 + [1]

This order satisfies following ordering constraints

          [p(0())] = [1]                
                   > [0]                
                   = [0()]              
                                        
         [p(s(x))] = [1] x + [4]        
                   > [1] x + [0]        
                   = [x]                
                                        
   [minus(x, 0())] = [2] x + [1]        
                   > [1] x + [0]        
                   = [x]                
                                        
  [minus(x, s(y))] = [2] x + [1] y + [4]
                   > [2] x + [1] y + [3]
                   = [minus(p(x), y)]   
                                        

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

MAYBE

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

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

The input cannot be shown compatible

Arrrr..

YES(?,POLY)

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

Strict Trs:
  { p(0()) -> 0()
  , p(s(x)) -> x
  , minus(x, 0()) -> x
  , minus(x, s(y)) -> minus(p(x), y) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,POLY)

The input was oriented with the instance of 'Polynomial Path Order
(PS)' as induced by the safe mapping

 safe(p) = {1}, safe(0) = {}, safe(s) = {1}, safe(minus) = {1}

and precedence

 minus > p .

Following symbols are considered recursive:

 {p, minus}

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:
   { p(; 0()) -> 0()
   , p(; s(; x)) -> x
   , minus(0(); x) -> x
   , minus(s(; y); x) -> minus(y; p(; x)) }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)