Problem SK90 2.43

TIMEOUT

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

Strict Trs:
  { merge(x, nil()) -> x
  , merge(nil(), y) -> y
  , merge(.(x, y), .(u, v)) ->
    if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
  , if(true(), x, y) -> x
  , if(false(), x, y) -> x
  , ++(nil(), y) -> y
  , ++(.(x, y), z) -> .(x, ++(y, z)) }
Obligation:
  innermost runtime complexity
Answer:
  TIMEOUT

Computation stopped due to timeout after 20.0 seconds.

Arrrr..

YES(?,ELEMENTARY)

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

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

and precedence

 merge > if .

Following symbols are considered recursive:

 {merge, if, ++}

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

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

 merge > ., merge > if, merge > <, ++ > ., . ~ if .

Hurray, we answered YES(?,PRIMREC)

MAYBE

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

Strict Trs:
  { merge(nil(), y) -> y
  , merge(x, nil()) -> x
  , merge(.(x, y), .(u, v)) ->
    if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
  , ++(nil(), y) -> y
  , ++(.(x, y), z) -> .(x, ++(y, z))
  , if(true(), x, y) -> x
  , if(false(), x, y) -> 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:
  { merge(nil(), y) -> y
  , merge(x, nil()) -> x
  , merge(.(x, y), .(u, v)) ->
    if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
  , ++(nil(), y) -> y
  , ++(.(x, y), z) -> .(x, ++(y, z))
  , if(true(), x, y) -> x
  , if(false(), x, y) -> x }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..