MAYBE

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

Strict Trs:
  { a__from(X) -> cons(mark(X), from(s(X)))
  , a__from(X) -> from(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(from(X)) -> a__from(mark(X))
  , mark(s(X)) -> s(mark(X))
  , mark(0()) -> 0()
  , mark(rnil()) -> rnil()
  , mark(cons2(X1, X2)) -> cons2(X1, mark(X2))
  , mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2))
  , mark(posrecip(X)) -> posrecip(mark(X))
  , mark(negrecip(X)) -> negrecip(mark(X))
  , mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2))
  , mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2))
  , mark(pi(X)) -> a__pi(mark(X))
  , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
  , mark(times(X1, X2)) -> a__times(mark(X1), mark(X2))
  , mark(square(X)) -> a__square(mark(X))
  , mark(nil()) -> nil()
  , a__2ndspos(X1, X2) -> 2ndspos(X1, X2)
  , a__2ndspos(s(N), cons(X, Z)) ->
    a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
  , a__2ndspos(s(N), cons2(X, cons(Y, Z))) ->
    rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
  , a__2ndspos(0(), Z) -> rnil()
  , a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2)
  , a__2ndsneg(s(N), cons(X, Z)) ->
    a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
  , a__2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
    rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z)))
  , a__2ndsneg(0(), Z) -> rnil()
  , a__pi(X) -> a__2ndspos(mark(X), a__from(0()))
  , a__pi(X) -> pi(X)
  , a__plus(X1, X2) -> plus(X1, X2)
  , a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y)))
  , a__plus(0(), Y) -> mark(Y)
  , a__times(X1, X2) -> times(X1, X2)
  , a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y)))
  , a__times(0(), Y) -> 0()
  , a__square(X) -> a__times(mark(X), mark(X))
  , a__square(X) -> square(X) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { a__from^#(X) -> c_1(mark^#(X))
  , a__from^#(X) -> c_2()
  , mark^#(cons(X1, X2)) -> c_3(mark^#(X1))
  , mark^#(from(X)) -> c_4(a__from^#(mark(X)), mark^#(X))
  , mark^#(s(X)) -> c_5(mark^#(X))
  , mark^#(0()) -> c_6()
  , mark^#(rnil()) -> c_7()
  , mark^#(cons2(X1, X2)) -> c_8(mark^#(X2))
  , mark^#(rcons(X1, X2)) -> c_9(mark^#(X1), mark^#(X2))
  , mark^#(posrecip(X)) -> c_10(mark^#(X))
  , mark^#(negrecip(X)) -> c_11(mark^#(X))
  , mark^#(2ndspos(X1, X2)) ->
    c_12(a__2ndspos^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(2ndsneg(X1, X2)) ->
    c_13(a__2ndsneg^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(pi(X)) -> c_14(a__pi^#(mark(X)), mark^#(X))
  , mark^#(plus(X1, X2)) ->
    c_15(a__plus^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(times(X1, X2)) ->
    c_16(a__times^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(square(X)) -> c_17(a__square^#(mark(X)), mark^#(X))
  , mark^#(nil()) -> c_18()
  , a__2ndspos^#(X1, X2) -> c_19()
  , a__2ndspos^#(s(N), cons(X, Z)) ->
    c_20(a__2ndspos^#(s(mark(N)), cons2(X, mark(Z))),
         mark^#(N),
         mark^#(Z))
  , a__2ndspos^#(s(N), cons2(X, cons(Y, Z))) ->
    c_21(mark^#(Y),
         a__2ndsneg^#(mark(N), mark(Z)),
         mark^#(N),
         mark^#(Z))
  , a__2ndspos^#(0(), Z) -> c_22()
  , a__2ndsneg^#(X1, X2) -> c_23()
  , a__2ndsneg^#(s(N), cons(X, Z)) ->
    c_24(a__2ndsneg^#(s(mark(N)), cons2(X, mark(Z))),
         mark^#(N),
         mark^#(Z))
  , a__2ndsneg^#(s(N), cons2(X, cons(Y, Z))) ->
    c_25(mark^#(Y),
         a__2ndspos^#(mark(N), mark(Z)),
         mark^#(N),
         mark^#(Z))
  , a__2ndsneg^#(0(), Z) -> c_26()
  , a__pi^#(X) ->
    c_27(a__2ndspos^#(mark(X), a__from(0())),
         mark^#(X),
         a__from^#(0()))
  , a__pi^#(X) -> c_28()
  , a__plus^#(X1, X2) -> c_29()
  , a__plus^#(s(X), Y) ->
    c_30(a__plus^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
  , a__plus^#(0(), Y) -> c_31(mark^#(Y))
  , a__times^#(X1, X2) -> c_32()
  , a__times^#(s(X), Y) ->
    c_33(a__plus^#(mark(Y), a__times(mark(X), mark(Y))),
         mark^#(Y),
         a__times^#(mark(X), mark(Y)),
         mark^#(X),
         mark^#(Y))
  , a__times^#(0(), Y) -> c_34()
  , a__square^#(X) ->
    c_35(a__times^#(mark(X), mark(X)), mark^#(X), mark^#(X))
  , a__square^#(X) -> c_36() }

and mark the set of starting terms.

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

Strict DPs:
  { a__from^#(X) -> c_1(mark^#(X))
  , a__from^#(X) -> c_2()
  , mark^#(cons(X1, X2)) -> c_3(mark^#(X1))
  , mark^#(from(X)) -> c_4(a__from^#(mark(X)), mark^#(X))
  , mark^#(s(X)) -> c_5(mark^#(X))
  , mark^#(0()) -> c_6()
  , mark^#(rnil()) -> c_7()
  , mark^#(cons2(X1, X2)) -> c_8(mark^#(X2))
  , mark^#(rcons(X1, X2)) -> c_9(mark^#(X1), mark^#(X2))
  , mark^#(posrecip(X)) -> c_10(mark^#(X))
  , mark^#(negrecip(X)) -> c_11(mark^#(X))
  , mark^#(2ndspos(X1, X2)) ->
    c_12(a__2ndspos^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(2ndsneg(X1, X2)) ->
    c_13(a__2ndsneg^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(pi(X)) -> c_14(a__pi^#(mark(X)), mark^#(X))
  , mark^#(plus(X1, X2)) ->
    c_15(a__plus^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(times(X1, X2)) ->
    c_16(a__times^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(square(X)) -> c_17(a__square^#(mark(X)), mark^#(X))
  , mark^#(nil()) -> c_18()
  , a__2ndspos^#(X1, X2) -> c_19()
  , a__2ndspos^#(s(N), cons(X, Z)) ->
    c_20(a__2ndspos^#(s(mark(N)), cons2(X, mark(Z))),
         mark^#(N),
         mark^#(Z))
  , a__2ndspos^#(s(N), cons2(X, cons(Y, Z))) ->
    c_21(mark^#(Y),
         a__2ndsneg^#(mark(N), mark(Z)),
         mark^#(N),
         mark^#(Z))
  , a__2ndspos^#(0(), Z) -> c_22()
  , a__2ndsneg^#(X1, X2) -> c_23()
  , a__2ndsneg^#(s(N), cons(X, Z)) ->
    c_24(a__2ndsneg^#(s(mark(N)), cons2(X, mark(Z))),
         mark^#(N),
         mark^#(Z))
  , a__2ndsneg^#(s(N), cons2(X, cons(Y, Z))) ->
    c_25(mark^#(Y),
         a__2ndspos^#(mark(N), mark(Z)),
         mark^#(N),
         mark^#(Z))
  , a__2ndsneg^#(0(), Z) -> c_26()
  , a__pi^#(X) ->
    c_27(a__2ndspos^#(mark(X), a__from(0())),
         mark^#(X),
         a__from^#(0()))
  , a__pi^#(X) -> c_28()
  , a__plus^#(X1, X2) -> c_29()
  , a__plus^#(s(X), Y) ->
    c_30(a__plus^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
  , a__plus^#(0(), Y) -> c_31(mark^#(Y))
  , a__times^#(X1, X2) -> c_32()
  , a__times^#(s(X), Y) ->
    c_33(a__plus^#(mark(Y), a__times(mark(X), mark(Y))),
         mark^#(Y),
         a__times^#(mark(X), mark(Y)),
         mark^#(X),
         mark^#(Y))
  , a__times^#(0(), Y) -> c_34()
  , a__square^#(X) ->
    c_35(a__times^#(mark(X), mark(X)), mark^#(X), mark^#(X))
  , a__square^#(X) -> c_36() }
Weak Trs:
  { a__from(X) -> cons(mark(X), from(s(X)))
  , a__from(X) -> from(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(from(X)) -> a__from(mark(X))
  , mark(s(X)) -> s(mark(X))
  , mark(0()) -> 0()
  , mark(rnil()) -> rnil()
  , mark(cons2(X1, X2)) -> cons2(X1, mark(X2))
  , mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2))
  , mark(posrecip(X)) -> posrecip(mark(X))
  , mark(negrecip(X)) -> negrecip(mark(X))
  , mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2))
  , mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2))
  , mark(pi(X)) -> a__pi(mark(X))
  , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
  , mark(times(X1, X2)) -> a__times(mark(X1), mark(X2))
  , mark(square(X)) -> a__square(mark(X))
  , mark(nil()) -> nil()
  , a__2ndspos(X1, X2) -> 2ndspos(X1, X2)
  , a__2ndspos(s(N), cons(X, Z)) ->
    a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
  , a__2ndspos(s(N), cons2(X, cons(Y, Z))) ->
    rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
  , a__2ndspos(0(), Z) -> rnil()
  , a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2)
  , a__2ndsneg(s(N), cons(X, Z)) ->
    a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
  , a__2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
    rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z)))
  , a__2ndsneg(0(), Z) -> rnil()
  , a__pi(X) -> a__2ndspos(mark(X), a__from(0()))
  , a__pi(X) -> pi(X)
  , a__plus(X1, X2) -> plus(X1, X2)
  , a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y)))
  , a__plus(0(), Y) -> mark(Y)
  , a__times(X1, X2) -> times(X1, X2)
  , a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y)))
  , a__times(0(), Y) -> 0()
  , a__square(X) -> a__times(mark(X), mark(X))
  , a__square(X) -> square(X) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of
{2,6,7,18,19,22,23,26,28,29,32,34,36} by applications of
Pre({2,6,7,18,19,22,23,26,28,29,32,34,36}) =
{1,3,4,5,8,9,10,11,12,13,14,15,16,17,20,21,24,25,27,30,31,33,35}.
Here rules are labeled as follows:

  DPs:
    { 1: a__from^#(X) -> c_1(mark^#(X))
    , 2: a__from^#(X) -> c_2()
    , 3: mark^#(cons(X1, X2)) -> c_3(mark^#(X1))
    , 4: mark^#(from(X)) -> c_4(a__from^#(mark(X)), mark^#(X))
    , 5: mark^#(s(X)) -> c_5(mark^#(X))
    , 6: mark^#(0()) -> c_6()
    , 7: mark^#(rnil()) -> c_7()
    , 8: mark^#(cons2(X1, X2)) -> c_8(mark^#(X2))
    , 9: mark^#(rcons(X1, X2)) -> c_9(mark^#(X1), mark^#(X2))
    , 10: mark^#(posrecip(X)) -> c_10(mark^#(X))
    , 11: mark^#(negrecip(X)) -> c_11(mark^#(X))
    , 12: mark^#(2ndspos(X1, X2)) ->
          c_12(a__2ndspos^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 13: mark^#(2ndsneg(X1, X2)) ->
          c_13(a__2ndsneg^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 14: mark^#(pi(X)) -> c_14(a__pi^#(mark(X)), mark^#(X))
    , 15: mark^#(plus(X1, X2)) ->
          c_15(a__plus^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 16: mark^#(times(X1, X2)) ->
          c_16(a__times^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
    , 17: mark^#(square(X)) -> c_17(a__square^#(mark(X)), mark^#(X))
    , 18: mark^#(nil()) -> c_18()
    , 19: a__2ndspos^#(X1, X2) -> c_19()
    , 20: a__2ndspos^#(s(N), cons(X, Z)) ->
          c_20(a__2ndspos^#(s(mark(N)), cons2(X, mark(Z))),
               mark^#(N),
               mark^#(Z))
    , 21: a__2ndspos^#(s(N), cons2(X, cons(Y, Z))) ->
          c_21(mark^#(Y),
               a__2ndsneg^#(mark(N), mark(Z)),
               mark^#(N),
               mark^#(Z))
    , 22: a__2ndspos^#(0(), Z) -> c_22()
    , 23: a__2ndsneg^#(X1, X2) -> c_23()
    , 24: a__2ndsneg^#(s(N), cons(X, Z)) ->
          c_24(a__2ndsneg^#(s(mark(N)), cons2(X, mark(Z))),
               mark^#(N),
               mark^#(Z))
    , 25: a__2ndsneg^#(s(N), cons2(X, cons(Y, Z))) ->
          c_25(mark^#(Y),
               a__2ndspos^#(mark(N), mark(Z)),
               mark^#(N),
               mark^#(Z))
    , 26: a__2ndsneg^#(0(), Z) -> c_26()
    , 27: a__pi^#(X) ->
          c_27(a__2ndspos^#(mark(X), a__from(0())),
               mark^#(X),
               a__from^#(0()))
    , 28: a__pi^#(X) -> c_28()
    , 29: a__plus^#(X1, X2) -> c_29()
    , 30: a__plus^#(s(X), Y) ->
          c_30(a__plus^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
    , 31: a__plus^#(0(), Y) -> c_31(mark^#(Y))
    , 32: a__times^#(X1, X2) -> c_32()
    , 33: a__times^#(s(X), Y) ->
          c_33(a__plus^#(mark(Y), a__times(mark(X), mark(Y))),
               mark^#(Y),
               a__times^#(mark(X), mark(Y)),
               mark^#(X),
               mark^#(Y))
    , 34: a__times^#(0(), Y) -> c_34()
    , 35: a__square^#(X) ->
          c_35(a__times^#(mark(X), mark(X)), mark^#(X), mark^#(X))
    , 36: a__square^#(X) -> c_36() }

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

Strict DPs:
  { a__from^#(X) -> c_1(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_3(mark^#(X1))
  , mark^#(from(X)) -> c_4(a__from^#(mark(X)), mark^#(X))
  , mark^#(s(X)) -> c_5(mark^#(X))
  , mark^#(cons2(X1, X2)) -> c_8(mark^#(X2))
  , mark^#(rcons(X1, X2)) -> c_9(mark^#(X1), mark^#(X2))
  , mark^#(posrecip(X)) -> c_10(mark^#(X))
  , mark^#(negrecip(X)) -> c_11(mark^#(X))
  , mark^#(2ndspos(X1, X2)) ->
    c_12(a__2ndspos^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(2ndsneg(X1, X2)) ->
    c_13(a__2ndsneg^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(pi(X)) -> c_14(a__pi^#(mark(X)), mark^#(X))
  , mark^#(plus(X1, X2)) ->
    c_15(a__plus^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(times(X1, X2)) ->
    c_16(a__times^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(square(X)) -> c_17(a__square^#(mark(X)), mark^#(X))
  , a__2ndspos^#(s(N), cons(X, Z)) ->
    c_20(a__2ndspos^#(s(mark(N)), cons2(X, mark(Z))),
         mark^#(N),
         mark^#(Z))
  , a__2ndspos^#(s(N), cons2(X, cons(Y, Z))) ->
    c_21(mark^#(Y),
         a__2ndsneg^#(mark(N), mark(Z)),
         mark^#(N),
         mark^#(Z))
  , a__2ndsneg^#(s(N), cons(X, Z)) ->
    c_24(a__2ndsneg^#(s(mark(N)), cons2(X, mark(Z))),
         mark^#(N),
         mark^#(Z))
  , a__2ndsneg^#(s(N), cons2(X, cons(Y, Z))) ->
    c_25(mark^#(Y),
         a__2ndspos^#(mark(N), mark(Z)),
         mark^#(N),
         mark^#(Z))
  , a__pi^#(X) ->
    c_27(a__2ndspos^#(mark(X), a__from(0())),
         mark^#(X),
         a__from^#(0()))
  , a__plus^#(s(X), Y) ->
    c_30(a__plus^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
  , a__plus^#(0(), Y) -> c_31(mark^#(Y))
  , a__times^#(s(X), Y) ->
    c_33(a__plus^#(mark(Y), a__times(mark(X), mark(Y))),
         mark^#(Y),
         a__times^#(mark(X), mark(Y)),
         mark^#(X),
         mark^#(Y))
  , a__square^#(X) ->
    c_35(a__times^#(mark(X), mark(X)), mark^#(X), mark^#(X)) }
Weak DPs:
  { a__from^#(X) -> c_2()
  , mark^#(0()) -> c_6()
  , mark^#(rnil()) -> c_7()
  , mark^#(nil()) -> c_18()
  , a__2ndspos^#(X1, X2) -> c_19()
  , a__2ndspos^#(0(), Z) -> c_22()
  , a__2ndsneg^#(X1, X2) -> c_23()
  , a__2ndsneg^#(0(), Z) -> c_26()
  , a__pi^#(X) -> c_28()
  , a__plus^#(X1, X2) -> c_29()
  , a__times^#(X1, X2) -> c_32()
  , a__times^#(0(), Y) -> c_34()
  , a__square^#(X) -> c_36() }
Weak Trs:
  { a__from(X) -> cons(mark(X), from(s(X)))
  , a__from(X) -> from(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(from(X)) -> a__from(mark(X))
  , mark(s(X)) -> s(mark(X))
  , mark(0()) -> 0()
  , mark(rnil()) -> rnil()
  , mark(cons2(X1, X2)) -> cons2(X1, mark(X2))
  , mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2))
  , mark(posrecip(X)) -> posrecip(mark(X))
  , mark(negrecip(X)) -> negrecip(mark(X))
  , mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2))
  , mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2))
  , mark(pi(X)) -> a__pi(mark(X))
  , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
  , mark(times(X1, X2)) -> a__times(mark(X1), mark(X2))
  , mark(square(X)) -> a__square(mark(X))
  , mark(nil()) -> nil()
  , a__2ndspos(X1, X2) -> 2ndspos(X1, X2)
  , a__2ndspos(s(N), cons(X, Z)) ->
    a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
  , a__2ndspos(s(N), cons2(X, cons(Y, Z))) ->
    rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
  , a__2ndspos(0(), Z) -> rnil()
  , a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2)
  , a__2ndsneg(s(N), cons(X, Z)) ->
    a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
  , a__2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
    rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z)))
  , a__2ndsneg(0(), Z) -> rnil()
  , a__pi(X) -> a__2ndspos(mark(X), a__from(0()))
  , a__pi(X) -> pi(X)
  , a__plus(X1, X2) -> plus(X1, X2)
  , a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y)))
  , a__plus(0(), Y) -> mark(Y)
  , a__times(X1, X2) -> times(X1, X2)
  , a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y)))
  , a__times(0(), Y) -> 0()
  , a__square(X) -> a__times(mark(X), mark(X))
  , a__square(X) -> square(X) }
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.

{ a__from^#(X) -> c_2()
, mark^#(0()) -> c_6()
, mark^#(rnil()) -> c_7()
, mark^#(nil()) -> c_18()
, a__2ndspos^#(X1, X2) -> c_19()
, a__2ndspos^#(0(), Z) -> c_22()
, a__2ndsneg^#(X1, X2) -> c_23()
, a__2ndsneg^#(0(), Z) -> c_26()
, a__pi^#(X) -> c_28()
, a__plus^#(X1, X2) -> c_29()
, a__times^#(X1, X2) -> c_32()
, a__times^#(0(), Y) -> c_34()
, a__square^#(X) -> c_36() }

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

Strict DPs:
  { a__from^#(X) -> c_1(mark^#(X))
  , mark^#(cons(X1, X2)) -> c_3(mark^#(X1))
  , mark^#(from(X)) -> c_4(a__from^#(mark(X)), mark^#(X))
  , mark^#(s(X)) -> c_5(mark^#(X))
  , mark^#(cons2(X1, X2)) -> c_8(mark^#(X2))
  , mark^#(rcons(X1, X2)) -> c_9(mark^#(X1), mark^#(X2))
  , mark^#(posrecip(X)) -> c_10(mark^#(X))
  , mark^#(negrecip(X)) -> c_11(mark^#(X))
  , mark^#(2ndspos(X1, X2)) ->
    c_12(a__2ndspos^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(2ndsneg(X1, X2)) ->
    c_13(a__2ndsneg^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(pi(X)) -> c_14(a__pi^#(mark(X)), mark^#(X))
  , mark^#(plus(X1, X2)) ->
    c_15(a__plus^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(times(X1, X2)) ->
    c_16(a__times^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2))
  , mark^#(square(X)) -> c_17(a__square^#(mark(X)), mark^#(X))
  , a__2ndspos^#(s(N), cons(X, Z)) ->
    c_20(a__2ndspos^#(s(mark(N)), cons2(X, mark(Z))),
         mark^#(N),
         mark^#(Z))
  , a__2ndspos^#(s(N), cons2(X, cons(Y, Z))) ->
    c_21(mark^#(Y),
         a__2ndsneg^#(mark(N), mark(Z)),
         mark^#(N),
         mark^#(Z))
  , a__2ndsneg^#(s(N), cons(X, Z)) ->
    c_24(a__2ndsneg^#(s(mark(N)), cons2(X, mark(Z))),
         mark^#(N),
         mark^#(Z))
  , a__2ndsneg^#(s(N), cons2(X, cons(Y, Z))) ->
    c_25(mark^#(Y),
         a__2ndspos^#(mark(N), mark(Z)),
         mark^#(N),
         mark^#(Z))
  , a__pi^#(X) ->
    c_27(a__2ndspos^#(mark(X), a__from(0())),
         mark^#(X),
         a__from^#(0()))
  , a__plus^#(s(X), Y) ->
    c_30(a__plus^#(mark(X), mark(Y)), mark^#(X), mark^#(Y))
  , a__plus^#(0(), Y) -> c_31(mark^#(Y))
  , a__times^#(s(X), Y) ->
    c_33(a__plus^#(mark(Y), a__times(mark(X), mark(Y))),
         mark^#(Y),
         a__times^#(mark(X), mark(Y)),
         mark^#(X),
         mark^#(Y))
  , a__square^#(X) ->
    c_35(a__times^#(mark(X), mark(X)), mark^#(X), mark^#(X)) }
Weak Trs:
  { a__from(X) -> cons(mark(X), from(s(X)))
  , a__from(X) -> from(X)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(from(X)) -> a__from(mark(X))
  , mark(s(X)) -> s(mark(X))
  , mark(0()) -> 0()
  , mark(rnil()) -> rnil()
  , mark(cons2(X1, X2)) -> cons2(X1, mark(X2))
  , mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2))
  , mark(posrecip(X)) -> posrecip(mark(X))
  , mark(negrecip(X)) -> negrecip(mark(X))
  , mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2))
  , mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2))
  , mark(pi(X)) -> a__pi(mark(X))
  , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
  , mark(times(X1, X2)) -> a__times(mark(X1), mark(X2))
  , mark(square(X)) -> a__square(mark(X))
  , mark(nil()) -> nil()
  , a__2ndspos(X1, X2) -> 2ndspos(X1, X2)
  , a__2ndspos(s(N), cons(X, Z)) ->
    a__2ndspos(s(mark(N)), cons2(X, mark(Z)))
  , a__2ndspos(s(N), cons2(X, cons(Y, Z))) ->
    rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z)))
  , a__2ndspos(0(), Z) -> rnil()
  , a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2)
  , a__2ndsneg(s(N), cons(X, Z)) ->
    a__2ndsneg(s(mark(N)), cons2(X, mark(Z)))
  , a__2ndsneg(s(N), cons2(X, cons(Y, Z))) ->
    rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z)))
  , a__2ndsneg(0(), Z) -> rnil()
  , a__pi(X) -> a__2ndspos(mark(X), a__from(0()))
  , a__pi(X) -> pi(X)
  , a__plus(X1, X2) -> plus(X1, X2)
  , a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y)))
  , a__plus(0(), Y) -> mark(Y)
  , a__times(X1, X2) -> times(X1, X2)
  , a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y)))
  , a__times(0(), Y) -> 0()
  , a__square(X) -> a__times(mark(X), mark(X))
  , a__square(X) -> square(X) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..