YES

We show the termination of the TRS R:

  active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
  active(sqr(|0|())) -> mark(|0|())
  active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
  active(dbl(|0|())) -> mark(|0|())
  active(dbl(s(X))) -> mark(s(s(dbl(X))))
  active(add(|0|(),X)) -> mark(X)
  active(add(s(X),Y)) -> mark(s(add(X,Y)))
  active(first(|0|(),X)) -> mark(nil())
  active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
  mark(terms(X)) -> active(terms(mark(X)))
  mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
  mark(recip(X)) -> active(recip(mark(X)))
  mark(sqr(X)) -> active(sqr(mark(X)))
  mark(s(X)) -> active(s(X))
  mark(|0|()) -> active(|0|())
  mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
  mark(dbl(X)) -> active(dbl(mark(X)))
  mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
  mark(nil()) -> active(nil())
  terms(mark(X)) -> terms(X)
  terms(active(X)) -> terms(X)
  cons(mark(X1),X2) -> cons(X1,X2)
  cons(X1,mark(X2)) -> cons(X1,X2)
  cons(active(X1),X2) -> cons(X1,X2)
  cons(X1,active(X2)) -> cons(X1,X2)
  recip(mark(X)) -> recip(X)
  recip(active(X)) -> recip(X)
  sqr(mark(X)) -> sqr(X)
  sqr(active(X)) -> sqr(X)
  s(mark(X)) -> s(X)
  s(active(X)) -> s(X)
  add(mark(X1),X2) -> add(X1,X2)
  add(X1,mark(X2)) -> add(X1,X2)
  add(active(X1),X2) -> add(X1,X2)
  add(X1,active(X2)) -> add(X1,X2)
  dbl(mark(X)) -> dbl(X)
  dbl(active(X)) -> dbl(X)
  first(mark(X1),X2) -> first(X1,X2)
  first(X1,mark(X2)) -> first(X1,X2)
  first(active(X1),X2) -> first(X1,X2)
  first(X1,active(X2)) -> first(X1,X2)

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N))))
p2: active#(terms(N)) -> cons#(recip(sqr(N)),terms(s(N)))
p3: active#(terms(N)) -> recip#(sqr(N))
p4: active#(terms(N)) -> sqr#(N)
p5: active#(terms(N)) -> terms#(s(N))
p6: active#(terms(N)) -> s#(N)
p7: active#(sqr(|0|())) -> mark#(|0|())
p8: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X))))
p9: active#(sqr(s(X))) -> s#(add(sqr(X),dbl(X)))
p10: active#(sqr(s(X))) -> add#(sqr(X),dbl(X))
p11: active#(sqr(s(X))) -> sqr#(X)
p12: active#(sqr(s(X))) -> dbl#(X)
p13: active#(dbl(|0|())) -> mark#(|0|())
p14: active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
p15: active#(dbl(s(X))) -> s#(s(dbl(X)))
p16: active#(dbl(s(X))) -> s#(dbl(X))
p17: active#(dbl(s(X))) -> dbl#(X)
p18: active#(add(|0|(),X)) -> mark#(X)
p19: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p20: active#(add(s(X),Y)) -> s#(add(X,Y))
p21: active#(add(s(X),Y)) -> add#(X,Y)
p22: active#(first(|0|(),X)) -> mark#(nil())
p23: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p24: active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
p25: active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
p26: mark#(terms(X)) -> active#(terms(mark(X)))
p27: mark#(terms(X)) -> terms#(mark(X))
p28: mark#(terms(X)) -> mark#(X)
p29: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p30: mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
p31: mark#(cons(X1,X2)) -> mark#(X1)
p32: mark#(recip(X)) -> active#(recip(mark(X)))
p33: mark#(recip(X)) -> recip#(mark(X))
p34: mark#(recip(X)) -> mark#(X)
p35: mark#(sqr(X)) -> active#(sqr(mark(X)))
p36: mark#(sqr(X)) -> sqr#(mark(X))
p37: mark#(sqr(X)) -> mark#(X)
p38: mark#(s(X)) -> active#(s(X))
p39: mark#(|0|()) -> active#(|0|())
p40: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p41: mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
p42: mark#(add(X1,X2)) -> mark#(X1)
p43: mark#(add(X1,X2)) -> mark#(X2)
p44: mark#(dbl(X)) -> active#(dbl(mark(X)))
p45: mark#(dbl(X)) -> dbl#(mark(X))
p46: mark#(dbl(X)) -> mark#(X)
p47: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p48: mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
p49: mark#(first(X1,X2)) -> mark#(X1)
p50: mark#(first(X1,X2)) -> mark#(X2)
p51: mark#(nil()) -> active#(nil())
p52: terms#(mark(X)) -> terms#(X)
p53: terms#(active(X)) -> terms#(X)
p54: cons#(mark(X1),X2) -> cons#(X1,X2)
p55: cons#(X1,mark(X2)) -> cons#(X1,X2)
p56: cons#(active(X1),X2) -> cons#(X1,X2)
p57: cons#(X1,active(X2)) -> cons#(X1,X2)
p58: recip#(mark(X)) -> recip#(X)
p59: recip#(active(X)) -> recip#(X)
p60: sqr#(mark(X)) -> sqr#(X)
p61: sqr#(active(X)) -> sqr#(X)
p62: s#(mark(X)) -> s#(X)
p63: s#(active(X)) -> s#(X)
p64: add#(mark(X1),X2) -> add#(X1,X2)
p65: add#(X1,mark(X2)) -> add#(X1,X2)
p66: add#(active(X1),X2) -> add#(X1,X2)
p67: add#(X1,active(X2)) -> add#(X1,X2)
p68: dbl#(mark(X)) -> dbl#(X)
p69: dbl#(active(X)) -> dbl#(X)
p70: first#(mark(X1),X2) -> first#(X1,X2)
p71: first#(X1,mark(X2)) -> first#(X1,X2)
p72: first#(active(X1),X2) -> first#(X1,X2)
p73: first#(X1,active(X2)) -> first#(X1,X2)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p8, p14, p18, p19, p23, p26, p28, p29, p31, p32, p34, p35, p37, p38, p40, p42, p43, p44, p46, p47, p49, p50}
  {p54, p55, p56, p57}
  {p58, p59}
  {p60, p61}
  {p52, p53}
  {p62, p63}
  {p64, p65, p66, p67}
  {p68, p69}
  {p70, p71, p72, p73}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N))))
p2: mark#(first(X1,X2)) -> mark#(X2)
p3: mark#(first(X1,X2)) -> mark#(X1)
p4: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p5: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p6: mark#(dbl(X)) -> mark#(X)
p7: mark#(dbl(X)) -> active#(dbl(mark(X)))
p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p9: mark#(add(X1,X2)) -> mark#(X2)
p10: mark#(add(X1,X2)) -> mark#(X1)
p11: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p12: active#(add(|0|(),X)) -> mark#(X)
p13: mark#(s(X)) -> active#(s(X))
p14: active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
p15: mark#(sqr(X)) -> mark#(X)
p16: mark#(sqr(X)) -> active#(sqr(mark(X)))
p17: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X))))
p18: mark#(recip(X)) -> mark#(X)
p19: mark#(recip(X)) -> active#(recip(mark(X)))
p20: mark#(cons(X1,X2)) -> mark#(X1)
p21: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p22: mark#(terms(X)) -> mark#(X)
p23: mark#(terms(X)) -> active#(terms(mark(X)))

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      mark > |0| > active > dbl > first > nil > cons > s > sqr > add > recip > active# > mark# > terms
    
    argument filter:
  
      pi(active#) = 1
      pi(terms) = 1
      pi(mark#) = 1
      pi(cons) = 1
      pi(recip) = 1
      pi(sqr) = 1
      pi(s) = []
      pi(first) = [1, 2]
      pi(mark) = 1
      pi(dbl) = 1
      pi(add) = [1, 2]
      pi(|0|) = []
      pi(active) = 1
      pi(nil) = []

The next rules are strictly ordered:

  p2, p3, p5, p8, p9, p10, p12

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N))))
p2: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p3: mark#(dbl(X)) -> mark#(X)
p4: mark#(dbl(X)) -> active#(dbl(mark(X)))
p5: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p6: mark#(s(X)) -> active#(s(X))
p7: active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
p8: mark#(sqr(X)) -> mark#(X)
p9: mark#(sqr(X)) -> active#(sqr(mark(X)))
p10: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X))))
p11: mark#(recip(X)) -> mark#(X)
p12: mark#(recip(X)) -> active#(recip(mark(X)))
p13: mark#(cons(X1,X2)) -> mark#(X1)
p14: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p15: mark#(terms(X)) -> mark#(X)
p16: mark#(terms(X)) -> active#(terms(mark(X)))

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: active#(terms(N)) -> mark#(cons(recip(sqr(N)),terms(s(N))))
p2: mark#(terms(X)) -> active#(terms(mark(X)))
p3: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X))))
p4: mark#(terms(X)) -> mark#(X)
p5: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p6: active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
p7: mark#(cons(X1,X2)) -> mark#(X1)
p8: mark#(recip(X)) -> active#(recip(mark(X)))
p9: mark#(recip(X)) -> mark#(X)
p10: mark#(sqr(X)) -> active#(sqr(mark(X)))
p11: mark#(sqr(X)) -> mark#(X)
p12: mark#(s(X)) -> active#(s(X))
p13: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p14: mark#(dbl(X)) -> active#(dbl(mark(X)))
p15: mark#(dbl(X)) -> mark#(X)
p16: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      |0| > first > active# > mark# > add > s > nil > terms > mark > sqr > recip > active > dbl > cons
    
    argument filter:
  
      pi(active#) = 1
      pi(terms) = [1]
      pi(mark#) = 1
      pi(cons) = 1
      pi(recip) = 1
      pi(sqr) = 1
      pi(s) = []
      pi(mark) = 1
      pi(add) = [2]
      pi(dbl) = [1]
      pi(first) = [1, 2]
      pi(active) = 1
      pi(|0|) = []
      pi(nil) = []

The next rules are strictly ordered:

  p1, p4, p6, p15

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(terms(X)) -> active#(terms(mark(X)))
p2: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X))))
p3: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p4: mark#(cons(X1,X2)) -> mark#(X1)
p5: mark#(recip(X)) -> active#(recip(mark(X)))
p6: mark#(recip(X)) -> mark#(X)
p7: mark#(sqr(X)) -> active#(sqr(mark(X)))
p8: mark#(sqr(X)) -> mark#(X)
p9: mark#(s(X)) -> active#(s(X))
p10: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p11: mark#(dbl(X)) -> active#(dbl(mark(X)))
p12: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(terms(X)) -> active#(terms(mark(X)))
p2: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X))))
p3: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p4: mark#(dbl(X)) -> active#(dbl(mark(X)))
p5: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p6: mark#(s(X)) -> active#(s(X))
p7: mark#(sqr(X)) -> mark#(X)
p8: mark#(sqr(X)) -> active#(sqr(mark(X)))
p9: mark#(recip(X)) -> mark#(X)
p10: mark#(recip(X)) -> active#(recip(mark(X)))
p11: mark#(cons(X1,X2)) -> mark#(X1)
p12: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      terms > sqr > dbl > add > |0| > mark > s > mark# > active# > cons > first > nil > recip > active
    
    argument filter:
  
      pi(mark#) = 1
      pi(terms) = [1]
      pi(active#) = 1
      pi(mark) = 1
      pi(sqr) = 1
      pi(s) = 1
      pi(add) = 2
      pi(dbl) = 1
      pi(first) = [2]
      pi(recip) = [1]
      pi(cons) = 1
      pi(active) = 1
      pi(|0|) = []
      pi(nil) = []

The next rules are strictly ordered:

  p9

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(terms(X)) -> active#(terms(mark(X)))
p2: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X))))
p3: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p4: mark#(dbl(X)) -> active#(dbl(mark(X)))
p5: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p6: mark#(s(X)) -> active#(s(X))
p7: mark#(sqr(X)) -> mark#(X)
p8: mark#(sqr(X)) -> active#(sqr(mark(X)))
p9: mark#(recip(X)) -> active#(recip(mark(X)))
p10: mark#(cons(X1,X2)) -> mark#(X1)
p11: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(terms(X)) -> active#(terms(mark(X)))
p2: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X))))
p3: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p4: mark#(cons(X1,X2)) -> mark#(X1)
p5: mark#(recip(X)) -> active#(recip(mark(X)))
p6: mark#(sqr(X)) -> active#(sqr(mark(X)))
p7: mark#(sqr(X)) -> mark#(X)
p8: mark#(s(X)) -> active#(s(X))
p9: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p10: mark#(dbl(X)) -> active#(dbl(mark(X)))
p11: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      terms > sqr > add > active > active# > mark# > dbl > s > mark > first > nil > |0| > recip > cons
    
    argument filter:
  
      pi(mark#) = [1]
      pi(terms) = [1]
      pi(active#) = 1
      pi(mark) = 1
      pi(sqr) = [1]
      pi(s) = []
      pi(add) = [2]
      pi(dbl) = []
      pi(cons) = 1
      pi(recip) = 1
      pi(first) = [2]
      pi(active) = 1
      pi(|0|) = []
      pi(nil) = []

The next rules are strictly ordered:

  p1, p2, p3, p5, p6, p7, p8, p9, p10, p11

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(cons(X1,X2)) -> mark#(X1)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(cons(X1,X2)) -> mark#(X1)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      cons > mark#
    
    argument filter:
  
      pi(mark#) = [1]
      pi(cons) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(X1,active(X2)) -> cons#(X1,X2)
p3: cons#(active(X1),X2) -> cons#(X1,X2)
p4: cons#(X1,mark(X2)) -> cons#(X1,X2)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      cons# > active > mark
    
    argument filter:
  
      pi(cons#) = 2
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p2, p4

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(active(X1),X2) -> cons#(X1,X2)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(active(X1),X2) -> cons#(X1,X2)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      cons# > active > mark
    
    argument filter:
  
      pi(cons#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: recip#(mark(X)) -> recip#(X)
p2: recip#(active(X)) -> recip#(X)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      recip# > active > mark
    
    argument filter:
  
      pi(recip#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: sqr#(mark(X)) -> sqr#(X)
p2: sqr#(active(X)) -> sqr#(X)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      sqr# > active > mark
    
    argument filter:
  
      pi(sqr#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: terms#(mark(X)) -> terms#(X)
p2: terms#(active(X)) -> terms#(X)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      terms# > active > mark
    
    argument filter:
  
      pi(terms#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: s#(mark(X)) -> s#(X)
p2: s#(active(X)) -> s#(X)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      s# > active > mark
    
    argument filter:
  
      pi(s#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: add#(mark(X1),X2) -> add#(X1,X2)
p2: add#(X1,active(X2)) -> add#(X1,X2)
p3: add#(active(X1),X2) -> add#(X1,X2)
p4: add#(X1,mark(X2)) -> add#(X1,X2)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      add# > active > mark
    
    argument filter:
  
      pi(add#) = 2
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p2, p4

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: add#(mark(X1),X2) -> add#(X1,X2)
p2: add#(active(X1),X2) -> add#(X1,X2)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: add#(mark(X1),X2) -> add#(X1,X2)
p2: add#(active(X1),X2) -> add#(X1,X2)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      add# > active > mark
    
    argument filter:
  
      pi(add#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: dbl#(mark(X)) -> dbl#(X)
p2: dbl#(active(X)) -> dbl#(X)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      dbl# > active > mark
    
    argument filter:
  
      pi(dbl#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: first#(mark(X1),X2) -> first#(X1,X2)
p2: first#(X1,active(X2)) -> first#(X1,X2)
p3: first#(active(X1),X2) -> first#(X1,X2)
p4: first#(X1,mark(X2)) -> first#(X1,X2)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      first# > active > mark
    
    argument filter:
  
      pi(first#) = 2
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p2, p4

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: first#(mark(X1),X2) -> first#(X1,X2)
p2: first#(active(X1),X2) -> first#(X1,X2)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: first#(mark(X1),X2) -> first#(X1,X2)
p2: first#(active(X1),X2) -> first#(X1,X2)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: mark(terms(X)) -> active(terms(mark(X)))
r11: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r12: mark(recip(X)) -> active(recip(mark(X)))
r13: mark(sqr(X)) -> active(sqr(mark(X)))
r14: mark(s(X)) -> active(s(X))
r15: mark(|0|()) -> active(|0|())
r16: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r17: mark(dbl(X)) -> active(dbl(mark(X)))
r18: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r19: mark(nil()) -> active(nil())
r20: terms(mark(X)) -> terms(X)
r21: terms(active(X)) -> terms(X)
r22: cons(mark(X1),X2) -> cons(X1,X2)
r23: cons(X1,mark(X2)) -> cons(X1,X2)
r24: cons(active(X1),X2) -> cons(X1,X2)
r25: cons(X1,active(X2)) -> cons(X1,X2)
r26: recip(mark(X)) -> recip(X)
r27: recip(active(X)) -> recip(X)
r28: sqr(mark(X)) -> sqr(X)
r29: sqr(active(X)) -> sqr(X)
r30: s(mark(X)) -> s(X)
r31: s(active(X)) -> s(X)
r32: add(mark(X1),X2) -> add(X1,X2)
r33: add(X1,mark(X2)) -> add(X1,X2)
r34: add(active(X1),X2) -> add(X1,X2)
r35: add(X1,active(X2)) -> add(X1,X2)
r36: dbl(mark(X)) -> dbl(X)
r37: dbl(active(X)) -> dbl(X)
r38: first(mark(X1),X2) -> first(X1,X2)
r39: first(X1,mark(X2)) -> first(X1,X2)
r40: first(active(X1),X2) -> first(X1,X2)
r41: first(X1,active(X2)) -> first(X1,X2)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      first# > active > mark
    
    argument filter:
  
      pi(first#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.  Then no dependency pair remains.