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)))
  active(half(|0|())) -> mark(|0|())
  active(half(s(|0|()))) -> mark(|0|())
  active(half(s(s(X)))) -> mark(s(half(X)))
  active(half(dbl(X))) -> mark(X)
  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(mark(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())
  mark(half(X)) -> active(half(mark(X)))
  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)
  half(mark(X)) -> half(X)
  half(active(X)) -> half(X)

-- 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: active#(half(|0|())) -> mark#(|0|())
p27: active#(half(s(|0|()))) -> mark#(|0|())
p28: active#(half(s(s(X)))) -> mark#(s(half(X)))
p29: active#(half(s(s(X)))) -> s#(half(X))
p30: active#(half(s(s(X)))) -> half#(X)
p31: active#(half(dbl(X))) -> mark#(X)
p32: mark#(terms(X)) -> active#(terms(mark(X)))
p33: mark#(terms(X)) -> terms#(mark(X))
p34: mark#(terms(X)) -> mark#(X)
p35: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p36: mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
p37: mark#(cons(X1,X2)) -> mark#(X1)
p38: mark#(recip(X)) -> active#(recip(mark(X)))
p39: mark#(recip(X)) -> recip#(mark(X))
p40: mark#(recip(X)) -> mark#(X)
p41: mark#(sqr(X)) -> active#(sqr(mark(X)))
p42: mark#(sqr(X)) -> sqr#(mark(X))
p43: mark#(sqr(X)) -> mark#(X)
p44: mark#(s(X)) -> active#(s(mark(X)))
p45: mark#(s(X)) -> s#(mark(X))
p46: mark#(s(X)) -> mark#(X)
p47: mark#(|0|()) -> active#(|0|())
p48: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p49: mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
p50: mark#(add(X1,X2)) -> mark#(X1)
p51: mark#(add(X1,X2)) -> mark#(X2)
p52: mark#(dbl(X)) -> active#(dbl(mark(X)))
p53: mark#(dbl(X)) -> dbl#(mark(X))
p54: mark#(dbl(X)) -> mark#(X)
p55: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p56: mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
p57: mark#(first(X1,X2)) -> mark#(X1)
p58: mark#(first(X1,X2)) -> mark#(X2)
p59: mark#(nil()) -> active#(nil())
p60: mark#(half(X)) -> active#(half(mark(X)))
p61: mark#(half(X)) -> half#(mark(X))
p62: mark#(half(X)) -> mark#(X)
p63: terms#(mark(X)) -> terms#(X)
p64: terms#(active(X)) -> terms#(X)
p65: cons#(mark(X1),X2) -> cons#(X1,X2)
p66: cons#(X1,mark(X2)) -> cons#(X1,X2)
p67: cons#(active(X1),X2) -> cons#(X1,X2)
p68: cons#(X1,active(X2)) -> cons#(X1,X2)
p69: recip#(mark(X)) -> recip#(X)
p70: recip#(active(X)) -> recip#(X)
p71: sqr#(mark(X)) -> sqr#(X)
p72: sqr#(active(X)) -> sqr#(X)
p73: s#(mark(X)) -> s#(X)
p74: s#(active(X)) -> s#(X)
p75: add#(mark(X1),X2) -> add#(X1,X2)
p76: add#(X1,mark(X2)) -> add#(X1,X2)
p77: add#(active(X1),X2) -> add#(X1,X2)
p78: add#(X1,active(X2)) -> add#(X1,X2)
p79: dbl#(mark(X)) -> dbl#(X)
p80: dbl#(active(X)) -> dbl#(X)
p81: first#(mark(X1),X2) -> first#(X1,X2)
p82: first#(X1,mark(X2)) -> first#(X1,X2)
p83: first#(active(X1),X2) -> first#(X1,X2)
p84: first#(X1,active(X2)) -> first#(X1,X2)
p85: half#(mark(X)) -> half#(X)
p86: half#(active(X)) -> half#(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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

The estimated dependency graph contains the following SCCs:

  {p1, p8, p14, p18, p19, p23, p28, p31, p32, p34, p35, p37, p38, p40, p41, p43, p44, p46, p48, p50, p51, p52, p54, p55, p57, p58, p60, p62}
  {p65, p66, p67, p68}
  {p69, p70}
  {p71, p72}
  {p63, p64}
  {p73, p74}
  {p75, p76, p77, p78}
  {p79, p80}
  {p81, p82, p83, p84}
  {p85, p86}


-- 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#(half(X)) -> mark#(X)
p3: mark#(half(X)) -> active#(half(mark(X)))
p4: active#(half(dbl(X))) -> mark#(X)
p5: mark#(first(X1,X2)) -> mark#(X2)
p6: mark#(first(X1,X2)) -> mark#(X1)
p7: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p8: active#(half(s(s(X)))) -> mark#(s(half(X)))
p9: mark#(dbl(X)) -> mark#(X)
p10: mark#(dbl(X)) -> active#(dbl(mark(X)))
p11: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p12: mark#(add(X1,X2)) -> mark#(X2)
p13: mark#(add(X1,X2)) -> mark#(X1)
p14: mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
p15: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p16: mark#(s(X)) -> mark#(X)
p17: mark#(s(X)) -> active#(s(mark(X)))
p18: active#(add(|0|(),X)) -> mark#(X)
p19: mark#(sqr(X)) -> mark#(X)
p20: mark#(sqr(X)) -> active#(sqr(mark(X)))
p21: active#(dbl(s(X))) -> mark#(s(s(dbl(X))))
p22: mark#(recip(X)) -> mark#(X)
p23: mark#(recip(X)) -> active#(recip(mark(X)))
p24: active#(sqr(s(X))) -> mark#(s(add(sqr(X),dbl(X))))
p25: mark#(cons(X1,X2)) -> mark#(X1)
p26: mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
p27: mark#(terms(X)) -> mark#(X)
p28: 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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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, r42, r43, r44, r45, r46, r47, r48

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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, r42, r43, r44, r45, r46, r47, r48

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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, r42, r43, r44, r45, r46, r47, r48

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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, r42, r43, r44, r45, r46, r47, r48

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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, r42, r43, r44, r45, r46, r47, r48

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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, r42, r43, r44, r45, r46, r47, r48

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

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.

-- Reduction pair.

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

p1: half#(mark(X)) -> half#(X)
p2: half#(active(X)) -> half#(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: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: mark(terms(X)) -> active(terms(mark(X)))
r15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
r16: mark(recip(X)) -> active(recip(mark(X)))
r17: mark(sqr(X)) -> active(sqr(mark(X)))
r18: mark(s(X)) -> active(s(mark(X)))
r19: mark(|0|()) -> active(|0|())
r20: mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
r21: mark(dbl(X)) -> active(dbl(mark(X)))
r22: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r23: mark(nil()) -> active(nil())
r24: mark(half(X)) -> active(half(mark(X)))
r25: terms(mark(X)) -> terms(X)
r26: terms(active(X)) -> terms(X)
r27: cons(mark(X1),X2) -> cons(X1,X2)
r28: cons(X1,mark(X2)) -> cons(X1,X2)
r29: cons(active(X1),X2) -> cons(X1,X2)
r30: cons(X1,active(X2)) -> cons(X1,X2)
r31: recip(mark(X)) -> recip(X)
r32: recip(active(X)) -> recip(X)
r33: sqr(mark(X)) -> sqr(X)
r34: sqr(active(X)) -> sqr(X)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: add(mark(X1),X2) -> add(X1,X2)
r38: add(X1,mark(X2)) -> add(X1,X2)
r39: add(active(X1),X2) -> add(X1,X2)
r40: add(X1,active(X2)) -> add(X1,X2)
r41: dbl(mark(X)) -> dbl(X)
r42: dbl(active(X)) -> dbl(X)
r43: first(mark(X1),X2) -> first(X1,X2)
r44: first(X1,mark(X2)) -> first(X1,X2)
r45: first(active(X1),X2) -> first(X1,X2)
r46: first(X1,active(X2)) -> first(X1,X2)
r47: half(mark(X)) -> half(X)
r48: half(active(X)) -> half(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      half# > active > mark
    
    argument filter:
  
      pi(half#) = 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, r42, r43, r44, r45, r46, r47, r48

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