MAYBE

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

Strict Trs:
  { div(x, y) -> div2(x, y, 0())
  , div2(x, y, i) ->
    if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i))
  , if1(true(), b, x, y, i, j) -> divZeroError()
  , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j)
  , le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , plus(x, y) -> plusIter(x, y, 0())
  , inc(0()) -> 0()
  , inc(s(i)) -> s(inc(i))
  , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j)
  , if2(false(), x, y, i, j) -> i
  , minus(x, 0()) -> x
  , minus(0(), y) -> 0()
  , minus(s(x), s(y)) -> minus(x, y)
  , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z)
  , ifPlus(true(), x, y, z) -> y
  , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z))
  , a() -> c()
  , a() -> d() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { div^#(x, y) -> c_1(div2^#(x, y, 0()))
  , div2^#(x, y, i) ->
    c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
        le^#(y, 0()),
        le^#(y, x),
        plus^#(i, 0()),
        inc^#(i))
  , if1^#(true(), b, x, y, i, j) -> c_3()
  , if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j))
  , le^#(0(), y) -> c_5()
  , le^#(s(x), 0()) -> c_6()
  , le^#(s(x), s(y)) -> c_7(le^#(x, y))
  , plus^#(x, y) -> c_8(plusIter^#(x, y, 0()))
  , inc^#(0()) -> c_9()
  , inc^#(s(i)) -> c_10(inc^#(i))
  , if2^#(true(), x, y, i, j) ->
    c_11(div2^#(minus(x, y), y, j), minus^#(x, y))
  , if2^#(false(), x, y, i, j) -> c_12()
  , plusIter^#(x, y, z) ->
    c_16(ifPlus^#(le(x, z), x, y, z), le^#(x, z))
  , minus^#(x, 0()) -> c_13()
  , minus^#(0(), y) -> c_14()
  , minus^#(s(x), s(y)) -> c_15(minus^#(x, y))
  , ifPlus^#(true(), x, y, z) -> c_17()
  , ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z)))
  , a^#() -> c_19()
  , a^#() -> c_20() }

and mark the set of starting terms.

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

Strict DPs:
  { div^#(x, y) -> c_1(div2^#(x, y, 0()))
  , div2^#(x, y, i) ->
    c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
        le^#(y, 0()),
        le^#(y, x),
        plus^#(i, 0()),
        inc^#(i))
  , if1^#(true(), b, x, y, i, j) -> c_3()
  , if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j))
  , le^#(0(), y) -> c_5()
  , le^#(s(x), 0()) -> c_6()
  , le^#(s(x), s(y)) -> c_7(le^#(x, y))
  , plus^#(x, y) -> c_8(plusIter^#(x, y, 0()))
  , inc^#(0()) -> c_9()
  , inc^#(s(i)) -> c_10(inc^#(i))
  , if2^#(true(), x, y, i, j) ->
    c_11(div2^#(minus(x, y), y, j), minus^#(x, y))
  , if2^#(false(), x, y, i, j) -> c_12()
  , plusIter^#(x, y, z) ->
    c_16(ifPlus^#(le(x, z), x, y, z), le^#(x, z))
  , minus^#(x, 0()) -> c_13()
  , minus^#(0(), y) -> c_14()
  , minus^#(s(x), s(y)) -> c_15(minus^#(x, y))
  , ifPlus^#(true(), x, y, z) -> c_17()
  , ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z)))
  , a^#() -> c_19()
  , a^#() -> c_20() }
Weak Trs:
  { div(x, y) -> div2(x, y, 0())
  , div2(x, y, i) ->
    if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i))
  , if1(true(), b, x, y, i, j) -> divZeroError()
  , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j)
  , le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , plus(x, y) -> plusIter(x, y, 0())
  , inc(0()) -> 0()
  , inc(s(i)) -> s(inc(i))
  , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j)
  , if2(false(), x, y, i, j) -> i
  , minus(x, 0()) -> x
  , minus(0(), y) -> 0()
  , minus(s(x), s(y)) -> minus(x, y)
  , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z)
  , ifPlus(true(), x, y, z) -> y
  , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z))
  , a() -> c()
  , a() -> d() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of
{3,5,6,9,12,14,15,17,19,20} by applications of
Pre({3,5,6,9,12,14,15,17,19,20}) = {2,4,7,10,11,13,16}. Here rules
are labeled as follows:

  DPs:
    { 1: div^#(x, y) -> c_1(div2^#(x, y, 0()))
    , 2: div2^#(x, y, i) ->
         c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
             le^#(y, 0()),
             le^#(y, x),
             plus^#(i, 0()),
             inc^#(i))
    , 3: if1^#(true(), b, x, y, i, j) -> c_3()
    , 4: if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j))
    , 5: le^#(0(), y) -> c_5()
    , 6: le^#(s(x), 0()) -> c_6()
    , 7: le^#(s(x), s(y)) -> c_7(le^#(x, y))
    , 8: plus^#(x, y) -> c_8(plusIter^#(x, y, 0()))
    , 9: inc^#(0()) -> c_9()
    , 10: inc^#(s(i)) -> c_10(inc^#(i))
    , 11: if2^#(true(), x, y, i, j) ->
          c_11(div2^#(minus(x, y), y, j), minus^#(x, y))
    , 12: if2^#(false(), x, y, i, j) -> c_12()
    , 13: plusIter^#(x, y, z) ->
          c_16(ifPlus^#(le(x, z), x, y, z), le^#(x, z))
    , 14: minus^#(x, 0()) -> c_13()
    , 15: minus^#(0(), y) -> c_14()
    , 16: minus^#(s(x), s(y)) -> c_15(minus^#(x, y))
    , 17: ifPlus^#(true(), x, y, z) -> c_17()
    , 18: ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z)))
    , 19: a^#() -> c_19()
    , 20: a^#() -> c_20() }

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

Strict DPs:
  { div^#(x, y) -> c_1(div2^#(x, y, 0()))
  , div2^#(x, y, i) ->
    c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
        le^#(y, 0()),
        le^#(y, x),
        plus^#(i, 0()),
        inc^#(i))
  , if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j))
  , le^#(s(x), s(y)) -> c_7(le^#(x, y))
  , plus^#(x, y) -> c_8(plusIter^#(x, y, 0()))
  , inc^#(s(i)) -> c_10(inc^#(i))
  , if2^#(true(), x, y, i, j) ->
    c_11(div2^#(minus(x, y), y, j), minus^#(x, y))
  , plusIter^#(x, y, z) ->
    c_16(ifPlus^#(le(x, z), x, y, z), le^#(x, z))
  , minus^#(s(x), s(y)) -> c_15(minus^#(x, y))
  , ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z))) }
Weak DPs:
  { if1^#(true(), b, x, y, i, j) -> c_3()
  , le^#(0(), y) -> c_5()
  , le^#(s(x), 0()) -> c_6()
  , inc^#(0()) -> c_9()
  , if2^#(false(), x, y, i, j) -> c_12()
  , minus^#(x, 0()) -> c_13()
  , minus^#(0(), y) -> c_14()
  , ifPlus^#(true(), x, y, z) -> c_17()
  , a^#() -> c_19()
  , a^#() -> c_20() }
Weak Trs:
  { div(x, y) -> div2(x, y, 0())
  , div2(x, y, i) ->
    if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i))
  , if1(true(), b, x, y, i, j) -> divZeroError()
  , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j)
  , le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , plus(x, y) -> plusIter(x, y, 0())
  , inc(0()) -> 0()
  , inc(s(i)) -> s(inc(i))
  , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j)
  , if2(false(), x, y, i, j) -> i
  , minus(x, 0()) -> x
  , minus(0(), y) -> 0()
  , minus(s(x), s(y)) -> minus(x, y)
  , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z)
  , ifPlus(true(), x, y, z) -> y
  , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z))
  , a() -> c()
  , a() -> d() }
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.

{ if1^#(true(), b, x, y, i, j) -> c_3()
, le^#(0(), y) -> c_5()
, le^#(s(x), 0()) -> c_6()
, inc^#(0()) -> c_9()
, if2^#(false(), x, y, i, j) -> c_12()
, minus^#(x, 0()) -> c_13()
, minus^#(0(), y) -> c_14()
, ifPlus^#(true(), x, y, z) -> c_17()
, a^#() -> c_19()
, a^#() -> c_20() }

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

Strict DPs:
  { div^#(x, y) -> c_1(div2^#(x, y, 0()))
  , div2^#(x, y, i) ->
    c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
        le^#(y, 0()),
        le^#(y, x),
        plus^#(i, 0()),
        inc^#(i))
  , if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j))
  , le^#(s(x), s(y)) -> c_7(le^#(x, y))
  , plus^#(x, y) -> c_8(plusIter^#(x, y, 0()))
  , inc^#(s(i)) -> c_10(inc^#(i))
  , if2^#(true(), x, y, i, j) ->
    c_11(div2^#(minus(x, y), y, j), minus^#(x, y))
  , plusIter^#(x, y, z) ->
    c_16(ifPlus^#(le(x, z), x, y, z), le^#(x, z))
  , minus^#(s(x), s(y)) -> c_15(minus^#(x, y))
  , ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z))) }
Weak Trs:
  { div(x, y) -> div2(x, y, 0())
  , div2(x, y, i) ->
    if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i))
  , if1(true(), b, x, y, i, j) -> divZeroError()
  , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j)
  , le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , plus(x, y) -> plusIter(x, y, 0())
  , inc(0()) -> 0()
  , inc(s(i)) -> s(inc(i))
  , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j)
  , if2(false(), x, y, i, j) -> i
  , minus(x, 0()) -> x
  , minus(0(), y) -> 0()
  , minus(s(x), s(y)) -> minus(x, y)
  , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z)
  , ifPlus(true(), x, y, z) -> y
  , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z))
  , a() -> c()
  , a() -> d() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { div2^#(x, y, i) ->
    c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
        le^#(y, 0()),
        le^#(y, x),
        plus^#(i, 0()),
        inc^#(i)) }

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

Strict DPs:
  { div^#(x, y) -> c_1(div2^#(x, y, 0()))
  , div2^#(x, y, i) ->
    c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
        le^#(y, x),
        plus^#(i, 0()),
        inc^#(i))
  , if1^#(false(), b, x, y, i, j) -> c_3(if2^#(b, x, y, i, j))
  , le^#(s(x), s(y)) -> c_4(le^#(x, y))
  , plus^#(x, y) -> c_5(plusIter^#(x, y, 0()))
  , inc^#(s(i)) -> c_6(inc^#(i))
  , if2^#(true(), x, y, i, j) ->
    c_7(div2^#(minus(x, y), y, j), minus^#(x, y))
  , plusIter^#(x, y, z) ->
    c_8(ifPlus^#(le(x, z), x, y, z), le^#(x, z))
  , minus^#(s(x), s(y)) -> c_9(minus^#(x, y))
  , ifPlus^#(false(), x, y, z) -> c_10(plusIter^#(x, s(y), s(z))) }
Weak Trs:
  { div(x, y) -> div2(x, y, 0())
  , div2(x, y, i) ->
    if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i))
  , if1(true(), b, x, y, i, j) -> divZeroError()
  , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j)
  , le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , plus(x, y) -> plusIter(x, y, 0())
  , inc(0()) -> 0()
  , inc(s(i)) -> s(inc(i))
  , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j)
  , if2(false(), x, y, i, j) -> i
  , minus(x, 0()) -> x
  , minus(0(), y) -> 0()
  , minus(s(x), s(y)) -> minus(x, y)
  , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z)
  , ifPlus(true(), x, y, z) -> y
  , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z))
  , a() -> c()
  , a() -> d() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { le(0(), y) -> true()
    , le(s(x), 0()) -> false()
    , le(s(x), s(y)) -> le(x, y)
    , plus(x, y) -> plusIter(x, y, 0())
    , inc(0()) -> 0()
    , inc(s(i)) -> s(inc(i))
    , minus(x, 0()) -> x
    , minus(0(), y) -> 0()
    , minus(s(x), s(y)) -> minus(x, y)
    , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z)
    , ifPlus(true(), x, y, z) -> y
    , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) }

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

Strict DPs:
  { div^#(x, y) -> c_1(div2^#(x, y, 0()))
  , div2^#(x, y, i) ->
    c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
        le^#(y, x),
        plus^#(i, 0()),
        inc^#(i))
  , if1^#(false(), b, x, y, i, j) -> c_3(if2^#(b, x, y, i, j))
  , le^#(s(x), s(y)) -> c_4(le^#(x, y))
  , plus^#(x, y) -> c_5(plusIter^#(x, y, 0()))
  , inc^#(s(i)) -> c_6(inc^#(i))
  , if2^#(true(), x, y, i, j) ->
    c_7(div2^#(minus(x, y), y, j), minus^#(x, y))
  , plusIter^#(x, y, z) ->
    c_8(ifPlus^#(le(x, z), x, y, z), le^#(x, z))
  , minus^#(s(x), s(y)) -> c_9(minus^#(x, y))
  , ifPlus^#(false(), x, y, z) -> c_10(plusIter^#(x, s(y), s(z))) }
Weak Trs:
  { le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , plus(x, y) -> plusIter(x, y, 0())
  , inc(0()) -> 0()
  , inc(s(i)) -> s(inc(i))
  , minus(x, 0()) -> x
  , minus(0(), y) -> 0()
  , minus(s(x), s(y)) -> minus(x, y)
  , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z)
  , ifPlus(true(), x, y, z) -> y
  , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: div^#(x, y) -> c_1(div2^#(x, y, 0()))
     -->_1 div2^#(x, y, i) ->
           c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
               le^#(y, x),
               plus^#(i, 0()),
               inc^#(i)) :2
  
  2: div2^#(x, y, i) ->
     c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
         le^#(y, x),
         plus^#(i, 0()),
         inc^#(i))
     -->_4 inc^#(s(i)) -> c_6(inc^#(i)) :6
     -->_3 plus^#(x, y) -> c_5(plusIter^#(x, y, 0())) :5
     -->_2 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4
     -->_1 if1^#(false(), b, x, y, i, j) -> c_3(if2^#(b, x, y, i, j)) :3
  
  3: if1^#(false(), b, x, y, i, j) -> c_3(if2^#(b, x, y, i, j))
     -->_1 if2^#(true(), x, y, i, j) ->
           c_7(div2^#(minus(x, y), y, j), minus^#(x, y)) :7
  
  4: le^#(s(x), s(y)) -> c_4(le^#(x, y))
     -->_1 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4
  
  5: plus^#(x, y) -> c_5(plusIter^#(x, y, 0()))
     -->_1 plusIter^#(x, y, z) ->
           c_8(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) :8
  
  6: inc^#(s(i)) -> c_6(inc^#(i))
     -->_1 inc^#(s(i)) -> c_6(inc^#(i)) :6
  
  7: if2^#(true(), x, y, i, j) ->
     c_7(div2^#(minus(x, y), y, j), minus^#(x, y))
     -->_2 minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) :9
     -->_1 div2^#(x, y, i) ->
           c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
               le^#(y, x),
               plus^#(i, 0()),
               inc^#(i)) :2
  
  8: plusIter^#(x, y, z) ->
     c_8(ifPlus^#(le(x, z), x, y, z), le^#(x, z))
     -->_1 ifPlus^#(false(), x, y, z) ->
           c_10(plusIter^#(x, s(y), s(z))) :10
     -->_2 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4
  
  9: minus^#(s(x), s(y)) -> c_9(minus^#(x, y))
     -->_1 minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) :9
  
  10: ifPlus^#(false(), x, y, z) -> c_10(plusIter^#(x, s(y), s(z)))
     -->_1 plusIter^#(x, y, z) ->
           c_8(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) :8
  

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).

  { div^#(x, y) -> c_1(div2^#(x, y, 0())) }


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

Strict DPs:
  { div2^#(x, y, i) ->
    c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
        le^#(y, x),
        plus^#(i, 0()),
        inc^#(i))
  , if1^#(false(), b, x, y, i, j) -> c_3(if2^#(b, x, y, i, j))
  , le^#(s(x), s(y)) -> c_4(le^#(x, y))
  , plus^#(x, y) -> c_5(plusIter^#(x, y, 0()))
  , inc^#(s(i)) -> c_6(inc^#(i))
  , if2^#(true(), x, y, i, j) ->
    c_7(div2^#(minus(x, y), y, j), minus^#(x, y))
  , plusIter^#(x, y, z) ->
    c_8(ifPlus^#(le(x, z), x, y, z), le^#(x, z))
  , minus^#(s(x), s(y)) -> c_9(minus^#(x, y))
  , ifPlus^#(false(), x, y, z) -> c_10(plusIter^#(x, s(y), s(z))) }
Weak Trs:
  { le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , plus(x, y) -> plusIter(x, y, 0())
  , inc(0()) -> 0()
  , inc(s(i)) -> s(inc(i))
  , minus(x, 0()) -> x
  , minus(0(), y) -> 0()
  , minus(s(x), s(y)) -> minus(x, y)
  , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z)
  , ifPlus(true(), x, y, z) -> y
  , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'matrices' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'matrix interpretation of dimension 4' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   2) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   4) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   5) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   6) 'matrix interpretation of dimension 1' failed due to the
      following reason:
      
      The input cannot be shown compatible
   

2) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.


Arrrr..