MAYBE

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

Strict Trs:
  { null(nil()) -> true()
  , null(add(n, x)) -> false()
  , tail(nil()) -> nil()
  , tail(add(n, x)) -> x
  , head(add(n, x)) -> n
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(x) -> shuff(x, nil())
  , shuff(x, y) -> if(null(x), x, y, app(y, add(head(x), nil())))
  , if(true(), x, y, z) -> y
  , if(false(), x, y, z) -> shuff(reverse(tail(x)), z) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { null^#(nil()) -> c_1()
  , null^#(add(n, x)) -> c_2()
  , tail^#(nil()) -> c_3()
  , tail^#(add(n, x)) -> c_4()
  , head^#(add(n, x)) -> c_5()
  , app^#(nil(), y) -> c_6()
  , app^#(add(n, x), y) -> c_7(app^#(x, y))
  , reverse^#(nil()) -> c_8()
  , reverse^#(add(n, x)) ->
    c_9(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(x) -> c_10(shuff^#(x, nil()))
  , shuff^#(x, y) ->
    c_11(if^#(null(x), x, y, app(y, add(head(x), nil()))),
         null^#(x),
         app^#(y, add(head(x), nil())),
         head^#(x))
  , if^#(true(), x, y, z) -> c_12()
  , if^#(false(), x, y, z) ->
    c_13(shuff^#(reverse(tail(x)), z), reverse^#(tail(x)), tail^#(x)) }

and mark the set of starting terms.

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

Strict DPs:
  { null^#(nil()) -> c_1()
  , null^#(add(n, x)) -> c_2()
  , tail^#(nil()) -> c_3()
  , tail^#(add(n, x)) -> c_4()
  , head^#(add(n, x)) -> c_5()
  , app^#(nil(), y) -> c_6()
  , app^#(add(n, x), y) -> c_7(app^#(x, y))
  , reverse^#(nil()) -> c_8()
  , reverse^#(add(n, x)) ->
    c_9(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(x) -> c_10(shuff^#(x, nil()))
  , shuff^#(x, y) ->
    c_11(if^#(null(x), x, y, app(y, add(head(x), nil()))),
         null^#(x),
         app^#(y, add(head(x), nil())),
         head^#(x))
  , if^#(true(), x, y, z) -> c_12()
  , if^#(false(), x, y, z) ->
    c_13(shuff^#(reverse(tail(x)), z), reverse^#(tail(x)), tail^#(x)) }
Weak Trs:
  { null(nil()) -> true()
  , null(add(n, x)) -> false()
  , tail(nil()) -> nil()
  , tail(add(n, x)) -> x
  , head(add(n, x)) -> n
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(x) -> shuff(x, nil())
  , shuff(x, y) -> if(null(x), x, y, app(y, add(head(x), nil())))
  , if(true(), x, y, z) -> y
  , if(false(), x, y, z) -> shuff(reverse(tail(x)), z) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {1,2,3,4,5,6,8,12} by
applications of Pre({1,2,3,4,5,6,8,12}) = {7,9,11,13}. Here rules
are labeled as follows:

  DPs:
    { 1: null^#(nil()) -> c_1()
    , 2: null^#(add(n, x)) -> c_2()
    , 3: tail^#(nil()) -> c_3()
    , 4: tail^#(add(n, x)) -> c_4()
    , 5: head^#(add(n, x)) -> c_5()
    , 6: app^#(nil(), y) -> c_6()
    , 7: app^#(add(n, x), y) -> c_7(app^#(x, y))
    , 8: reverse^#(nil()) -> c_8()
    , 9: reverse^#(add(n, x)) ->
         c_9(app^#(reverse(x), add(n, nil())), reverse^#(x))
    , 10: shuffle^#(x) -> c_10(shuff^#(x, nil()))
    , 11: shuff^#(x, y) ->
          c_11(if^#(null(x), x, y, app(y, add(head(x), nil()))),
               null^#(x),
               app^#(y, add(head(x), nil())),
               head^#(x))
    , 12: if^#(true(), x, y, z) -> c_12()
    , 13: if^#(false(), x, y, z) ->
          c_13(shuff^#(reverse(tail(x)), z), reverse^#(tail(x)), tail^#(x)) }

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

Strict DPs:
  { app^#(add(n, x), y) -> c_7(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_9(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(x) -> c_10(shuff^#(x, nil()))
  , shuff^#(x, y) ->
    c_11(if^#(null(x), x, y, app(y, add(head(x), nil()))),
         null^#(x),
         app^#(y, add(head(x), nil())),
         head^#(x))
  , if^#(false(), x, y, z) ->
    c_13(shuff^#(reverse(tail(x)), z), reverse^#(tail(x)), tail^#(x)) }
Weak DPs:
  { null^#(nil()) -> c_1()
  , null^#(add(n, x)) -> c_2()
  , tail^#(nil()) -> c_3()
  , tail^#(add(n, x)) -> c_4()
  , head^#(add(n, x)) -> c_5()
  , app^#(nil(), y) -> c_6()
  , reverse^#(nil()) -> c_8()
  , if^#(true(), x, y, z) -> c_12() }
Weak Trs:
  { null(nil()) -> true()
  , null(add(n, x)) -> false()
  , tail(nil()) -> nil()
  , tail(add(n, x)) -> x
  , head(add(n, x)) -> n
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(x) -> shuff(x, nil())
  , shuff(x, y) -> if(null(x), x, y, app(y, add(head(x), nil())))
  , if(true(), x, y, z) -> y
  , if(false(), x, y, z) -> shuff(reverse(tail(x)), z) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ null^#(nil()) -> c_1()
, null^#(add(n, x)) -> c_2()
, tail^#(nil()) -> c_3()
, tail^#(add(n, x)) -> c_4()
, head^#(add(n, x)) -> c_5()
, app^#(nil(), y) -> c_6()
, reverse^#(nil()) -> c_8()
, if^#(true(), x, y, z) -> c_12() }

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

Strict DPs:
  { app^#(add(n, x), y) -> c_7(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_9(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(x) -> c_10(shuff^#(x, nil()))
  , shuff^#(x, y) ->
    c_11(if^#(null(x), x, y, app(y, add(head(x), nil()))),
         null^#(x),
         app^#(y, add(head(x), nil())),
         head^#(x))
  , if^#(false(), x, y, z) ->
    c_13(shuff^#(reverse(tail(x)), z), reverse^#(tail(x)), tail^#(x)) }
Weak Trs:
  { null(nil()) -> true()
  , null(add(n, x)) -> false()
  , tail(nil()) -> nil()
  , tail(add(n, x)) -> x
  , head(add(n, x)) -> n
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(x) -> shuff(x, nil())
  , shuff(x, y) -> if(null(x), x, y, app(y, add(head(x), nil())))
  , if(true(), x, y, z) -> y
  , if(false(), x, y, z) -> shuff(reverse(tail(x)), z) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { shuff^#(x, y) ->
    c_11(if^#(null(x), x, y, app(y, add(head(x), nil()))),
         null^#(x),
         app^#(y, add(head(x), nil())),
         head^#(x))
  , if^#(false(), x, y, z) ->
    c_13(shuff^#(reverse(tail(x)), z), reverse^#(tail(x)), tail^#(x)) }

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

Strict DPs:
  { app^#(add(n, x), y) -> c_1(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_2(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(x) -> c_3(shuff^#(x, nil()))
  , shuff^#(x, y) ->
    c_4(if^#(null(x), x, y, app(y, add(head(x), nil()))),
        app^#(y, add(head(x), nil())))
  , if^#(false(), x, y, z) ->
    c_5(shuff^#(reverse(tail(x)), z), reverse^#(tail(x))) }
Weak Trs:
  { null(nil()) -> true()
  , null(add(n, x)) -> false()
  , tail(nil()) -> nil()
  , tail(add(n, x)) -> x
  , head(add(n, x)) -> n
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(x) -> shuff(x, nil())
  , shuff(x, y) -> if(null(x), x, y, app(y, add(head(x), nil())))
  , if(true(), x, y, z) -> y
  , if(false(), x, y, z) -> shuff(reverse(tail(x)), z) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { null(nil()) -> true()
    , null(add(n, x)) -> false()
    , tail(nil()) -> nil()
    , tail(add(n, x)) -> x
    , head(add(n, x)) -> n
    , app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }

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

Strict DPs:
  { app^#(add(n, x), y) -> c_1(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_2(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(x) -> c_3(shuff^#(x, nil()))
  , shuff^#(x, y) ->
    c_4(if^#(null(x), x, y, app(y, add(head(x), nil()))),
        app^#(y, add(head(x), nil())))
  , if^#(false(), x, y, z) ->
    c_5(shuff^#(reverse(tail(x)), z), reverse^#(tail(x))) }
Weak Trs:
  { null(nil()) -> true()
  , null(add(n, x)) -> false()
  , tail(nil()) -> nil()
  , tail(add(n, x)) -> x
  , head(add(n, x)) -> n
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: app^#(add(n, x), y) -> c_1(app^#(x, y))
     -->_1 app^#(add(n, x), y) -> c_1(app^#(x, y)) :1
  
  2: reverse^#(add(n, x)) ->
     c_2(app^#(reverse(x), add(n, nil())), reverse^#(x))
     -->_2 reverse^#(add(n, x)) ->
           c_2(app^#(reverse(x), add(n, nil())), reverse^#(x)) :2
     -->_1 app^#(add(n, x), y) -> c_1(app^#(x, y)) :1
  
  3: shuffle^#(x) -> c_3(shuff^#(x, nil()))
     -->_1 shuff^#(x, y) ->
           c_4(if^#(null(x), x, y, app(y, add(head(x), nil()))),
               app^#(y, add(head(x), nil()))) :4
  
  4: shuff^#(x, y) ->
     c_4(if^#(null(x), x, y, app(y, add(head(x), nil()))),
         app^#(y, add(head(x), nil())))
     -->_1 if^#(false(), x, y, z) ->
           c_5(shuff^#(reverse(tail(x)), z), reverse^#(tail(x))) :5
     -->_2 app^#(add(n, x), y) -> c_1(app^#(x, y)) :1
  
  5: if^#(false(), x, y, z) ->
     c_5(shuff^#(reverse(tail(x)), z), reverse^#(tail(x)))
     -->_1 shuff^#(x, y) ->
           c_4(if^#(null(x), x, y, app(y, add(head(x), nil()))),
               app^#(y, add(head(x), nil()))) :4
     -->_2 reverse^#(add(n, x)) ->
           c_2(app^#(reverse(x), add(n, nil())), reverse^#(x)) :2
  

Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).

  { shuffle^#(x) -> c_3(shuff^#(x, nil())) }


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

Strict DPs:
  { app^#(add(n, x), y) -> c_1(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_2(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuff^#(x, y) ->
    c_4(if^#(null(x), x, y, app(y, add(head(x), nil()))),
        app^#(y, add(head(x), nil())))
  , if^#(false(), x, y, z) ->
    c_5(shuff^#(reverse(tail(x)), z), reverse^#(tail(x))) }
Weak Trs:
  { null(nil()) -> true()
  , null(add(n, x)) -> false()
  , tail(nil()) -> nil()
  , tail(add(n, x)) -> x
  , head(add(n, x)) -> n
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..