Problem SK90 4.29

YES(?,O(n^1))

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

Strict Trs:
  { merge(x, nil()) -> x
  , merge(nil(), y) -> y
  , merge(++(x, y), ++(u(), v())) -> ++(x, merge(y, ++(u(), v())))
  , merge(++(x, y), ++(u(), v())) -> ++(u(), merge(++(x, y), v())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following argument positions are usable:
  Uargs(merge) = {}, Uargs(++) = {2}

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

  [merge](x1, x2) = [3] x1 + [2] x2 + [1]
                                         
            [nil] = [0]
                       
     [++](x1, x2) = [1] x2 + [2]
                                
              [u] = [0]
                       
              [v] = [0]

This order satisfies following ordering constraints

                [merge(x, nil())] = [3] x + [1]                    
                                  > [1] x + [0]                    
                                  = [x]                            
                                                                   
                [merge(nil(), y)] = [2] y + [1]                    
                                  > [1] y + [0]                    
                                  = [y]                            
                                                                   
  [merge(++(x, y), ++(u(), v()))] = [3] y + [11]                   
                                  > [3] y + [7]                    
                                  = [++(x, merge(y, ++(u(), v())))]
                                                                   
  [merge(++(x, y), ++(u(), v()))] = [3] y + [11]                   
                                  > [3] y + [9]                    
                                  = [++(u(), merge(++(x, y), v()))]
                                                                   

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

YES(?,ELEMENTARY)

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

Strict Trs:
  { merge(x, nil()) -> x
  , merge(nil(), y) -> y
  , merge(++(x, y), ++(u(), v())) -> ++(x, merge(y, ++(u(), v())))
  , merge(++(x, y), ++(u(), v())) -> ++(u(), merge(++(x, y), v())) }
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(merge) = {}, safe(nil) = {}, safe(++) = {1, 2}, safe(u) = {},
 safe(v) = {}

and precedence

 empty .

Following symbols are considered recursive:

 {merge}

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:
   { merge(x,  nil();) -> x
   , merge(nil(),  y;) -> y
   , merge(++(; x,  y),  ++(; u(),  v());) ->
     ++(; x,  merge(y,  ++(; u(),  v());))
   , merge(++(; x,  y),  ++(; u(),  v());) ->
     ++(; u(),  merge(++(; x,  y),  v();)) }
 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:
  { merge(x, nil()) -> x
  , merge(nil(), y) -> y
  , merge(++(x, y), ++(u(), v())) -> ++(x, merge(y, ++(u(), v())))
  , merge(++(x, y), ++(u(), v())) -> ++(u(), merge(++(x, y), v())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,PRIMREC)

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

 merge > ++ .

Hurray, we answered YES(?,PRIMREC)

YES(?,POLY)

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

Strict Trs:
  { merge(x, nil()) -> x
  , merge(nil(), y) -> y
  , merge(++(x, y), ++(u(), v())) -> ++(x, merge(y, ++(u(), v())))
  , merge(++(x, y), ++(u(), v())) -> ++(u(), merge(++(x, y), v())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,POLY)

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

 safe(merge) = {}, safe(nil) = {}, safe(++) = {1, 2}, safe(u) = {},
 safe(v) = {}

and precedence

 empty .

Following symbols are considered recursive:

 {merge}

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:
   { merge(x,  nil();) -> x
   , merge(nil(),  y;) -> y
   , merge(++(; x,  y),  ++(; u(),  v());) ->
     ++(; x,  merge(y,  ++(; u(),  v());))
   , merge(++(; x,  y),  ++(; u(),  v());) ->
     ++(; u(),  merge(++(; x,  y),  v();)) }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)

YES(?,POLY)

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

Strict Trs:
  { merge(x, nil()) -> x
  , merge(nil(), y) -> y
  , merge(++(x, y), ++(u(), v())) -> ++(x, merge(y, ++(u(), v())))
  , merge(++(x, y), ++(u(), v())) -> ++(u(), merge(++(x, y), v())) }
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(merge) = {}, safe(nil) = {}, safe(++) = {1, 2}, safe(u) = {},
 safe(v) = {}

and precedence

 empty .

Following symbols are considered recursive:

 {merge}

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:
   { merge(x,  nil();) -> x
   , merge(nil(),  y;) -> y
   , merge(++(; x,  y),  ++(; u(),  v());) ->
     ++(; x,  merge(y,  ++(; u(),  v());))
   , merge(++(; x,  y),  ++(; u(),  v());) ->
     ++(; u(),  merge(++(; x,  y),  v();)) }
 Weak Trs  : 

Hurray, we answered YES(?,POLY)