MAYBE

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

Strict Trs:
  { gcd(x, y) -> gcd2(x, y, 0())
  , gcd2(x, y, i) ->
    if1(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc(i))
  , if1(true(), b1, b2, b3, x, y, i) ->
    pair(result(y), neededIterations(i))
  , if1(false(), b1, b2, b3, x, y, i) -> if2(b1, b2, b3, x, y, i)
  , le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , inc(0()) -> 0()
  , inc(s(i)) -> s(inc(i))
  , if2(true(), b2, b3, x, y, i) ->
    pair(result(x), neededIterations(i))
  , if2(false(), b2, b3, x, y, i) -> if3(b2, b3, x, y, i)
  , if3(true(), b3, x, y, i) -> if4(b3, x, y, i)
  , if3(false(), b3, x, y, i) -> gcd2(minus(x, y), y, i)
  , minus(x, 0()) -> x
  , minus(0(), y) -> 0()
  , minus(s(x), s(y)) -> minus(x, y)
  , if4(true(), x, y, i) -> pair(result(x), neededIterations(i))
  , if4(false(), x, y, i) -> gcd2(x, minus(y, x), i)
  , a() -> b()
  , a() -> c() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { gcd^#(x, y) -> c_1(gcd2^#(x, y, 0()))
  , gcd2^#(x, y, i) ->
    c_2(if1^#(le(x, 0()),
              le(y, 0()),
              le(x, y),
              le(y, x),
              x,
              y,
              inc(i)),
        le^#(x, 0()),
        le^#(y, 0()),
        le^#(x, y),
        le^#(y, x),
        inc^#(i))
  , if1^#(true(), b1, b2, b3, x, y, i) -> c_3()
  , if1^#(false(), b1, b2, b3, x, y, i) ->
    c_4(if2^#(b1, b2, b3, x, y, i))
  , le^#(0(), y) -> c_5()
  , le^#(s(x), 0()) -> c_6()
  , le^#(s(x), s(y)) -> c_7(le^#(x, y))
  , inc^#(0()) -> c_8()
  , inc^#(s(i)) -> c_9(inc^#(i))
  , if2^#(true(), b2, b3, x, y, i) -> c_10()
  , if2^#(false(), b2, b3, x, y, i) -> c_11(if3^#(b2, b3, x, y, i))
  , if3^#(true(), b3, x, y, i) -> c_12(if4^#(b3, x, y, i))
  , if3^#(false(), b3, x, y, i) ->
    c_13(gcd2^#(minus(x, y), y, i), minus^#(x, y))
  , if4^#(true(), x, y, i) -> c_17()
  , if4^#(false(), x, y, i) ->
    c_18(gcd2^#(x, minus(y, x), i), minus^#(y, x))
  , minus^#(x, 0()) -> c_14()
  , minus^#(0(), y) -> c_15()
  , minus^#(s(x), s(y)) -> c_16(minus^#(x, y))
  , 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:
  { gcd^#(x, y) -> c_1(gcd2^#(x, y, 0()))
  , gcd2^#(x, y, i) ->
    c_2(if1^#(le(x, 0()),
              le(y, 0()),
              le(x, y),
              le(y, x),
              x,
              y,
              inc(i)),
        le^#(x, 0()),
        le^#(y, 0()),
        le^#(x, y),
        le^#(y, x),
        inc^#(i))
  , if1^#(true(), b1, b2, b3, x, y, i) -> c_3()
  , if1^#(false(), b1, b2, b3, x, y, i) ->
    c_4(if2^#(b1, b2, b3, x, y, i))
  , le^#(0(), y) -> c_5()
  , le^#(s(x), 0()) -> c_6()
  , le^#(s(x), s(y)) -> c_7(le^#(x, y))
  , inc^#(0()) -> c_8()
  , inc^#(s(i)) -> c_9(inc^#(i))
  , if2^#(true(), b2, b3, x, y, i) -> c_10()
  , if2^#(false(), b2, b3, x, y, i) -> c_11(if3^#(b2, b3, x, y, i))
  , if3^#(true(), b3, x, y, i) -> c_12(if4^#(b3, x, y, i))
  , if3^#(false(), b3, x, y, i) ->
    c_13(gcd2^#(minus(x, y), y, i), minus^#(x, y))
  , if4^#(true(), x, y, i) -> c_17()
  , if4^#(false(), x, y, i) ->
    c_18(gcd2^#(x, minus(y, x), i), minus^#(y, x))
  , minus^#(x, 0()) -> c_14()
  , minus^#(0(), y) -> c_15()
  , minus^#(s(x), s(y)) -> c_16(minus^#(x, y))
  , a^#() -> c_19()
  , a^#() -> c_20() }
Weak Trs:
  { gcd(x, y) -> gcd2(x, y, 0())
  , gcd2(x, y, i) ->
    if1(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc(i))
  , if1(true(), b1, b2, b3, x, y, i) ->
    pair(result(y), neededIterations(i))
  , if1(false(), b1, b2, b3, x, y, i) -> if2(b1, b2, b3, x, y, i)
  , le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , inc(0()) -> 0()
  , inc(s(i)) -> s(inc(i))
  , if2(true(), b2, b3, x, y, i) ->
    pair(result(x), neededIterations(i))
  , if2(false(), b2, b3, x, y, i) -> if3(b2, b3, x, y, i)
  , if3(true(), b3, x, y, i) -> if4(b3, x, y, i)
  , if3(false(), b3, x, y, i) -> gcd2(minus(x, y), y, i)
  , minus(x, 0()) -> x
  , minus(0(), y) -> 0()
  , minus(s(x), s(y)) -> minus(x, y)
  , if4(true(), x, y, i) -> pair(result(x), neededIterations(i))
  , if4(false(), x, y, i) -> gcd2(x, minus(y, x), i)
  , a() -> b()
  , a() -> c() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: gcd^#(x, y) -> c_1(gcd2^#(x, y, 0()))
    , 2: gcd2^#(x, y, i) ->
         c_2(if1^#(le(x, 0()),
                   le(y, 0()),
                   le(x, y),
                   le(y, x),
                   x,
                   y,
                   inc(i)),
             le^#(x, 0()),
             le^#(y, 0()),
             le^#(x, y),
             le^#(y, x),
             inc^#(i))
    , 3: if1^#(true(), b1, b2, b3, x, y, i) -> c_3()
    , 4: if1^#(false(), b1, b2, b3, x, y, i) ->
         c_4(if2^#(b1, b2, b3, x, y, i))
    , 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: inc^#(0()) -> c_8()
    , 9: inc^#(s(i)) -> c_9(inc^#(i))
    , 10: if2^#(true(), b2, b3, x, y, i) -> c_10()
    , 11: if2^#(false(), b2, b3, x, y, i) ->
          c_11(if3^#(b2, b3, x, y, i))
    , 12: if3^#(true(), b3, x, y, i) -> c_12(if4^#(b3, x, y, i))
    , 13: if3^#(false(), b3, x, y, i) ->
          c_13(gcd2^#(minus(x, y), y, i), minus^#(x, y))
    , 14: if4^#(true(), x, y, i) -> c_17()
    , 15: if4^#(false(), x, y, i) ->
          c_18(gcd2^#(x, minus(y, x), i), minus^#(y, x))
    , 16: minus^#(x, 0()) -> c_14()
    , 17: minus^#(0(), y) -> c_15()
    , 18: minus^#(s(x), s(y)) -> c_16(minus^#(x, y))
    , 19: a^#() -> c_19()
    , 20: a^#() -> c_20() }

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

Strict DPs:
  { gcd^#(x, y) -> c_1(gcd2^#(x, y, 0()))
  , gcd2^#(x, y, i) ->
    c_2(if1^#(le(x, 0()),
              le(y, 0()),
              le(x, y),
              le(y, x),
              x,
              y,
              inc(i)),
        le^#(x, 0()),
        le^#(y, 0()),
        le^#(x, y),
        le^#(y, x),
        inc^#(i))
  , if1^#(false(), b1, b2, b3, x, y, i) ->
    c_4(if2^#(b1, b2, b3, x, y, i))
  , le^#(s(x), s(y)) -> c_7(le^#(x, y))
  , inc^#(s(i)) -> c_9(inc^#(i))
  , if2^#(false(), b2, b3, x, y, i) -> c_11(if3^#(b2, b3, x, y, i))
  , if3^#(true(), b3, x, y, i) -> c_12(if4^#(b3, x, y, i))
  , if3^#(false(), b3, x, y, i) ->
    c_13(gcd2^#(minus(x, y), y, i), minus^#(x, y))
  , if4^#(false(), x, y, i) ->
    c_18(gcd2^#(x, minus(y, x), i), minus^#(y, x))
  , minus^#(s(x), s(y)) -> c_16(minus^#(x, y)) }
Weak DPs:
  { if1^#(true(), b1, b2, b3, x, y, i) -> c_3()
  , le^#(0(), y) -> c_5()
  , le^#(s(x), 0()) -> c_6()
  , inc^#(0()) -> c_8()
  , if2^#(true(), b2, b3, x, y, i) -> c_10()
  , if4^#(true(), x, y, i) -> c_17()
  , minus^#(x, 0()) -> c_14()
  , minus^#(0(), y) -> c_15()
  , a^#() -> c_19()
  , a^#() -> c_20() }
Weak Trs:
  { gcd(x, y) -> gcd2(x, y, 0())
  , gcd2(x, y, i) ->
    if1(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc(i))
  , if1(true(), b1, b2, b3, x, y, i) ->
    pair(result(y), neededIterations(i))
  , if1(false(), b1, b2, b3, x, y, i) -> if2(b1, b2, b3, x, y, i)
  , le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , inc(0()) -> 0()
  , inc(s(i)) -> s(inc(i))
  , if2(true(), b2, b3, x, y, i) ->
    pair(result(x), neededIterations(i))
  , if2(false(), b2, b3, x, y, i) -> if3(b2, b3, x, y, i)
  , if3(true(), b3, x, y, i) -> if4(b3, x, y, i)
  , if3(false(), b3, x, y, i) -> gcd2(minus(x, y), y, i)
  , minus(x, 0()) -> x
  , minus(0(), y) -> 0()
  , minus(s(x), s(y)) -> minus(x, y)
  , if4(true(), x, y, i) -> pair(result(x), neededIterations(i))
  , if4(false(), x, y, i) -> gcd2(x, minus(y, x), i)
  , a() -> b()
  , a() -> c() }
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(), b1, b2, b3, x, y, i) -> c_3()
, le^#(0(), y) -> c_5()
, le^#(s(x), 0()) -> c_6()
, inc^#(0()) -> c_8()
, if2^#(true(), b2, b3, x, y, i) -> c_10()
, if4^#(true(), x, y, i) -> c_17()
, minus^#(x, 0()) -> c_14()
, minus^#(0(), y) -> c_15()
, a^#() -> c_19()
, a^#() -> c_20() }

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

Strict DPs:
  { gcd^#(x, y) -> c_1(gcd2^#(x, y, 0()))
  , gcd2^#(x, y, i) ->
    c_2(if1^#(le(x, 0()),
              le(y, 0()),
              le(x, y),
              le(y, x),
              x,
              y,
              inc(i)),
        le^#(x, 0()),
        le^#(y, 0()),
        le^#(x, y),
        le^#(y, x),
        inc^#(i))
  , if1^#(false(), b1, b2, b3, x, y, i) ->
    c_4(if2^#(b1, b2, b3, x, y, i))
  , le^#(s(x), s(y)) -> c_7(le^#(x, y))
  , inc^#(s(i)) -> c_9(inc^#(i))
  , if2^#(false(), b2, b3, x, y, i) -> c_11(if3^#(b2, b3, x, y, i))
  , if3^#(true(), b3, x, y, i) -> c_12(if4^#(b3, x, y, i))
  , if3^#(false(), b3, x, y, i) ->
    c_13(gcd2^#(minus(x, y), y, i), minus^#(x, y))
  , if4^#(false(), x, y, i) ->
    c_18(gcd2^#(x, minus(y, x), i), minus^#(y, x))
  , minus^#(s(x), s(y)) -> c_16(minus^#(x, y)) }
Weak Trs:
  { gcd(x, y) -> gcd2(x, y, 0())
  , gcd2(x, y, i) ->
    if1(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc(i))
  , if1(true(), b1, b2, b3, x, y, i) ->
    pair(result(y), neededIterations(i))
  , if1(false(), b1, b2, b3, x, y, i) -> if2(b1, b2, b3, x, y, i)
  , le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , inc(0()) -> 0()
  , inc(s(i)) -> s(inc(i))
  , if2(true(), b2, b3, x, y, i) ->
    pair(result(x), neededIterations(i))
  , if2(false(), b2, b3, x, y, i) -> if3(b2, b3, x, y, i)
  , if3(true(), b3, x, y, i) -> if4(b3, x, y, i)
  , if3(false(), b3, x, y, i) -> gcd2(minus(x, y), y, i)
  , minus(x, 0()) -> x
  , minus(0(), y) -> 0()
  , minus(s(x), s(y)) -> minus(x, y)
  , if4(true(), x, y, i) -> pair(result(x), neededIterations(i))
  , if4(false(), x, y, i) -> gcd2(x, minus(y, x), i)
  , a() -> b()
  , a() -> c() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

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

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

Strict DPs:
  { gcd^#(x, y) -> c_1(gcd2^#(x, y, 0()))
  , gcd2^#(x, y, i) ->
    c_2(if1^#(le(x, 0()),
              le(y, 0()),
              le(x, y),
              le(y, x),
              x,
              y,
              inc(i)),
        le^#(x, y),
        le^#(y, x),
        inc^#(i))
  , if1^#(false(), b1, b2, b3, x, y, i) ->
    c_3(if2^#(b1, b2, b3, x, y, i))
  , le^#(s(x), s(y)) -> c_4(le^#(x, y))
  , inc^#(s(i)) -> c_5(inc^#(i))
  , if2^#(false(), b2, b3, x, y, i) -> c_6(if3^#(b2, b3, x, y, i))
  , if3^#(true(), b3, x, y, i) -> c_7(if4^#(b3, x, y, i))
  , if3^#(false(), b3, x, y, i) ->
    c_8(gcd2^#(minus(x, y), y, i), minus^#(x, y))
  , if4^#(false(), x, y, i) ->
    c_9(gcd2^#(x, minus(y, x), i), minus^#(y, x))
  , minus^#(s(x), s(y)) -> c_10(minus^#(x, y)) }
Weak Trs:
  { gcd(x, y) -> gcd2(x, y, 0())
  , gcd2(x, y, i) ->
    if1(le(x, 0()), le(y, 0()), le(x, y), le(y, x), x, y, inc(i))
  , if1(true(), b1, b2, b3, x, y, i) ->
    pair(result(y), neededIterations(i))
  , if1(false(), b1, b2, b3, x, y, i) -> if2(b1, b2, b3, x, y, i)
  , le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , inc(0()) -> 0()
  , inc(s(i)) -> s(inc(i))
  , if2(true(), b2, b3, x, y, i) ->
    pair(result(x), neededIterations(i))
  , if2(false(), b2, b3, x, y, i) -> if3(b2, b3, x, y, i)
  , if3(true(), b3, x, y, i) -> if4(b3, x, y, i)
  , if3(false(), b3, x, y, i) -> gcd2(minus(x, y), y, i)
  , minus(x, 0()) -> x
  , minus(0(), y) -> 0()
  , minus(s(x), s(y)) -> minus(x, y)
  , if4(true(), x, y, i) -> pair(result(x), neededIterations(i))
  , if4(false(), x, y, i) -> gcd2(x, minus(y, x), i)
  , a() -> b()
  , a() -> c() }
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)
    , 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) }

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

Strict DPs:
  { gcd^#(x, y) -> c_1(gcd2^#(x, y, 0()))
  , gcd2^#(x, y, i) ->
    c_2(if1^#(le(x, 0()),
              le(y, 0()),
              le(x, y),
              le(y, x),
              x,
              y,
              inc(i)),
        le^#(x, y),
        le^#(y, x),
        inc^#(i))
  , if1^#(false(), b1, b2, b3, x, y, i) ->
    c_3(if2^#(b1, b2, b3, x, y, i))
  , le^#(s(x), s(y)) -> c_4(le^#(x, y))
  , inc^#(s(i)) -> c_5(inc^#(i))
  , if2^#(false(), b2, b3, x, y, i) -> c_6(if3^#(b2, b3, x, y, i))
  , if3^#(true(), b3, x, y, i) -> c_7(if4^#(b3, x, y, i))
  , if3^#(false(), b3, x, y, i) ->
    c_8(gcd2^#(minus(x, y), y, i), minus^#(x, y))
  , if4^#(false(), x, y, i) ->
    c_9(gcd2^#(x, minus(y, x), i), minus^#(y, x))
  , minus^#(s(x), s(y)) -> c_10(minus^#(x, y)) }
Weak Trs:
  { le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , 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) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: gcd^#(x, y) -> c_1(gcd2^#(x, y, 0()))
     -->_1 gcd2^#(x, y, i) ->
           c_2(if1^#(le(x, 0()),
                     le(y, 0()),
                     le(x, y),
                     le(y, x),
                     x,
                     y,
                     inc(i)),
               le^#(x, y),
               le^#(y, x),
               inc^#(i)) :2
  
  2: gcd2^#(x, y, i) ->
     c_2(if1^#(le(x, 0()),
               le(y, 0()),
               le(x, y),
               le(y, x),
               x,
               y,
               inc(i)),
         le^#(x, y),
         le^#(y, x),
         inc^#(i))
     -->_4 inc^#(s(i)) -> c_5(inc^#(i)) :5
     -->_3 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4
     -->_2 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4
     -->_1 if1^#(false(), b1, b2, b3, x, y, i) ->
           c_3(if2^#(b1, b2, b3, x, y, i)) :3
  
  3: if1^#(false(), b1, b2, b3, x, y, i) ->
     c_3(if2^#(b1, b2, b3, x, y, i))
     -->_1 if2^#(false(), b2, b3, x, y, i) ->
           c_6(if3^#(b2, b3, x, y, i)) :6
  
  4: le^#(s(x), s(y)) -> c_4(le^#(x, y))
     -->_1 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4
  
  5: inc^#(s(i)) -> c_5(inc^#(i))
     -->_1 inc^#(s(i)) -> c_5(inc^#(i)) :5
  
  6: if2^#(false(), b2, b3, x, y, i) -> c_6(if3^#(b2, b3, x, y, i))
     -->_1 if3^#(false(), b3, x, y, i) ->
           c_8(gcd2^#(minus(x, y), y, i), minus^#(x, y)) :8
     -->_1 if3^#(true(), b3, x, y, i) -> c_7(if4^#(b3, x, y, i)) :7
  
  7: if3^#(true(), b3, x, y, i) -> c_7(if4^#(b3, x, y, i))
     -->_1 if4^#(false(), x, y, i) ->
           c_9(gcd2^#(x, minus(y, x), i), minus^#(y, x)) :9
  
  8: if3^#(false(), b3, x, y, i) ->
     c_8(gcd2^#(minus(x, y), y, i), minus^#(x, y))
     -->_2 minus^#(s(x), s(y)) -> c_10(minus^#(x, y)) :10
     -->_1 gcd2^#(x, y, i) ->
           c_2(if1^#(le(x, 0()),
                     le(y, 0()),
                     le(x, y),
                     le(y, x),
                     x,
                     y,
                     inc(i)),
               le^#(x, y),
               le^#(y, x),
               inc^#(i)) :2
  
  9: if4^#(false(), x, y, i) ->
     c_9(gcd2^#(x, minus(y, x), i), minus^#(y, x))
     -->_2 minus^#(s(x), s(y)) -> c_10(minus^#(x, y)) :10
     -->_1 gcd2^#(x, y, i) ->
           c_2(if1^#(le(x, 0()),
                     le(y, 0()),
                     le(x, y),
                     le(y, x),
                     x,
                     y,
                     inc(i)),
               le^#(x, y),
               le^#(y, x),
               inc^#(i)) :2
  
  10: minus^#(s(x), s(y)) -> c_10(minus^#(x, y))
     -->_1 minus^#(s(x), s(y)) -> c_10(minus^#(x, y)) :10
  

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

  { gcd^#(x, y) -> c_1(gcd2^#(x, y, 0())) }


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

Strict DPs:
  { gcd2^#(x, y, i) ->
    c_2(if1^#(le(x, 0()),
              le(y, 0()),
              le(x, y),
              le(y, x),
              x,
              y,
              inc(i)),
        le^#(x, y),
        le^#(y, x),
        inc^#(i))
  , if1^#(false(), b1, b2, b3, x, y, i) ->
    c_3(if2^#(b1, b2, b3, x, y, i))
  , le^#(s(x), s(y)) -> c_4(le^#(x, y))
  , inc^#(s(i)) -> c_5(inc^#(i))
  , if2^#(false(), b2, b3, x, y, i) -> c_6(if3^#(b2, b3, x, y, i))
  , if3^#(true(), b3, x, y, i) -> c_7(if4^#(b3, x, y, i))
  , if3^#(false(), b3, x, y, i) ->
    c_8(gcd2^#(minus(x, y), y, i), minus^#(x, y))
  , if4^#(false(), x, y, i) ->
    c_9(gcd2^#(x, minus(y, x), i), minus^#(y, x))
  , minus^#(s(x), s(y)) -> c_10(minus^#(x, y)) }
Weak Trs:
  { le(0(), y) -> true()
  , le(s(x), 0()) -> false()
  , le(s(x), s(y)) -> le(x, y)
  , 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) }
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..