MAYBE

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

Strict Trs:
  { car(cons(x, l)) -> x
  , cddr(cons(x, cons(y, l))) -> l
  , cddr(cons(x, nil())) -> nil()
  , cddr(nil()) -> nil()
  , cadr(cons(x, cons(y, l))) -> y
  , isZero(0()) -> true()
  , isZero(s(x)) -> false()
  , plus(x, y) -> ifplus(isZero(x), x, y)
  , ifplus(true(), x, y) -> y
  , ifplus(false(), x, y) -> s(plus(p(x), y))
  , p(0()) -> 0()
  , p(s(x)) -> x
  , times(x, y) -> iftimes(isZero(x), x, y)
  , iftimes(true(), x, y) -> 0()
  , iftimes(false(), x, y) -> plus(y, times(p(x), y))
  , shorter(cons(x, l), 0()) -> false()
  , shorter(cons(x, l), s(y)) -> shorter(l, y)
  , shorter(nil(), y) -> true()
  , prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l)
  , if(true(), b, l) -> s(0())
  , if(false(), b, l) -> if2(b, l)
  , if2(true(), l) -> car(l)
  , if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { car^#(cons(x, l)) -> c_1()
  , cddr^#(cons(x, cons(y, l))) -> c_2()
  , cddr^#(cons(x, nil())) -> c_3()
  , cddr^#(nil()) -> c_4()
  , cadr^#(cons(x, cons(y, l))) -> c_5()
  , isZero^#(0()) -> c_6()
  , isZero^#(s(x)) -> c_7()
  , plus^#(x, y) -> c_8(ifplus^#(isZero(x), x, y), isZero^#(x))
  , ifplus^#(true(), x, y) -> c_9()
  , ifplus^#(false(), x, y) -> c_10(plus^#(p(x), y), p^#(x))
  , p^#(0()) -> c_11()
  , p^#(s(x)) -> c_12()
  , times^#(x, y) -> c_13(iftimes^#(isZero(x), x, y), isZero^#(x))
  , iftimes^#(true(), x, y) -> c_14()
  , iftimes^#(false(), x, y) ->
    c_15(plus^#(y, times(p(x), y)), times^#(p(x), y), p^#(x))
  , shorter^#(cons(x, l), 0()) -> c_16()
  , shorter^#(cons(x, l), s(y)) -> c_17(shorter^#(l, y))
  , shorter^#(nil(), y) -> c_18()
  , prod^#(l) ->
    c_19(if^#(shorter(l, 0()), shorter(l, s(0())), l),
         shorter^#(l, 0()),
         shorter^#(l, s(0())))
  , if^#(true(), b, l) -> c_20()
  , if^#(false(), b, l) -> c_21(if2^#(b, l))
  , if2^#(true(), l) -> c_22(car^#(l))
  , if2^#(false(), l) ->
    c_23(prod^#(cons(times(car(l), cadr(l)), cddr(l))),
         times^#(car(l), cadr(l)),
         car^#(l),
         cadr^#(l),
         cddr^#(l)) }

and mark the set of starting terms.

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

Strict DPs:
  { car^#(cons(x, l)) -> c_1()
  , cddr^#(cons(x, cons(y, l))) -> c_2()
  , cddr^#(cons(x, nil())) -> c_3()
  , cddr^#(nil()) -> c_4()
  , cadr^#(cons(x, cons(y, l))) -> c_5()
  , isZero^#(0()) -> c_6()
  , isZero^#(s(x)) -> c_7()
  , plus^#(x, y) -> c_8(ifplus^#(isZero(x), x, y), isZero^#(x))
  , ifplus^#(true(), x, y) -> c_9()
  , ifplus^#(false(), x, y) -> c_10(plus^#(p(x), y), p^#(x))
  , p^#(0()) -> c_11()
  , p^#(s(x)) -> c_12()
  , times^#(x, y) -> c_13(iftimes^#(isZero(x), x, y), isZero^#(x))
  , iftimes^#(true(), x, y) -> c_14()
  , iftimes^#(false(), x, y) ->
    c_15(plus^#(y, times(p(x), y)), times^#(p(x), y), p^#(x))
  , shorter^#(cons(x, l), 0()) -> c_16()
  , shorter^#(cons(x, l), s(y)) -> c_17(shorter^#(l, y))
  , shorter^#(nil(), y) -> c_18()
  , prod^#(l) ->
    c_19(if^#(shorter(l, 0()), shorter(l, s(0())), l),
         shorter^#(l, 0()),
         shorter^#(l, s(0())))
  , if^#(true(), b, l) -> c_20()
  , if^#(false(), b, l) -> c_21(if2^#(b, l))
  , if2^#(true(), l) -> c_22(car^#(l))
  , if2^#(false(), l) ->
    c_23(prod^#(cons(times(car(l), cadr(l)), cddr(l))),
         times^#(car(l), cadr(l)),
         car^#(l),
         cadr^#(l),
         cddr^#(l)) }
Weak Trs:
  { car(cons(x, l)) -> x
  , cddr(cons(x, cons(y, l))) -> l
  , cddr(cons(x, nil())) -> nil()
  , cddr(nil()) -> nil()
  , cadr(cons(x, cons(y, l))) -> y
  , isZero(0()) -> true()
  , isZero(s(x)) -> false()
  , plus(x, y) -> ifplus(isZero(x), x, y)
  , ifplus(true(), x, y) -> y
  , ifplus(false(), x, y) -> s(plus(p(x), y))
  , p(0()) -> 0()
  , p(s(x)) -> x
  , times(x, y) -> iftimes(isZero(x), x, y)
  , iftimes(true(), x, y) -> 0()
  , iftimes(false(), x, y) -> plus(y, times(p(x), y))
  , shorter(cons(x, l), 0()) -> false()
  , shorter(cons(x, l), s(y)) -> shorter(l, y)
  , shorter(nil(), y) -> true()
  , prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l)
  , if(true(), b, l) -> s(0())
  , if(false(), b, l) -> if2(b, l)
  , if2(true(), l) -> car(l)
  , if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: car^#(cons(x, l)) -> c_1()
    , 2: cddr^#(cons(x, cons(y, l))) -> c_2()
    , 3: cddr^#(cons(x, nil())) -> c_3()
    , 4: cddr^#(nil()) -> c_4()
    , 5: cadr^#(cons(x, cons(y, l))) -> c_5()
    , 6: isZero^#(0()) -> c_6()
    , 7: isZero^#(s(x)) -> c_7()
    , 8: plus^#(x, y) -> c_8(ifplus^#(isZero(x), x, y), isZero^#(x))
    , 9: ifplus^#(true(), x, y) -> c_9()
    , 10: ifplus^#(false(), x, y) -> c_10(plus^#(p(x), y), p^#(x))
    , 11: p^#(0()) -> c_11()
    , 12: p^#(s(x)) -> c_12()
    , 13: times^#(x, y) ->
          c_13(iftimes^#(isZero(x), x, y), isZero^#(x))
    , 14: iftimes^#(true(), x, y) -> c_14()
    , 15: iftimes^#(false(), x, y) ->
          c_15(plus^#(y, times(p(x), y)), times^#(p(x), y), p^#(x))
    , 16: shorter^#(cons(x, l), 0()) -> c_16()
    , 17: shorter^#(cons(x, l), s(y)) -> c_17(shorter^#(l, y))
    , 18: shorter^#(nil(), y) -> c_18()
    , 19: prod^#(l) ->
          c_19(if^#(shorter(l, 0()), shorter(l, s(0())), l),
               shorter^#(l, 0()),
               shorter^#(l, s(0())))
    , 20: if^#(true(), b, l) -> c_20()
    , 21: if^#(false(), b, l) -> c_21(if2^#(b, l))
    , 22: if2^#(true(), l) -> c_22(car^#(l))
    , 23: if2^#(false(), l) ->
          c_23(prod^#(cons(times(car(l), cadr(l)), cddr(l))),
               times^#(car(l), cadr(l)),
               car^#(l),
               cadr^#(l),
               cddr^#(l)) }

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

Strict DPs:
  { plus^#(x, y) -> c_8(ifplus^#(isZero(x), x, y), isZero^#(x))
  , ifplus^#(false(), x, y) -> c_10(plus^#(p(x), y), p^#(x))
  , times^#(x, y) -> c_13(iftimes^#(isZero(x), x, y), isZero^#(x))
  , iftimes^#(false(), x, y) ->
    c_15(plus^#(y, times(p(x), y)), times^#(p(x), y), p^#(x))
  , shorter^#(cons(x, l), s(y)) -> c_17(shorter^#(l, y))
  , prod^#(l) ->
    c_19(if^#(shorter(l, 0()), shorter(l, s(0())), l),
         shorter^#(l, 0()),
         shorter^#(l, s(0())))
  , if^#(false(), b, l) -> c_21(if2^#(b, l))
  , if2^#(true(), l) -> c_22(car^#(l))
  , if2^#(false(), l) ->
    c_23(prod^#(cons(times(car(l), cadr(l)), cddr(l))),
         times^#(car(l), cadr(l)),
         car^#(l),
         cadr^#(l),
         cddr^#(l)) }
Weak DPs:
  { car^#(cons(x, l)) -> c_1()
  , cddr^#(cons(x, cons(y, l))) -> c_2()
  , cddr^#(cons(x, nil())) -> c_3()
  , cddr^#(nil()) -> c_4()
  , cadr^#(cons(x, cons(y, l))) -> c_5()
  , isZero^#(0()) -> c_6()
  , isZero^#(s(x)) -> c_7()
  , ifplus^#(true(), x, y) -> c_9()
  , p^#(0()) -> c_11()
  , p^#(s(x)) -> c_12()
  , iftimes^#(true(), x, y) -> c_14()
  , shorter^#(cons(x, l), 0()) -> c_16()
  , shorter^#(nil(), y) -> c_18()
  , if^#(true(), b, l) -> c_20() }
Weak Trs:
  { car(cons(x, l)) -> x
  , cddr(cons(x, cons(y, l))) -> l
  , cddr(cons(x, nil())) -> nil()
  , cddr(nil()) -> nil()
  , cadr(cons(x, cons(y, l))) -> y
  , isZero(0()) -> true()
  , isZero(s(x)) -> false()
  , plus(x, y) -> ifplus(isZero(x), x, y)
  , ifplus(true(), x, y) -> y
  , ifplus(false(), x, y) -> s(plus(p(x), y))
  , p(0()) -> 0()
  , p(s(x)) -> x
  , times(x, y) -> iftimes(isZero(x), x, y)
  , iftimes(true(), x, y) -> 0()
  , iftimes(false(), x, y) -> plus(y, times(p(x), y))
  , shorter(cons(x, l), 0()) -> false()
  , shorter(cons(x, l), s(y)) -> shorter(l, y)
  , shorter(nil(), y) -> true()
  , prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l)
  , if(true(), b, l) -> s(0())
  , if(false(), b, l) -> if2(b, l)
  , if2(true(), l) -> car(l)
  , if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {8} by applications of
Pre({8}) = {7}. Here rules are labeled as follows:

  DPs:
    { 1: plus^#(x, y) -> c_8(ifplus^#(isZero(x), x, y), isZero^#(x))
    , 2: ifplus^#(false(), x, y) -> c_10(plus^#(p(x), y), p^#(x))
    , 3: times^#(x, y) -> c_13(iftimes^#(isZero(x), x, y), isZero^#(x))
    , 4: iftimes^#(false(), x, y) ->
         c_15(plus^#(y, times(p(x), y)), times^#(p(x), y), p^#(x))
    , 5: shorter^#(cons(x, l), s(y)) -> c_17(shorter^#(l, y))
    , 6: prod^#(l) ->
         c_19(if^#(shorter(l, 0()), shorter(l, s(0())), l),
              shorter^#(l, 0()),
              shorter^#(l, s(0())))
    , 7: if^#(false(), b, l) -> c_21(if2^#(b, l))
    , 8: if2^#(true(), l) -> c_22(car^#(l))
    , 9: if2^#(false(), l) ->
         c_23(prod^#(cons(times(car(l), cadr(l)), cddr(l))),
              times^#(car(l), cadr(l)),
              car^#(l),
              cadr^#(l),
              cddr^#(l))
    , 10: car^#(cons(x, l)) -> c_1()
    , 11: cddr^#(cons(x, cons(y, l))) -> c_2()
    , 12: cddr^#(cons(x, nil())) -> c_3()
    , 13: cddr^#(nil()) -> c_4()
    , 14: cadr^#(cons(x, cons(y, l))) -> c_5()
    , 15: isZero^#(0()) -> c_6()
    , 16: isZero^#(s(x)) -> c_7()
    , 17: ifplus^#(true(), x, y) -> c_9()
    , 18: p^#(0()) -> c_11()
    , 19: p^#(s(x)) -> c_12()
    , 20: iftimes^#(true(), x, y) -> c_14()
    , 21: shorter^#(cons(x, l), 0()) -> c_16()
    , 22: shorter^#(nil(), y) -> c_18()
    , 23: if^#(true(), b, l) -> c_20() }

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

Strict DPs:
  { plus^#(x, y) -> c_8(ifplus^#(isZero(x), x, y), isZero^#(x))
  , ifplus^#(false(), x, y) -> c_10(plus^#(p(x), y), p^#(x))
  , times^#(x, y) -> c_13(iftimes^#(isZero(x), x, y), isZero^#(x))
  , iftimes^#(false(), x, y) ->
    c_15(plus^#(y, times(p(x), y)), times^#(p(x), y), p^#(x))
  , shorter^#(cons(x, l), s(y)) -> c_17(shorter^#(l, y))
  , prod^#(l) ->
    c_19(if^#(shorter(l, 0()), shorter(l, s(0())), l),
         shorter^#(l, 0()),
         shorter^#(l, s(0())))
  , if^#(false(), b, l) -> c_21(if2^#(b, l))
  , if2^#(false(), l) ->
    c_23(prod^#(cons(times(car(l), cadr(l)), cddr(l))),
         times^#(car(l), cadr(l)),
         car^#(l),
         cadr^#(l),
         cddr^#(l)) }
Weak DPs:
  { car^#(cons(x, l)) -> c_1()
  , cddr^#(cons(x, cons(y, l))) -> c_2()
  , cddr^#(cons(x, nil())) -> c_3()
  , cddr^#(nil()) -> c_4()
  , cadr^#(cons(x, cons(y, l))) -> c_5()
  , isZero^#(0()) -> c_6()
  , isZero^#(s(x)) -> c_7()
  , ifplus^#(true(), x, y) -> c_9()
  , p^#(0()) -> c_11()
  , p^#(s(x)) -> c_12()
  , iftimes^#(true(), x, y) -> c_14()
  , shorter^#(cons(x, l), 0()) -> c_16()
  , shorter^#(nil(), y) -> c_18()
  , if^#(true(), b, l) -> c_20()
  , if2^#(true(), l) -> c_22(car^#(l)) }
Weak Trs:
  { car(cons(x, l)) -> x
  , cddr(cons(x, cons(y, l))) -> l
  , cddr(cons(x, nil())) -> nil()
  , cddr(nil()) -> nil()
  , cadr(cons(x, cons(y, l))) -> y
  , isZero(0()) -> true()
  , isZero(s(x)) -> false()
  , plus(x, y) -> ifplus(isZero(x), x, y)
  , ifplus(true(), x, y) -> y
  , ifplus(false(), x, y) -> s(plus(p(x), y))
  , p(0()) -> 0()
  , p(s(x)) -> x
  , times(x, y) -> iftimes(isZero(x), x, y)
  , iftimes(true(), x, y) -> 0()
  , iftimes(false(), x, y) -> plus(y, times(p(x), y))
  , shorter(cons(x, l), 0()) -> false()
  , shorter(cons(x, l), s(y)) -> shorter(l, y)
  , shorter(nil(), y) -> true()
  , prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l)
  , if(true(), b, l) -> s(0())
  , if(false(), b, l) -> if2(b, l)
  , if2(true(), l) -> car(l)
  , if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l))) }
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.

{ car^#(cons(x, l)) -> c_1()
, cddr^#(cons(x, cons(y, l))) -> c_2()
, cddr^#(cons(x, nil())) -> c_3()
, cddr^#(nil()) -> c_4()
, cadr^#(cons(x, cons(y, l))) -> c_5()
, isZero^#(0()) -> c_6()
, isZero^#(s(x)) -> c_7()
, ifplus^#(true(), x, y) -> c_9()
, p^#(0()) -> c_11()
, p^#(s(x)) -> c_12()
, iftimes^#(true(), x, y) -> c_14()
, shorter^#(cons(x, l), 0()) -> c_16()
, shorter^#(nil(), y) -> c_18()
, if^#(true(), b, l) -> c_20()
, if2^#(true(), l) -> c_22(car^#(l)) }

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

Strict DPs:
  { plus^#(x, y) -> c_8(ifplus^#(isZero(x), x, y), isZero^#(x))
  , ifplus^#(false(), x, y) -> c_10(plus^#(p(x), y), p^#(x))
  , times^#(x, y) -> c_13(iftimes^#(isZero(x), x, y), isZero^#(x))
  , iftimes^#(false(), x, y) ->
    c_15(plus^#(y, times(p(x), y)), times^#(p(x), y), p^#(x))
  , shorter^#(cons(x, l), s(y)) -> c_17(shorter^#(l, y))
  , prod^#(l) ->
    c_19(if^#(shorter(l, 0()), shorter(l, s(0())), l),
         shorter^#(l, 0()),
         shorter^#(l, s(0())))
  , if^#(false(), b, l) -> c_21(if2^#(b, l))
  , if2^#(false(), l) ->
    c_23(prod^#(cons(times(car(l), cadr(l)), cddr(l))),
         times^#(car(l), cadr(l)),
         car^#(l),
         cadr^#(l),
         cddr^#(l)) }
Weak Trs:
  { car(cons(x, l)) -> x
  , cddr(cons(x, cons(y, l))) -> l
  , cddr(cons(x, nil())) -> nil()
  , cddr(nil()) -> nil()
  , cadr(cons(x, cons(y, l))) -> y
  , isZero(0()) -> true()
  , isZero(s(x)) -> false()
  , plus(x, y) -> ifplus(isZero(x), x, y)
  , ifplus(true(), x, y) -> y
  , ifplus(false(), x, y) -> s(plus(p(x), y))
  , p(0()) -> 0()
  , p(s(x)) -> x
  , times(x, y) -> iftimes(isZero(x), x, y)
  , iftimes(true(), x, y) -> 0()
  , iftimes(false(), x, y) -> plus(y, times(p(x), y))
  , shorter(cons(x, l), 0()) -> false()
  , shorter(cons(x, l), s(y)) -> shorter(l, y)
  , shorter(nil(), y) -> true()
  , prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l)
  , if(true(), b, l) -> s(0())
  , if(false(), b, l) -> if2(b, l)
  , if2(true(), l) -> car(l)
  , if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { plus^#(x, y) -> c_8(ifplus^#(isZero(x), x, y), isZero^#(x))
  , ifplus^#(false(), x, y) -> c_10(plus^#(p(x), y), p^#(x))
  , times^#(x, y) -> c_13(iftimes^#(isZero(x), x, y), isZero^#(x))
  , iftimes^#(false(), x, y) ->
    c_15(plus^#(y, times(p(x), y)), times^#(p(x), y), p^#(x))
  , prod^#(l) ->
    c_19(if^#(shorter(l, 0()), shorter(l, s(0())), l),
         shorter^#(l, 0()),
         shorter^#(l, s(0())))
  , if2^#(false(), l) ->
    c_23(prod^#(cons(times(car(l), cadr(l)), cddr(l))),
         times^#(car(l), cadr(l)),
         car^#(l),
         cadr^#(l),
         cddr^#(l)) }

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

Strict DPs:
  { plus^#(x, y) -> c_1(ifplus^#(isZero(x), x, y))
  , ifplus^#(false(), x, y) -> c_2(plus^#(p(x), y))
  , times^#(x, y) -> c_3(iftimes^#(isZero(x), x, y))
  , iftimes^#(false(), x, y) ->
    c_4(plus^#(y, times(p(x), y)), times^#(p(x), y))
  , shorter^#(cons(x, l), s(y)) -> c_5(shorter^#(l, y))
  , prod^#(l) ->
    c_6(if^#(shorter(l, 0()), shorter(l, s(0())), l),
        shorter^#(l, s(0())))
  , if^#(false(), b, l) -> c_7(if2^#(b, l))
  , if2^#(false(), l) ->
    c_8(prod^#(cons(times(car(l), cadr(l)), cddr(l))),
        times^#(car(l), cadr(l))) }
Weak Trs:
  { car(cons(x, l)) -> x
  , cddr(cons(x, cons(y, l))) -> l
  , cddr(cons(x, nil())) -> nil()
  , cddr(nil()) -> nil()
  , cadr(cons(x, cons(y, l))) -> y
  , isZero(0()) -> true()
  , isZero(s(x)) -> false()
  , plus(x, y) -> ifplus(isZero(x), x, y)
  , ifplus(true(), x, y) -> y
  , ifplus(false(), x, y) -> s(plus(p(x), y))
  , p(0()) -> 0()
  , p(s(x)) -> x
  , times(x, y) -> iftimes(isZero(x), x, y)
  , iftimes(true(), x, y) -> 0()
  , iftimes(false(), x, y) -> plus(y, times(p(x), y))
  , shorter(cons(x, l), 0()) -> false()
  , shorter(cons(x, l), s(y)) -> shorter(l, y)
  , shorter(nil(), y) -> true()
  , prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l)
  , if(true(), b, l) -> s(0())
  , if(false(), b, l) -> if2(b, l)
  , if2(true(), l) -> car(l)
  , if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { car(cons(x, l)) -> x
    , cddr(cons(x, cons(y, l))) -> l
    , cddr(cons(x, nil())) -> nil()
    , cddr(nil()) -> nil()
    , cadr(cons(x, cons(y, l))) -> y
    , isZero(0()) -> true()
    , isZero(s(x)) -> false()
    , plus(x, y) -> ifplus(isZero(x), x, y)
    , ifplus(true(), x, y) -> y
    , ifplus(false(), x, y) -> s(plus(p(x), y))
    , p(0()) -> 0()
    , p(s(x)) -> x
    , times(x, y) -> iftimes(isZero(x), x, y)
    , iftimes(true(), x, y) -> 0()
    , iftimes(false(), x, y) -> plus(y, times(p(x), y))
    , shorter(cons(x, l), 0()) -> false()
    , shorter(cons(x, l), s(y)) -> shorter(l, y)
    , shorter(nil(), y) -> true() }

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

Strict DPs:
  { plus^#(x, y) -> c_1(ifplus^#(isZero(x), x, y))
  , ifplus^#(false(), x, y) -> c_2(plus^#(p(x), y))
  , times^#(x, y) -> c_3(iftimes^#(isZero(x), x, y))
  , iftimes^#(false(), x, y) ->
    c_4(plus^#(y, times(p(x), y)), times^#(p(x), y))
  , shorter^#(cons(x, l), s(y)) -> c_5(shorter^#(l, y))
  , prod^#(l) ->
    c_6(if^#(shorter(l, 0()), shorter(l, s(0())), l),
        shorter^#(l, s(0())))
  , if^#(false(), b, l) -> c_7(if2^#(b, l))
  , if2^#(false(), l) ->
    c_8(prod^#(cons(times(car(l), cadr(l)), cddr(l))),
        times^#(car(l), cadr(l))) }
Weak Trs:
  { car(cons(x, l)) -> x
  , cddr(cons(x, cons(y, l))) -> l
  , cddr(cons(x, nil())) -> nil()
  , cddr(nil()) -> nil()
  , cadr(cons(x, cons(y, l))) -> y
  , isZero(0()) -> true()
  , isZero(s(x)) -> false()
  , plus(x, y) -> ifplus(isZero(x), x, y)
  , ifplus(true(), x, y) -> y
  , ifplus(false(), x, y) -> s(plus(p(x), y))
  , p(0()) -> 0()
  , p(s(x)) -> x
  , times(x, y) -> iftimes(isZero(x), x, y)
  , iftimes(true(), x, y) -> 0()
  , iftimes(false(), x, y) -> plus(y, times(p(x), y))
  , shorter(cons(x, l), 0()) -> false()
  , shorter(cons(x, l), s(y)) -> shorter(l, y)
  , shorter(nil(), y) -> true() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..