MAYBE

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

Strict Trs:
  { table() -> gen(s(0()))
  , gen(x) -> if1(le(x, 10()), x)
  , if1(false(), x) -> nil()
  , if1(true(), x) -> if2(x, x)
  , le(s(x), s(y)) -> le(x, y)
  , le(s(x), 0()) -> false()
  , le(0(), y) -> true()
  , 10() -> s(s(s(s(s(s(s(s(s(s(0()))))))))))
  , if2(x, y) -> if3(le(y, 10()), x, y)
  , if3(false(), x, y) -> gen(s(x))
  , if3(true(), x, y) -> cons(entry(x, y, times(x, y)), if2(x, s(y)))
  , times(s(x), y) -> plus(y, times(x, y))
  , times(0(), y) -> 0()
  , plus(s(x), y) -> s(plus(x, y))
  , plus(0(), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { table^#() -> c_1(gen^#(s(0())))
  , gen^#(x) -> c_2(if1^#(le(x, 10()), x), le^#(x, 10()), 10^#())
  , if1^#(false(), x) -> c_3()
  , if1^#(true(), x) -> c_4(if2^#(x, x))
  , le^#(s(x), s(y)) -> c_5(le^#(x, y))
  , le^#(s(x), 0()) -> c_6()
  , le^#(0(), y) -> c_7()
  , 10^#() -> c_8()
  , if2^#(x, y) ->
    c_9(if3^#(le(y, 10()), x, y), le^#(y, 10()), 10^#())
  , if3^#(false(), x, y) -> c_10(gen^#(s(x)))
  , if3^#(true(), x, y) -> c_11(times^#(x, y), if2^#(x, s(y)))
  , times^#(s(x), y) -> c_12(plus^#(y, times(x, y)), times^#(x, y))
  , times^#(0(), y) -> c_13()
  , plus^#(s(x), y) -> c_14(plus^#(x, y))
  , plus^#(0(), y) -> c_15() }

and mark the set of starting terms.

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

Strict DPs:
  { table^#() -> c_1(gen^#(s(0())))
  , gen^#(x) -> c_2(if1^#(le(x, 10()), x), le^#(x, 10()), 10^#())
  , if1^#(false(), x) -> c_3()
  , if1^#(true(), x) -> c_4(if2^#(x, x))
  , le^#(s(x), s(y)) -> c_5(le^#(x, y))
  , le^#(s(x), 0()) -> c_6()
  , le^#(0(), y) -> c_7()
  , 10^#() -> c_8()
  , if2^#(x, y) ->
    c_9(if3^#(le(y, 10()), x, y), le^#(y, 10()), 10^#())
  , if3^#(false(), x, y) -> c_10(gen^#(s(x)))
  , if3^#(true(), x, y) -> c_11(times^#(x, y), if2^#(x, s(y)))
  , times^#(s(x), y) -> c_12(plus^#(y, times(x, y)), times^#(x, y))
  , times^#(0(), y) -> c_13()
  , plus^#(s(x), y) -> c_14(plus^#(x, y))
  , plus^#(0(), y) -> c_15() }
Weak Trs:
  { table() -> gen(s(0()))
  , gen(x) -> if1(le(x, 10()), x)
  , if1(false(), x) -> nil()
  , if1(true(), x) -> if2(x, x)
  , le(s(x), s(y)) -> le(x, y)
  , le(s(x), 0()) -> false()
  , le(0(), y) -> true()
  , 10() -> s(s(s(s(s(s(s(s(s(s(0()))))))))))
  , if2(x, y) -> if3(le(y, 10()), x, y)
  , if3(false(), x, y) -> gen(s(x))
  , if3(true(), x, y) -> cons(entry(x, y, times(x, y)), if2(x, s(y)))
  , times(s(x), y) -> plus(y, times(x, y))
  , times(0(), y) -> 0()
  , plus(s(x), y) -> s(plus(x, y))
  , plus(0(), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: table^#() -> c_1(gen^#(s(0())))
    , 2: gen^#(x) -> c_2(if1^#(le(x, 10()), x), le^#(x, 10()), 10^#())
    , 3: if1^#(false(), x) -> c_3()
    , 4: if1^#(true(), x) -> c_4(if2^#(x, x))
    , 5: le^#(s(x), s(y)) -> c_5(le^#(x, y))
    , 6: le^#(s(x), 0()) -> c_6()
    , 7: le^#(0(), y) -> c_7()
    , 8: 10^#() -> c_8()
    , 9: if2^#(x, y) ->
         c_9(if3^#(le(y, 10()), x, y), le^#(y, 10()), 10^#())
    , 10: if3^#(false(), x, y) -> c_10(gen^#(s(x)))
    , 11: if3^#(true(), x, y) -> c_11(times^#(x, y), if2^#(x, s(y)))
    , 12: times^#(s(x), y) ->
          c_12(plus^#(y, times(x, y)), times^#(x, y))
    , 13: times^#(0(), y) -> c_13()
    , 14: plus^#(s(x), y) -> c_14(plus^#(x, y))
    , 15: plus^#(0(), y) -> c_15() }

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

Strict DPs:
  { table^#() -> c_1(gen^#(s(0())))
  , gen^#(x) -> c_2(if1^#(le(x, 10()), x), le^#(x, 10()), 10^#())
  , if1^#(true(), x) -> c_4(if2^#(x, x))
  , le^#(s(x), s(y)) -> c_5(le^#(x, y))
  , if2^#(x, y) ->
    c_9(if3^#(le(y, 10()), x, y), le^#(y, 10()), 10^#())
  , if3^#(false(), x, y) -> c_10(gen^#(s(x)))
  , if3^#(true(), x, y) -> c_11(times^#(x, y), if2^#(x, s(y)))
  , times^#(s(x), y) -> c_12(plus^#(y, times(x, y)), times^#(x, y))
  , plus^#(s(x), y) -> c_14(plus^#(x, y)) }
Weak DPs:
  { if1^#(false(), x) -> c_3()
  , le^#(s(x), 0()) -> c_6()
  , le^#(0(), y) -> c_7()
  , 10^#() -> c_8()
  , times^#(0(), y) -> c_13()
  , plus^#(0(), y) -> c_15() }
Weak Trs:
  { table() -> gen(s(0()))
  , gen(x) -> if1(le(x, 10()), x)
  , if1(false(), x) -> nil()
  , if1(true(), x) -> if2(x, x)
  , le(s(x), s(y)) -> le(x, y)
  , le(s(x), 0()) -> false()
  , le(0(), y) -> true()
  , 10() -> s(s(s(s(s(s(s(s(s(s(0()))))))))))
  , if2(x, y) -> if3(le(y, 10()), x, y)
  , if3(false(), x, y) -> gen(s(x))
  , if3(true(), x, y) -> cons(entry(x, y, times(x, y)), if2(x, s(y)))
  , times(s(x), y) -> plus(y, times(x, y))
  , times(0(), y) -> 0()
  , plus(s(x), y) -> s(plus(x, y))
  , plus(0(), y) -> y }
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^#(false(), x) -> c_3()
, le^#(s(x), 0()) -> c_6()
, le^#(0(), y) -> c_7()
, 10^#() -> c_8()
, times^#(0(), y) -> c_13()
, plus^#(0(), y) -> c_15() }

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

Strict DPs:
  { table^#() -> c_1(gen^#(s(0())))
  , gen^#(x) -> c_2(if1^#(le(x, 10()), x), le^#(x, 10()), 10^#())
  , if1^#(true(), x) -> c_4(if2^#(x, x))
  , le^#(s(x), s(y)) -> c_5(le^#(x, y))
  , if2^#(x, y) ->
    c_9(if3^#(le(y, 10()), x, y), le^#(y, 10()), 10^#())
  , if3^#(false(), x, y) -> c_10(gen^#(s(x)))
  , if3^#(true(), x, y) -> c_11(times^#(x, y), if2^#(x, s(y)))
  , times^#(s(x), y) -> c_12(plus^#(y, times(x, y)), times^#(x, y))
  , plus^#(s(x), y) -> c_14(plus^#(x, y)) }
Weak Trs:
  { table() -> gen(s(0()))
  , gen(x) -> if1(le(x, 10()), x)
  , if1(false(), x) -> nil()
  , if1(true(), x) -> if2(x, x)
  , le(s(x), s(y)) -> le(x, y)
  , le(s(x), 0()) -> false()
  , le(0(), y) -> true()
  , 10() -> s(s(s(s(s(s(s(s(s(s(0()))))))))))
  , if2(x, y) -> if3(le(y, 10()), x, y)
  , if3(false(), x, y) -> gen(s(x))
  , if3(true(), x, y) -> cons(entry(x, y, times(x, y)), if2(x, s(y)))
  , times(s(x), y) -> plus(y, times(x, y))
  , times(0(), y) -> 0()
  , plus(s(x), y) -> s(plus(x, y))
  , plus(0(), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { gen^#(x) -> c_2(if1^#(le(x, 10()), x), le^#(x, 10()), 10^#())
  , if2^#(x, y) ->
    c_9(if3^#(le(y, 10()), x, y), le^#(y, 10()), 10^#()) }

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

Strict DPs:
  { table^#() -> c_1(gen^#(s(0())))
  , gen^#(x) -> c_2(if1^#(le(x, 10()), x), le^#(x, 10()))
  , if1^#(true(), x) -> c_3(if2^#(x, x))
  , le^#(s(x), s(y)) -> c_4(le^#(x, y))
  , if2^#(x, y) -> c_5(if3^#(le(y, 10()), x, y), le^#(y, 10()))
  , if3^#(false(), x, y) -> c_6(gen^#(s(x)))
  , if3^#(true(), x, y) -> c_7(times^#(x, y), if2^#(x, s(y)))
  , times^#(s(x), y) -> c_8(plus^#(y, times(x, y)), times^#(x, y))
  , plus^#(s(x), y) -> c_9(plus^#(x, y)) }
Weak Trs:
  { table() -> gen(s(0()))
  , gen(x) -> if1(le(x, 10()), x)
  , if1(false(), x) -> nil()
  , if1(true(), x) -> if2(x, x)
  , le(s(x), s(y)) -> le(x, y)
  , le(s(x), 0()) -> false()
  , le(0(), y) -> true()
  , 10() -> s(s(s(s(s(s(s(s(s(s(0()))))))))))
  , if2(x, y) -> if3(le(y, 10()), x, y)
  , if3(false(), x, y) -> gen(s(x))
  , if3(true(), x, y) -> cons(entry(x, y, times(x, y)), if2(x, s(y)))
  , times(s(x), y) -> plus(y, times(x, y))
  , times(0(), y) -> 0()
  , plus(s(x), y) -> s(plus(x, y))
  , plus(0(), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { le(s(x), s(y)) -> le(x, y)
    , le(s(x), 0()) -> false()
    , le(0(), y) -> true()
    , 10() -> s(s(s(s(s(s(s(s(s(s(0()))))))))))
    , times(s(x), y) -> plus(y, times(x, y))
    , times(0(), y) -> 0()
    , plus(s(x), y) -> s(plus(x, y))
    , plus(0(), y) -> y }

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

Strict DPs:
  { table^#() -> c_1(gen^#(s(0())))
  , gen^#(x) -> c_2(if1^#(le(x, 10()), x), le^#(x, 10()))
  , if1^#(true(), x) -> c_3(if2^#(x, x))
  , le^#(s(x), s(y)) -> c_4(le^#(x, y))
  , if2^#(x, y) -> c_5(if3^#(le(y, 10()), x, y), le^#(y, 10()))
  , if3^#(false(), x, y) -> c_6(gen^#(s(x)))
  , if3^#(true(), x, y) -> c_7(times^#(x, y), if2^#(x, s(y)))
  , times^#(s(x), y) -> c_8(plus^#(y, times(x, y)), times^#(x, y))
  , plus^#(s(x), y) -> c_9(plus^#(x, y)) }
Weak Trs:
  { le(s(x), s(y)) -> le(x, y)
  , le(s(x), 0()) -> false()
  , le(0(), y) -> true()
  , 10() -> s(s(s(s(s(s(s(s(s(s(0()))))))))))
  , times(s(x), y) -> plus(y, times(x, y))
  , times(0(), y) -> 0()
  , plus(s(x), y) -> s(plus(x, y))
  , plus(0(), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: table^#() -> c_1(gen^#(s(0())))
     -->_1 gen^#(x) -> c_2(if1^#(le(x, 10()), x), le^#(x, 10())) :2
  
  2: gen^#(x) -> c_2(if1^#(le(x, 10()), x), le^#(x, 10()))
     -->_2 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4
     -->_1 if1^#(true(), x) -> c_3(if2^#(x, x)) :3
  
  3: if1^#(true(), x) -> c_3(if2^#(x, x))
     -->_1 if2^#(x, y) ->
           c_5(if3^#(le(y, 10()), x, y), le^#(y, 10())) :5
  
  4: le^#(s(x), s(y)) -> c_4(le^#(x, y))
     -->_1 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4
  
  5: if2^#(x, y) -> c_5(if3^#(le(y, 10()), x, y), le^#(y, 10()))
     -->_1 if3^#(true(), x, y) -> c_7(times^#(x, y), if2^#(x, s(y))) :7
     -->_1 if3^#(false(), x, y) -> c_6(gen^#(s(x))) :6
     -->_2 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4
  
  6: if3^#(false(), x, y) -> c_6(gen^#(s(x)))
     -->_1 gen^#(x) -> c_2(if1^#(le(x, 10()), x), le^#(x, 10())) :2
  
  7: if3^#(true(), x, y) -> c_7(times^#(x, y), if2^#(x, s(y)))
     -->_1 times^#(s(x), y) ->
           c_8(plus^#(y, times(x, y)), times^#(x, y)) :8
     -->_2 if2^#(x, y) ->
           c_5(if3^#(le(y, 10()), x, y), le^#(y, 10())) :5
  
  8: times^#(s(x), y) -> c_8(plus^#(y, times(x, y)), times^#(x, y))
     -->_1 plus^#(s(x), y) -> c_9(plus^#(x, y)) :9
     -->_2 times^#(s(x), y) ->
           c_8(plus^#(y, times(x, y)), times^#(x, y)) :8
  
  9: plus^#(s(x), y) -> c_9(plus^#(x, y))
     -->_1 plus^#(s(x), y) -> c_9(plus^#(x, y)) :9
  

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

  { table^#() -> c_1(gen^#(s(0()))) }


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

Strict DPs:
  { gen^#(x) -> c_2(if1^#(le(x, 10()), x), le^#(x, 10()))
  , if1^#(true(), x) -> c_3(if2^#(x, x))
  , le^#(s(x), s(y)) -> c_4(le^#(x, y))
  , if2^#(x, y) -> c_5(if3^#(le(y, 10()), x, y), le^#(y, 10()))
  , if3^#(false(), x, y) -> c_6(gen^#(s(x)))
  , if3^#(true(), x, y) -> c_7(times^#(x, y), if2^#(x, s(y)))
  , times^#(s(x), y) -> c_8(plus^#(y, times(x, y)), times^#(x, y))
  , plus^#(s(x), y) -> c_9(plus^#(x, y)) }
Weak Trs:
  { le(s(x), s(y)) -> le(x, y)
  , le(s(x), 0()) -> false()
  , le(0(), y) -> true()
  , 10() -> s(s(s(s(s(s(s(s(s(s(0()))))))))))
  , times(s(x), y) -> plus(y, times(x, y))
  , times(0(), y) -> 0()
  , plus(s(x), y) -> s(plus(x, y))
  , plus(0(), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..