MAYBE

Problem:
 a__terms(N) -> cons(recip(a__sqr(mark(N))),terms(s(N)))
 a__sqr(0()) -> 0()
 a__sqr(s(X)) -> s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))
 a__dbl(0()) -> 0()
 a__dbl(s(X)) -> s(s(a__dbl(mark(X))))
 a__add(0(),X) -> mark(X)
 a__add(s(X),Y) -> s(a__add(mark(X),mark(Y)))
 a__first(0(),X) -> nil()
 a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z))
 a__half(0()) -> 0()
 a__half(s(0())) -> 0()
 a__half(s(s(X))) -> s(a__half(mark(X)))
 a__half(dbl(X)) -> mark(X)
 mark(terms(X)) -> a__terms(mark(X))
 mark(sqr(X)) -> a__sqr(mark(X))
 mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
 mark(dbl(X)) -> a__dbl(mark(X))
 mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
 mark(half(X)) -> a__half(mark(X))
 mark(cons(X1,X2)) -> cons(mark(X1),X2)
 mark(recip(X)) -> recip(mark(X))
 mark(s(X)) -> s(mark(X))
 mark(0()) -> 0()
 mark(nil()) -> nil()
 a__terms(X) -> terms(X)
 a__sqr(X) -> sqr(X)
 a__add(X1,X2) -> add(X1,X2)
 a__dbl(X) -> dbl(X)
 a__first(X1,X2) -> first(X1,X2)
 a__half(X) -> half(X)

Proof:
 DP Processor:
  DPs:
   a__terms#(N) -> mark#(N)
   a__terms#(N) -> a__sqr#(mark(N))
   a__sqr#(s(X)) -> a__dbl#(mark(X))
   a__sqr#(s(X)) -> mark#(X)
   a__sqr#(s(X)) -> a__sqr#(mark(X))
   a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)),a__dbl(mark(X)))
   a__dbl#(s(X)) -> mark#(X)
   a__dbl#(s(X)) -> a__dbl#(mark(X))
   a__add#(0(),X) -> mark#(X)
   a__add#(s(X),Y) -> mark#(Y)
   a__add#(s(X),Y) -> mark#(X)
   a__add#(s(X),Y) -> a__add#(mark(X),mark(Y))
   a__first#(s(X),cons(Y,Z)) -> mark#(Y)
   a__half#(s(s(X))) -> mark#(X)
   a__half#(s(s(X))) -> a__half#(mark(X))
   a__half#(dbl(X)) -> mark#(X)
   mark#(terms(X)) -> mark#(X)
   mark#(terms(X)) -> a__terms#(mark(X))
   mark#(sqr(X)) -> mark#(X)
   mark#(sqr(X)) -> a__sqr#(mark(X))
   mark#(add(X1,X2)) -> mark#(X2)
   mark#(add(X1,X2)) -> mark#(X1)
   mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
   mark#(dbl(X)) -> mark#(X)
   mark#(dbl(X)) -> a__dbl#(mark(X))
   mark#(first(X1,X2)) -> mark#(X2)
   mark#(first(X1,X2)) -> mark#(X1)
   mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
   mark#(half(X)) -> mark#(X)
   mark#(half(X)) -> a__half#(mark(X))
   mark#(cons(X1,X2)) -> mark#(X1)
   mark#(recip(X)) -> mark#(X)
   mark#(s(X)) -> mark#(X)
  TRS:
   a__terms(N) -> cons(recip(a__sqr(mark(N))),terms(s(N)))
   a__sqr(0()) -> 0()
   a__sqr(s(X)) -> s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))
   a__dbl(0()) -> 0()
   a__dbl(s(X)) -> s(s(a__dbl(mark(X))))
   a__add(0(),X) -> mark(X)
   a__add(s(X),Y) -> s(a__add(mark(X),mark(Y)))
   a__first(0(),X) -> nil()
   a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z))
   a__half(0()) -> 0()
   a__half(s(0())) -> 0()
   a__half(s(s(X))) -> s(a__half(mark(X)))
   a__half(dbl(X)) -> mark(X)
   mark(terms(X)) -> a__terms(mark(X))
   mark(sqr(X)) -> a__sqr(mark(X))
   mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
   mark(dbl(X)) -> a__dbl(mark(X))
   mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
   mark(half(X)) -> a__half(mark(X))
   mark(cons(X1,X2)) -> cons(mark(X1),X2)
   mark(recip(X)) -> recip(mark(X))
   mark(s(X)) -> s(mark(X))
   mark(0()) -> 0()
   mark(nil()) -> nil()
   a__terms(X) -> terms(X)
   a__sqr(X) -> sqr(X)
   a__add(X1,X2) -> add(X1,X2)
   a__dbl(X) -> dbl(X)
   a__first(X1,X2) -> first(X1,X2)
   a__half(X) -> half(X)
  CDG Processor:
   DPs:
    a__terms#(N) -> mark#(N)
    a__terms#(N) -> a__sqr#(mark(N))
    a__sqr#(s(X)) -> a__dbl#(mark(X))
    a__sqr#(s(X)) -> mark#(X)
    a__sqr#(s(X)) -> a__sqr#(mark(X))
    a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)),a__dbl(mark(X)))
    a__dbl#(s(X)) -> mark#(X)
    a__dbl#(s(X)) -> a__dbl#(mark(X))
    a__add#(0(),X) -> mark#(X)
    a__add#(s(X),Y) -> mark#(Y)
    a__add#(s(X),Y) -> mark#(X)
    a__add#(s(X),Y) -> a__add#(mark(X),mark(Y))
    a__first#(s(X),cons(Y,Z)) -> mark#(Y)
    a__half#(s(s(X))) -> mark#(X)
    a__half#(s(s(X))) -> a__half#(mark(X))
    a__half#(dbl(X)) -> mark#(X)
    mark#(terms(X)) -> mark#(X)
    mark#(terms(X)) -> a__terms#(mark(X))
    mark#(sqr(X)) -> mark#(X)
    mark#(sqr(X)) -> a__sqr#(mark(X))
    mark#(add(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(dbl(X)) -> mark#(X)
    mark#(dbl(X)) -> a__dbl#(mark(X))
    mark#(first(X1,X2)) -> mark#(X2)
    mark#(first(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    mark#(half(X)) -> mark#(X)
    mark#(half(X)) -> a__half#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(recip(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X)
   TRS:
    a__terms(N) -> cons(recip(a__sqr(mark(N))),terms(s(N)))
    a__sqr(0()) -> 0()
    a__sqr(s(X)) -> s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))
    a__dbl(0()) -> 0()
    a__dbl(s(X)) -> s(s(a__dbl(mark(X))))
    a__add(0(),X) -> mark(X)
    a__add(s(X),Y) -> s(a__add(mark(X),mark(Y)))
    a__first(0(),X) -> nil()
    a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z))
    a__half(0()) -> 0()
    a__half(s(0())) -> 0()
    a__half(s(s(X))) -> s(a__half(mark(X)))
    a__half(dbl(X)) -> mark(X)
    mark(terms(X)) -> a__terms(mark(X))
    mark(sqr(X)) -> a__sqr(mark(X))
    mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
    mark(dbl(X)) -> a__dbl(mark(X))
    mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
    mark(half(X)) -> a__half(mark(X))
    mark(cons(X1,X2)) -> cons(mark(X1),X2)
    mark(recip(X)) -> recip(mark(X))
    mark(s(X)) -> s(mark(X))
    mark(0()) -> 0()
    mark(nil()) -> nil()
    a__terms(X) -> terms(X)
    a__sqr(X) -> sqr(X)
    a__add(X1,X2) -> add(X1,X2)
    a__dbl(X) -> dbl(X)
    a__first(X1,X2) -> first(X1,X2)
    a__half(X) -> half(X)
   graph:
    a__half#(dbl(X)) -> mark#(X) -> mark#(terms(X)) -> mark#(X)
    a__half#(dbl(X)) -> mark#(X) ->
    mark#(terms(X)) -> a__terms#(mark(X))
    a__half#(dbl(X)) -> mark#(X) -> mark#(sqr(X)) -> mark#(X)
    a__half#(dbl(X)) -> mark#(X) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    a__half#(dbl(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    a__half#(dbl(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    a__half#(dbl(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    a__half#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    a__half#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    a__half#(dbl(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2)
    a__half#(dbl(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1)
    a__half#(dbl(X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    a__half#(dbl(X)) -> mark#(X) -> mark#(half(X)) -> mark#(X)
    a__half#(dbl(X)) -> mark#(X) -> mark#(half(X)) -> a__half#(mark(X))
    a__half#(dbl(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    a__half#(dbl(X)) -> mark#(X) -> mark#(recip(X)) -> mark#(X)
    a__half#(dbl(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__half#(s(s(X))) -> a__half#(mark(X)) ->
    a__half#(s(s(X))) -> mark#(X)
    a__half#(s(s(X))) -> a__half#(mark(X)) ->
    a__half#(s(s(X))) -> a__half#(mark(X))
    a__half#(s(s(X))) -> a__half#(mark(X)) ->
    a__half#(dbl(X)) -> mark#(X)
    a__half#(s(s(X))) -> mark#(X) -> mark#(terms(X)) -> mark#(X)
    a__half#(s(s(X))) -> mark#(X) ->
    mark#(terms(X)) -> a__terms#(mark(X))
    a__half#(s(s(X))) -> mark#(X) -> mark#(sqr(X)) -> mark#(X)
    a__half#(s(s(X))) -> mark#(X) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    a__half#(s(s(X))) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    a__half#(s(s(X))) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    a__half#(s(s(X))) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    a__half#(s(s(X))) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    a__half#(s(s(X))) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    a__half#(s(s(X))) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2)
    a__half#(s(s(X))) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1)
    a__half#(s(s(X))) -> mark#(X) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    a__half#(s(s(X))) -> mark#(X) -> mark#(half(X)) -> mark#(X)
    a__half#(s(s(X))) -> mark#(X) ->
    mark#(half(X)) -> a__half#(mark(X))
    a__half#(s(s(X))) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    a__half#(s(s(X))) -> mark#(X) -> mark#(recip(X)) -> mark#(X)
    a__half#(s(s(X))) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(terms(X)) -> mark#(X)
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(terms(X)) -> a__terms#(mark(X))
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(sqr(X)) -> mark#(X)
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(sqr(X)) -> a__sqr#(mark(X))
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(add(X1,X2)) -> mark#(X2)
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(add(X1,X2)) -> mark#(X1)
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(dbl(X)) -> mark#(X)
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(dbl(X)) -> a__dbl#(mark(X))
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(first(X1,X2)) -> mark#(X2)
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(first(X1,X2)) -> mark#(X1)
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(half(X)) -> mark#(X)
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(half(X)) -> a__half#(mark(X))
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) ->
    mark#(recip(X)) -> mark#(X)
    a__first#(s(X),cons(Y,Z)) -> mark#(Y) -> mark#(s(X)) -> mark#(X)
    a__add#(0(),X) -> mark#(X) -> mark#(terms(X)) -> mark#(X)
    a__add#(0(),X) -> mark#(X) -> mark#(terms(X)) -> a__terms#(mark(X))
    a__add#(0(),X) -> mark#(X) -> mark#(sqr(X)) -> mark#(X)
    a__add#(0(),X) -> mark#(X) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    a__add#(0(),X) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    a__add#(0(),X) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    a__add#(0(),X) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    a__add#(0(),X) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    a__add#(0(),X) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    a__add#(0(),X) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2)
    a__add#(0(),X) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1)
    a__add#(0(),X) -> mark#(X) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    a__add#(0(),X) -> mark#(X) -> mark#(half(X)) -> mark#(X)
    a__add#(0(),X) -> mark#(X) -> mark#(half(X)) -> a__half#(mark(X))
    a__add#(0(),X) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    a__add#(0(),X) -> mark#(X) -> mark#(recip(X)) -> mark#(X)
    a__add#(0(),X) -> mark#(X) ->
    mark#(s(X)) -> mark#(X)
    a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) ->
    a__add#(0(),X) -> mark#(X)
    a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) ->
    a__add#(s(X),Y) -> mark#(Y)
    a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) ->
    a__add#(s(X),Y) -> mark#(X)
    a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) ->
    a__add#(s(X),Y) -> a__add#(mark(X),mark(Y))
    a__add#(s(X),Y) -> mark#(Y) -> mark#(terms(X)) -> mark#(X)
    a__add#(s(X),Y) -> mark#(Y) -> mark#(terms(X)) -> a__terms#(mark(X))
    a__add#(s(X),Y) -> mark#(Y) -> mark#(sqr(X)) -> mark#(X)
    a__add#(s(X),Y) -> mark#(Y) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    a__add#(s(X),Y) -> mark#(Y) -> mark#(add(X1,X2)) -> mark#(X2)
    a__add#(s(X),Y) -> mark#(Y) -> mark#(add(X1,X2)) -> mark#(X1)
    a__add#(s(X),Y) -> mark#(Y) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    a__add#(s(X),Y) -> mark#(Y) -> mark#(dbl(X)) -> mark#(X)
    a__add#(s(X),Y) -> mark#(Y) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    a__add#(s(X),Y) -> mark#(Y) -> mark#(first(X1,X2)) -> mark#(X2)
    a__add#(s(X),Y) -> mark#(Y) -> mark#(first(X1,X2)) -> mark#(X1)
    a__add#(s(X),Y) -> mark#(Y) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    a__add#(s(X),Y) -> mark#(Y) -> mark#(half(X)) -> mark#(X)
    a__add#(s(X),Y) -> mark#(Y) -> mark#(half(X)) -> a__half#(mark(X))
    a__add#(s(X),Y) -> mark#(Y) -> mark#(cons(X1,X2)) -> mark#(X1)
    a__add#(s(X),Y) -> mark#(Y) -> mark#(recip(X)) -> mark#(X)
    a__add#(s(X),Y) -> mark#(Y) -> mark#(s(X)) -> mark#(X)
    a__add#(s(X),Y) -> mark#(X) -> mark#(terms(X)) -> mark#(X)
    a__add#(s(X),Y) -> mark#(X) -> mark#(terms(X)) -> a__terms#(mark(X))
    a__add#(s(X),Y) -> mark#(X) -> mark#(sqr(X)) -> mark#(X)
    a__add#(s(X),Y) -> mark#(X) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    a__add#(s(X),Y) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    a__add#(s(X),Y) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    a__add#(s(X),Y) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    a__add#(s(X),Y) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    a__add#(s(X),Y) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    a__add#(s(X),Y) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2)
    a__add#(s(X),Y) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1)
    a__add#(s(X),Y) -> mark#(X) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    a__add#(s(X),Y) -> mark#(X) -> mark#(half(X)) -> mark#(X)
    a__add#(s(X),Y) -> mark#(X) -> mark#(half(X)) -> a__half#(mark(X))
    a__add#(s(X),Y) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    a__add#(s(X),Y) -> mark#(X) -> mark#(recip(X)) -> mark#(X)
    a__add#(s(X),Y) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__dbl#(s(X)) -> a__dbl#(mark(X)) -> a__dbl#(s(X)) -> mark#(X)
    a__dbl#(s(X)) -> a__dbl#(mark(X)) -> a__dbl#(s(X)) -> a__dbl#(mark(X))
    a__dbl#(s(X)) -> mark#(X) -> mark#(terms(X)) -> mark#(X)
    a__dbl#(s(X)) -> mark#(X) -> mark#(terms(X)) -> a__terms#(mark(X))
    a__dbl#(s(X)) -> mark#(X) -> mark#(sqr(X)) -> mark#(X)
    a__dbl#(s(X)) -> mark#(X) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    a__dbl#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    a__dbl#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    a__dbl#(s(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    a__dbl#(s(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    a__dbl#(s(X)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    a__dbl#(s(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2)
    a__dbl#(s(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1)
    a__dbl#(s(X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    a__dbl#(s(X)) -> mark#(X) -> mark#(half(X)) -> mark#(X)
    a__dbl#(s(X)) -> mark#(X) -> mark#(half(X)) -> a__half#(mark(X))
    a__dbl#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    a__dbl#(s(X)) -> mark#(X) -> mark#(recip(X)) -> mark#(X)
    a__dbl#(s(X)) -> mark#(X) ->
    mark#(s(X)) -> mark#(X)
    a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)),a__dbl(mark(X))) ->
    a__add#(0(),X) -> mark#(X)
    a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)),a__dbl(mark(X))) ->
    a__add#(s(X),Y) -> mark#(Y)
    a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)),a__dbl(mark(X))) ->
    a__add#(s(X),Y) -> mark#(X)
    a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)),a__dbl(mark(X))) ->
    a__add#(s(X),Y) -> a__add#(mark(X),mark(Y))
    a__sqr#(s(X)) -> a__dbl#(mark(X)) -> a__dbl#(s(X)) -> mark#(X)
    a__sqr#(s(X)) -> a__dbl#(mark(X)) ->
    a__dbl#(s(X)) -> a__dbl#(mark(X))
    a__sqr#(s(X)) -> a__sqr#(mark(X)) ->
    a__sqr#(s(X)) -> a__dbl#(mark(X))
    a__sqr#(s(X)) -> a__sqr#(mark(X)) -> a__sqr#(s(X)) -> mark#(X)
    a__sqr#(s(X)) -> a__sqr#(mark(X)) ->
    a__sqr#(s(X)) -> a__sqr#(mark(X))
    a__sqr#(s(X)) -> a__sqr#(mark(X)) ->
    a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)),a__dbl(mark(X)))
    a__sqr#(s(X)) -> mark#(X) -> mark#(terms(X)) -> mark#(X)
    a__sqr#(s(X)) -> mark#(X) -> mark#(terms(X)) -> a__terms#(mark(X))
    a__sqr#(s(X)) -> mark#(X) -> mark#(sqr(X)) -> mark#(X)
    a__sqr#(s(X)) -> mark#(X) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    a__sqr#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    a__sqr#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    a__sqr#(s(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    a__sqr#(s(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    a__sqr#(s(X)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    a__sqr#(s(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2)
    a__sqr#(s(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1)
    a__sqr#(s(X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    a__sqr#(s(X)) -> mark#(X) -> mark#(half(X)) -> mark#(X)
    a__sqr#(s(X)) -> mark#(X) -> mark#(half(X)) -> a__half#(mark(X))
    a__sqr#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    a__sqr#(s(X)) -> mark#(X) -> mark#(recip(X)) -> mark#(X)
    a__sqr#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(half(X)) -> a__half#(mark(X)) ->
    a__half#(s(s(X))) -> mark#(X)
    mark#(half(X)) -> a__half#(mark(X)) ->
    a__half#(s(s(X))) -> a__half#(mark(X))
    mark#(half(X)) -> a__half#(mark(X)) -> a__half#(dbl(X)) -> mark#(X)
    mark#(half(X)) -> mark#(X) -> mark#(terms(X)) -> mark#(X)
    mark#(half(X)) -> mark#(X) -> mark#(terms(X)) -> a__terms#(mark(X))
    mark#(half(X)) -> mark#(X) -> mark#(sqr(X)) -> mark#(X)
    mark#(half(X)) -> mark#(X) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    mark#(half(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(half(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(half(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(half(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    mark#(half(X)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    mark#(half(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2)
    mark#(half(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1)
    mark#(half(X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    mark#(half(X)) -> mark#(X) -> mark#(half(X)) -> mark#(X)
    mark#(half(X)) -> mark#(X) -> mark#(half(X)) -> a__half#(mark(X))
    mark#(half(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(half(X)) -> mark#(X) -> mark#(recip(X)) -> mark#(X)
    mark#(half(X)) -> mark#(X) ->
    mark#(s(X)) -> mark#(X)
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) ->
    a__add#(0(),X) -> mark#(X)
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) ->
    a__add#(s(X),Y) -> mark#(Y)
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) ->
    a__add#(s(X),Y) -> mark#(X)
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) ->
    a__add#(s(X),Y) -> a__add#(mark(X),mark(Y))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(terms(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(terms(X)) -> a__terms#(mark(X))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(sqr(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(sqr(X)) -> a__sqr#(mark(X))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(dbl(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(dbl(X)) -> a__dbl#(mark(X))
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(first(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(first(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(half(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(half(X)) -> a__half#(mark(X))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(recip(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(terms(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(terms(X)) -> a__terms#(mark(X))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(sqr(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(sqr(X)) -> a__sqr#(mark(X))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(dbl(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(dbl(X)) -> a__dbl#(mark(X))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(half(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(half(X)) -> a__half#(mark(X))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(recip(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(sqr(X)) -> a__sqr#(mark(X)) ->
    a__sqr#(s(X)) -> a__dbl#(mark(X))
    mark#(sqr(X)) -> a__sqr#(mark(X)) -> a__sqr#(s(X)) -> mark#(X)
    mark#(sqr(X)) -> a__sqr#(mark(X)) ->
    a__sqr#(s(X)) -> a__sqr#(mark(X))
    mark#(sqr(X)) -> a__sqr#(mark(X)) ->
    a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)),a__dbl(mark(X)))
    mark#(sqr(X)) -> mark#(X) -> mark#(terms(X)) -> mark#(X)
    mark#(sqr(X)) -> mark#(X) -> mark#(terms(X)) -> a__terms#(mark(X))
    mark#(sqr(X)) -> mark#(X) -> mark#(sqr(X)) -> mark#(X)
    mark#(sqr(X)) -> mark#(X) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    mark#(sqr(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(sqr(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(sqr(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(sqr(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    mark#(sqr(X)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    mark#(sqr(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2)
    mark#(sqr(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1)
    mark#(sqr(X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    mark#(sqr(X)) -> mark#(X) -> mark#(half(X)) -> mark#(X)
    mark#(sqr(X)) -> mark#(X) -> mark#(half(X)) -> a__half#(mark(X))
    mark#(sqr(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(sqr(X)) -> mark#(X) -> mark#(recip(X)) -> mark#(X)
    mark#(sqr(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(dbl(X)) -> a__dbl#(mark(X)) -> a__dbl#(s(X)) -> mark#(X)
    mark#(dbl(X)) -> a__dbl#(mark(X)) -> a__dbl#(s(X)) -> a__dbl#(mark(X))
    mark#(dbl(X)) -> mark#(X) -> mark#(terms(X)) -> mark#(X)
    mark#(dbl(X)) -> mark#(X) -> mark#(terms(X)) -> a__terms#(mark(X))
    mark#(dbl(X)) -> mark#(X) -> mark#(sqr(X)) -> mark#(X)
    mark#(dbl(X)) -> mark#(X) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    mark#(dbl(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(dbl(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(dbl(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    mark#(dbl(X)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    mark#(dbl(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2)
    mark#(dbl(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1)
    mark#(dbl(X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    mark#(dbl(X)) -> mark#(X) -> mark#(half(X)) -> mark#(X)
    mark#(dbl(X)) -> mark#(X) -> mark#(half(X)) -> a__half#(mark(X))
    mark#(dbl(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(dbl(X)) -> mark#(X) -> mark#(recip(X)) -> mark#(X)
    mark#(dbl(X)) -> mark#(X) ->
    mark#(s(X)) -> mark#(X)
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2)) ->
    a__first#(s(X),cons(Y,Z)) -> mark#(Y)
    mark#(first(X1,X2)) -> mark#(X2) -> mark#(terms(X)) -> mark#(X)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(terms(X)) -> a__terms#(mark(X))
    mark#(first(X1,X2)) -> mark#(X2) -> mark#(sqr(X)) -> mark#(X)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(sqr(X)) -> a__sqr#(mark(X))
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> mark#(X2)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(first(X1,X2)) -> mark#(X2) -> mark#(dbl(X)) -> mark#(X)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(dbl(X)) -> a__dbl#(mark(X))
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(first(X1,X2)) -> mark#(X2)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(first(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    mark#(first(X1,X2)) -> mark#(X2) -> mark#(half(X)) -> mark#(X)
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(half(X)) -> a__half#(mark(X))
    mark#(first(X1,X2)) -> mark#(X2) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X2) -> mark#(recip(X)) -> mark#(X)
    mark#(first(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
    mark#(first(X1,X2)) -> mark#(X1) -> mark#(terms(X)) -> mark#(X)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(terms(X)) -> a__terms#(mark(X))
    mark#(first(X1,X2)) -> mark#(X1) -> mark#(sqr(X)) -> mark#(X)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(sqr(X)) -> a__sqr#(mark(X))
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> mark#(X2)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(first(X1,X2)) -> mark#(X1) -> mark#(dbl(X)) -> mark#(X)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(dbl(X)) -> a__dbl#(mark(X))
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X2)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    mark#(first(X1,X2)) -> mark#(X1) -> mark#(half(X)) -> mark#(X)
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(half(X)) -> a__half#(mark(X))
    mark#(first(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(first(X1,X2)) -> mark#(X1) -> mark#(recip(X)) -> mark#(X)
    mark#(first(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(terms(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(terms(X)) -> a__terms#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(sqr(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(sqr(X)) -> a__sqr#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> mark#(X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(dbl(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(dbl(X)) -> a__dbl#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(half(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(half(X)) -> a__half#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(recip(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(terms(X)) -> mark#(X) -> mark#(terms(X)) -> mark#(X)
    mark#(terms(X)) -> mark#(X) -> mark#(terms(X)) -> a__terms#(mark(X))
    mark#(terms(X)) -> mark#(X) -> mark#(sqr(X)) -> mark#(X)
    mark#(terms(X)) -> mark#(X) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    mark#(terms(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(terms(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(terms(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(terms(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    mark#(terms(X)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    mark#(terms(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2)
    mark#(terms(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1)
    mark#(terms(X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    mark#(terms(X)) -> mark#(X) -> mark#(half(X)) -> mark#(X)
    mark#(terms(X)) -> mark#(X) -> mark#(half(X)) -> a__half#(mark(X))
    mark#(terms(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(terms(X)) -> mark#(X) -> mark#(recip(X)) -> mark#(X)
    mark#(terms(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(terms(X)) -> a__terms#(mark(X)) ->
    a__terms#(N) -> mark#(N)
    mark#(terms(X)) -> a__terms#(mark(X)) ->
    a__terms#(N) -> a__sqr#(mark(N))
    mark#(s(X)) -> mark#(X) -> mark#(terms(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(terms(X)) -> a__terms#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(sqr(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(s(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2)
    mark#(s(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    mark#(s(X)) -> mark#(X) -> mark#(half(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(half(X)) -> a__half#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(recip(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(recip(X)) -> mark#(X) -> mark#(terms(X)) -> mark#(X)
    mark#(recip(X)) -> mark#(X) -> mark#(terms(X)) -> a__terms#(mark(X))
    mark#(recip(X)) -> mark#(X) -> mark#(sqr(X)) -> mark#(X)
    mark#(recip(X)) -> mark#(X) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    mark#(recip(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(recip(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(recip(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(recip(X)) -> mark#(X) -> mark#(dbl(X)) -> mark#(X)
    mark#(recip(X)) -> mark#(X) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    mark#(recip(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X2)
    mark#(recip(X)) -> mark#(X) -> mark#(first(X1,X2)) -> mark#(X1)
    mark#(recip(X)) -> mark#(X) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    mark#(recip(X)) -> mark#(X) -> mark#(half(X)) -> mark#(X)
    mark#(recip(X)) -> mark#(X) -> mark#(half(X)) -> a__half#(mark(X))
    mark#(recip(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(recip(X)) -> mark#(X) -> mark#(recip(X)) -> mark#(X)
    mark#(recip(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__terms#(N) -> a__sqr#(mark(N)) ->
    a__sqr#(s(X)) -> a__dbl#(mark(X))
    a__terms#(N) -> a__sqr#(mark(N)) -> a__sqr#(s(X)) -> mark#(X)
    a__terms#(N) -> a__sqr#(mark(N)) ->
    a__sqr#(s(X)) -> a__sqr#(mark(X))
    a__terms#(N) -> a__sqr#(mark(N)) ->
    a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)),a__dbl(mark(X)))
    a__terms#(N) -> mark#(N) -> mark#(terms(X)) -> mark#(X)
    a__terms#(N) -> mark#(N) -> mark#(terms(X)) -> a__terms#(mark(X))
    a__terms#(N) -> mark#(N) -> mark#(sqr(X)) -> mark#(X)
    a__terms#(N) -> mark#(N) -> mark#(sqr(X)) -> a__sqr#(mark(X))
    a__terms#(N) -> mark#(N) -> mark#(add(X1,X2)) -> mark#(X2)
    a__terms#(N) -> mark#(N) -> mark#(add(X1,X2)) -> mark#(X1)
    a__terms#(N) -> mark#(N) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    a__terms#(N) -> mark#(N) -> mark#(dbl(X)) -> mark#(X)
    a__terms#(N) -> mark#(N) -> mark#(dbl(X)) -> a__dbl#(mark(X))
    a__terms#(N) -> mark#(N) -> mark#(first(X1,X2)) -> mark#(X2)
    a__terms#(N) -> mark#(N) -> mark#(first(X1,X2)) -> mark#(X1)
    a__terms#(N) -> mark#(N) ->
    mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
    a__terms#(N) -> mark#(N) -> mark#(half(X)) -> mark#(X)
    a__terms#(N) -> mark#(N) -> mark#(half(X)) -> a__half#(mark(X))
    a__terms#(N) -> mark#(N) -> mark#(cons(X1,X2)) -> mark#(X1)
    a__terms#(N) -> mark#(N) -> mark#(recip(X)) -> mark#(X)
    a__terms#(N) -> mark#(N) -> mark#(s(X)) -> mark#(X)
   Restore Modifier:
    DPs:
     a__terms#(N) -> mark#(N)
     a__terms#(N) -> a__sqr#(mark(N))
     a__sqr#(s(X)) -> a__dbl#(mark(X))
     a__sqr#(s(X)) -> mark#(X)
     a__sqr#(s(X)) -> a__sqr#(mark(X))
     a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)),a__dbl(mark(X)))
     a__dbl#(s(X)) -> mark#(X)
     a__dbl#(s(X)) -> a__dbl#(mark(X))
     a__add#(0(),X) -> mark#(X)
     a__add#(s(X),Y) -> mark#(Y)
     a__add#(s(X),Y) -> mark#(X)
     a__add#(s(X),Y) -> a__add#(mark(X),mark(Y))
     a__first#(s(X),cons(Y,Z)) -> mark#(Y)
     a__half#(s(s(X))) -> mark#(X)
     a__half#(s(s(X))) -> a__half#(mark(X))
     a__half#(dbl(X)) -> mark#(X)
     mark#(terms(X)) -> mark#(X)
     mark#(terms(X)) -> a__terms#(mark(X))
     mark#(sqr(X)) -> mark#(X)
     mark#(sqr(X)) -> a__sqr#(mark(X))
     mark#(add(X1,X2)) -> mark#(X2)
     mark#(add(X1,X2)) -> mark#(X1)
     mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
     mark#(dbl(X)) -> mark#(X)
     mark#(dbl(X)) -> a__dbl#(mark(X))
     mark#(first(X1,X2)) -> mark#(X2)
     mark#(first(X1,X2)) -> mark#(X1)
     mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
     mark#(half(X)) -> mark#(X)
     mark#(half(X)) -> a__half#(mark(X))
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(recip(X)) -> mark#(X)
     mark#(s(X)) -> mark#(X)
    TRS:
     a__terms(N) -> cons(recip(a__sqr(mark(N))),terms(s(N)))
     a__sqr(0()) -> 0()
     a__sqr(s(X)) -> s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))
     a__dbl(0()) -> 0()
     a__dbl(s(X)) -> s(s(a__dbl(mark(X))))
     a__add(0(),X) -> mark(X)
     a__add(s(X),Y) -> s(a__add(mark(X),mark(Y)))
     a__first(0(),X) -> nil()
     a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z))
     a__half(0()) -> 0()
     a__half(s(0())) -> 0()
     a__half(s(s(X))) -> s(a__half(mark(X)))
     a__half(dbl(X)) -> mark(X)
     mark(terms(X)) -> a__terms(mark(X))
     mark(sqr(X)) -> a__sqr(mark(X))
     mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
     mark(dbl(X)) -> a__dbl(mark(X))
     mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
     mark(half(X)) -> a__half(mark(X))
     mark(cons(X1,X2)) -> cons(mark(X1),X2)
     mark(recip(X)) -> recip(mark(X))
     mark(s(X)) -> s(mark(X))
     mark(0()) -> 0()
     mark(nil()) -> nil()
     a__terms(X) -> terms(X)
     a__sqr(X) -> sqr(X)
     a__add(X1,X2) -> add(X1,X2)
     a__dbl(X) -> dbl(X)
     a__first(X1,X2) -> first(X1,X2)
     a__half(X) -> half(X)
    SCC Processor:
     #sccs: 1
     #rules: 33
     #arcs: 379/1089
     DPs:
      a__half#(dbl(X)) -> mark#(X)
      mark#(s(X)) -> mark#(X)
      mark#(recip(X)) -> mark#(X)
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(half(X)) -> a__half#(mark(X))
      a__half#(s(s(X))) -> a__half#(mark(X))
      a__half#(s(s(X))) -> mark#(X)
      mark#(half(X)) -> mark#(X)
      mark#(first(X1,X2)) -> a__first#(mark(X1),mark(X2))
      a__first#(s(X),cons(Y,Z)) -> mark#(Y)
      mark#(first(X1,X2)) -> mark#(X1)
      mark#(first(X1,X2)) -> mark#(X2)
      mark#(dbl(X)) -> a__dbl#(mark(X))
      a__dbl#(s(X)) -> a__dbl#(mark(X))
      a__dbl#(s(X)) -> mark#(X)
      mark#(dbl(X)) -> mark#(X)
      mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
      a__add#(s(X),Y) -> a__add#(mark(X),mark(Y))
      a__add#(s(X),Y) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(sqr(X)) -> a__sqr#(mark(X))
      a__sqr#(s(X)) -> a__add#(a__sqr(mark(X)),a__dbl(mark(X)))
      a__add#(s(X),Y) -> mark#(Y)
      mark#(sqr(X)) -> mark#(X)
      mark#(terms(X)) -> a__terms#(mark(X))
      a__terms#(N) -> a__sqr#(mark(N))
      a__sqr#(s(X)) -> a__sqr#(mark(X))
      a__sqr#(s(X)) -> mark#(X)
      mark#(terms(X)) -> mark#(X)
      a__sqr#(s(X)) -> a__dbl#(mark(X))
      a__terms#(N) -> mark#(N)
      a__add#(0(),X) -> mark#(X)
     TRS:
      a__terms(N) -> cons(recip(a__sqr(mark(N))),terms(s(N)))
      a__sqr(0()) -> 0()
      a__sqr(s(X)) -> s(a__add(a__sqr(mark(X)),a__dbl(mark(X))))
      a__dbl(0()) -> 0()
      a__dbl(s(X)) -> s(s(a__dbl(mark(X))))
      a__add(0(),X) -> mark(X)
      a__add(s(X),Y) -> s(a__add(mark(X),mark(Y)))
      a__first(0(),X) -> nil()
      a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z))
      a__half(0()) -> 0()
      a__half(s(0())) -> 0()
      a__half(s(s(X))) -> s(a__half(mark(X)))
      a__half(dbl(X)) -> mark(X)
      mark(terms(X)) -> a__terms(mark(X))
      mark(sqr(X)) -> a__sqr(mark(X))
      mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
      mark(dbl(X)) -> a__dbl(mark(X))
      mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
      mark(half(X)) -> a__half(mark(X))
      mark(cons(X1,X2)) -> cons(mark(X1),X2)
      mark(recip(X)) -> recip(mark(X))
      mark(s(X)) -> s(mark(X))
      mark(0()) -> 0()
      mark(nil()) -> nil()
      a__terms(X) -> terms(X)
      a__sqr(X) -> sqr(X)
      a__add(X1,X2) -> add(X1,X2)
      a__dbl(X) -> dbl(X)
      a__first(X1,X2) -> first(X1,X2)
      a__half(X) -> half(X)
     Open