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(terms(X)) -> terms(active(X))
  active(cons(X1,X2)) -> cons(active(X1),X2)
  active(recip(X)) -> recip(active(X))
  active(sqr(X)) -> sqr(active(X))
  active(add(X1,X2)) -> add(active(X1),X2)
  active(add(X1,X2)) -> add(X1,active(X2))
  active(dbl(X)) -> dbl(active(X))
  active(first(X1,X2)) -> first(active(X1),X2)
  active(first(X1,X2)) -> first(X1,active(X2))
  terms(mark(X)) -> mark(terms(X))
  cons(mark(X1),X2) -> mark(cons(X1,X2))
  recip(mark(X)) -> mark(recip(X))
  sqr(mark(X)) -> mark(sqr(X))
  add(mark(X1),X2) -> mark(add(X1,X2))
  add(X1,mark(X2)) -> mark(add(X1,X2))
  dbl(mark(X)) -> mark(dbl(X))
  first(mark(X1),X2) -> mark(first(X1,X2))
  first(X1,mark(X2)) -> mark(first(X1,X2))
  proper(terms(X)) -> terms(proper(X))
  proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
  proper(recip(X)) -> recip(proper(X))
  proper(sqr(X)) -> sqr(proper(X))
  proper(s(X)) -> s(proper(X))
  proper(|0|()) -> ok(|0|())
  proper(add(X1,X2)) -> add(proper(X1),proper(X2))
  proper(dbl(X)) -> dbl(proper(X))
  proper(first(X1,X2)) -> first(proper(X1),proper(X2))
  proper(nil()) -> ok(nil())
  terms(ok(X)) -> ok(terms(X))
  cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
  recip(ok(X)) -> ok(recip(X))
  sqr(ok(X)) -> ok(sqr(X))
  s(ok(X)) -> ok(s(X))
  add(ok(X1),ok(X2)) -> ok(add(X1,X2))
  dbl(ok(X)) -> ok(dbl(X))
  first(ok(X1),ok(X2)) -> ok(first(X1,X2))
  top(mark(X)) -> top(proper(X))
  top(ok(X)) -> top(active(X))

-- SCC decomposition.

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

p1: active#(terms(N)) -> cons#(recip(sqr(N)),terms(s(N)))
p2: active#(terms(N)) -> recip#(sqr(N))
p3: active#(terms(N)) -> sqr#(N)
p4: active#(terms(N)) -> terms#(s(N))
p5: active#(terms(N)) -> s#(N)
p6: active#(sqr(s(X))) -> s#(add(sqr(X),dbl(X)))
p7: active#(sqr(s(X))) -> add#(sqr(X),dbl(X))
p8: active#(sqr(s(X))) -> sqr#(X)
p9: active#(sqr(s(X))) -> dbl#(X)
p10: active#(dbl(s(X))) -> s#(s(dbl(X)))
p11: active#(dbl(s(X))) -> s#(dbl(X))
p12: active#(dbl(s(X))) -> dbl#(X)
p13: active#(add(s(X),Y)) -> s#(add(X,Y))
p14: active#(add(s(X),Y)) -> add#(X,Y)
p15: active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
p16: active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
p17: active#(terms(X)) -> terms#(active(X))
p18: active#(terms(X)) -> active#(X)
p19: active#(cons(X1,X2)) -> cons#(active(X1),X2)
p20: active#(cons(X1,X2)) -> active#(X1)
p21: active#(recip(X)) -> recip#(active(X))
p22: active#(recip(X)) -> active#(X)
p23: active#(sqr(X)) -> sqr#(active(X))
p24: active#(sqr(X)) -> active#(X)
p25: active#(add(X1,X2)) -> add#(active(X1),X2)
p26: active#(add(X1,X2)) -> active#(X1)
p27: active#(add(X1,X2)) -> add#(X1,active(X2))
p28: active#(add(X1,X2)) -> active#(X2)
p29: active#(dbl(X)) -> dbl#(active(X))
p30: active#(dbl(X)) -> active#(X)
p31: active#(first(X1,X2)) -> first#(active(X1),X2)
p32: active#(first(X1,X2)) -> active#(X1)
p33: active#(first(X1,X2)) -> first#(X1,active(X2))
p34: active#(first(X1,X2)) -> active#(X2)
p35: terms#(mark(X)) -> terms#(X)
p36: cons#(mark(X1),X2) -> cons#(X1,X2)
p37: recip#(mark(X)) -> recip#(X)
p38: sqr#(mark(X)) -> sqr#(X)
p39: add#(mark(X1),X2) -> add#(X1,X2)
p40: add#(X1,mark(X2)) -> add#(X1,X2)
p41: dbl#(mark(X)) -> dbl#(X)
p42: first#(mark(X1),X2) -> first#(X1,X2)
p43: first#(X1,mark(X2)) -> first#(X1,X2)
p44: proper#(terms(X)) -> terms#(proper(X))
p45: proper#(terms(X)) -> proper#(X)
p46: proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
p47: proper#(cons(X1,X2)) -> proper#(X1)
p48: proper#(cons(X1,X2)) -> proper#(X2)
p49: proper#(recip(X)) -> recip#(proper(X))
p50: proper#(recip(X)) -> proper#(X)
p51: proper#(sqr(X)) -> sqr#(proper(X))
p52: proper#(sqr(X)) -> proper#(X)
p53: proper#(s(X)) -> s#(proper(X))
p54: proper#(s(X)) -> proper#(X)
p55: proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
p56: proper#(add(X1,X2)) -> proper#(X1)
p57: proper#(add(X1,X2)) -> proper#(X2)
p58: proper#(dbl(X)) -> dbl#(proper(X))
p59: proper#(dbl(X)) -> proper#(X)
p60: proper#(first(X1,X2)) -> first#(proper(X1),proper(X2))
p61: proper#(first(X1,X2)) -> proper#(X1)
p62: proper#(first(X1,X2)) -> proper#(X2)
p63: terms#(ok(X)) -> terms#(X)
p64: cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
p65: recip#(ok(X)) -> recip#(X)
p66: sqr#(ok(X)) -> sqr#(X)
p67: s#(ok(X)) -> s#(X)
p68: add#(ok(X1),ok(X2)) -> add#(X1,X2)
p69: dbl#(ok(X)) -> dbl#(X)
p70: first#(ok(X1),ok(X2)) -> first#(X1,X2)
p71: top#(mark(X)) -> top#(proper(X))
p72: top#(mark(X)) -> proper#(X)
p73: top#(ok(X)) -> top#(active(X))
p74: top#(ok(X)) -> active#(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(terms(X)) -> terms(active(X))
r11: active(cons(X1,X2)) -> cons(active(X1),X2)
r12: active(recip(X)) -> recip(active(X))
r13: active(sqr(X)) -> sqr(active(X))
r14: active(add(X1,X2)) -> add(active(X1),X2)
r15: active(add(X1,X2)) -> add(X1,active(X2))
r16: active(dbl(X)) -> dbl(active(X))
r17: active(first(X1,X2)) -> first(active(X1),X2)
r18: active(first(X1,X2)) -> first(X1,active(X2))
r19: terms(mark(X)) -> mark(terms(X))
r20: cons(mark(X1),X2) -> mark(cons(X1,X2))
r21: recip(mark(X)) -> mark(recip(X))
r22: sqr(mark(X)) -> mark(sqr(X))
r23: add(mark(X1),X2) -> mark(add(X1,X2))
r24: add(X1,mark(X2)) -> mark(add(X1,X2))
r25: dbl(mark(X)) -> mark(dbl(X))
r26: first(mark(X1),X2) -> mark(first(X1,X2))
r27: first(X1,mark(X2)) -> mark(first(X1,X2))
r28: proper(terms(X)) -> terms(proper(X))
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(recip(X)) -> recip(proper(X))
r31: proper(sqr(X)) -> sqr(proper(X))
r32: proper(s(X)) -> s(proper(X))
r33: proper(|0|()) -> ok(|0|())
r34: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r35: proper(dbl(X)) -> dbl(proper(X))
r36: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r37: proper(nil()) -> ok(nil())
r38: terms(ok(X)) -> ok(terms(X))
r39: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r40: recip(ok(X)) -> ok(recip(X))
r41: sqr(ok(X)) -> ok(sqr(X))
r42: s(ok(X)) -> ok(s(X))
r43: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r44: dbl(ok(X)) -> ok(dbl(X))
r45: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r46: top(mark(X)) -> top(proper(X))
r47: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p71, p73}
  {p18, p20, p22, p24, p26, p28, p30, p32, p34}
  {p45, p47, p48, p50, p52, p54, p56, p57, p59, p61, p62}
  {p36, p64}
  {p37, p65}
  {p38, p66}
  {p35, p63}
  {p67}
  {p39, p40, p68}
  {p41, p69}
  {p42, p43, p70}


-- Reduction pair.

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

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

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      top#_A(x1) = x1
      ok_A(x1) = ((1,0),(1,0)) x1
      active_A(x1) = x1 + (0,1)
      mark_A(x1) = x1 + (6,18)
      proper_A(x1) = x1 + (0,1)
      terms_A(x1) = x1 + (15,16)
      cons_A(x1,x2) = x1 + (0,1)
      recip_A(x1) = ((1,0),(1,0)) x1 + (1,13)
      sqr_A(x1) = x1 + (7,8)
      add_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (7,17)
      dbl_A(x1) = ((1,0),(1,0)) x1 + (7,16)
      first_A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (7,13)
      s_A(x1) = ((0,0),(1,0)) x1 + (2,10)
      |0|_A() = (1,10)
      nil_A() = (1,1)

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      top#_A(x1) = x1
      ok_A(x1) = x1 + (0,2)
      active_A(x1) = x1 + (0,1)
      terms_A(x1) = x1 + (2,1)
      mark_A(x1) = (1,6)
      cons_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (1,0)
      recip_A(x1) = x1 + (1,1)
      sqr_A(x1) = x1 + (1,1)
      add_A(x1,x2) = x1 + x2 + (1,0)
      dbl_A(x1) = ((1,0),(1,1)) x1
      first_A(x1,x2) = x1 + (2,3)
      s_A(x1) = x1 + (5,1)
      |0|_A() = (3,3)
      nil_A() = (1,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: active#(first(X1,X2)) -> active#(X2)
p2: active#(first(X1,X2)) -> active#(X1)
p3: active#(dbl(X)) -> active#(X)
p4: active#(add(X1,X2)) -> active#(X2)
p5: active#(add(X1,X2)) -> active#(X1)
p6: active#(sqr(X)) -> active#(X)
p7: active#(recip(X)) -> active#(X)
p8: active#(cons(X1,X2)) -> active#(X1)
p9: active#(terms(X)) -> active#(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(terms(X)) -> terms(active(X))
r11: active(cons(X1,X2)) -> cons(active(X1),X2)
r12: active(recip(X)) -> recip(active(X))
r13: active(sqr(X)) -> sqr(active(X))
r14: active(add(X1,X2)) -> add(active(X1),X2)
r15: active(add(X1,X2)) -> add(X1,active(X2))
r16: active(dbl(X)) -> dbl(active(X))
r17: active(first(X1,X2)) -> first(active(X1),X2)
r18: active(first(X1,X2)) -> first(X1,active(X2))
r19: terms(mark(X)) -> mark(terms(X))
r20: cons(mark(X1),X2) -> mark(cons(X1,X2))
r21: recip(mark(X)) -> mark(recip(X))
r22: sqr(mark(X)) -> mark(sqr(X))
r23: add(mark(X1),X2) -> mark(add(X1,X2))
r24: add(X1,mark(X2)) -> mark(add(X1,X2))
r25: dbl(mark(X)) -> mark(dbl(X))
r26: first(mark(X1),X2) -> mark(first(X1,X2))
r27: first(X1,mark(X2)) -> mark(first(X1,X2))
r28: proper(terms(X)) -> terms(proper(X))
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(recip(X)) -> recip(proper(X))
r31: proper(sqr(X)) -> sqr(proper(X))
r32: proper(s(X)) -> s(proper(X))
r33: proper(|0|()) -> ok(|0|())
r34: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r35: proper(dbl(X)) -> dbl(proper(X))
r36: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r37: proper(nil()) -> ok(nil())
r38: terms(ok(X)) -> ok(terms(X))
r39: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r40: recip(ok(X)) -> ok(recip(X))
r41: sqr(ok(X)) -> ok(sqr(X))
r42: s(ok(X)) -> ok(s(X))
r43: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r44: dbl(ok(X)) -> ok(dbl(X))
r45: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r46: top(mark(X)) -> top(proper(X))
r47: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      active#_A(x1) = ((1,0),(1,1)) x1
      first_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
      dbl_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      add_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (1,1)
      sqr_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      recip_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      cons_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
      terms_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      proper#_A(x1) = ((1,0),(1,1)) x1
      first_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
      dbl_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      add_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
      s_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      sqr_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      recip_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      cons_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
      terms_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11
  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

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      cons#_A(x1,x2) = x1 + ((1,0),(1,1)) x2
      mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      ok_A(x1) = ((1,0),(1,1)) x1 + (1,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#(ok(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(terms(X)) -> terms(active(X))
r11: active(cons(X1,X2)) -> cons(active(X1),X2)
r12: active(recip(X)) -> recip(active(X))
r13: active(sqr(X)) -> sqr(active(X))
r14: active(add(X1,X2)) -> add(active(X1),X2)
r15: active(add(X1,X2)) -> add(X1,active(X2))
r16: active(dbl(X)) -> dbl(active(X))
r17: active(first(X1,X2)) -> first(active(X1),X2)
r18: active(first(X1,X2)) -> first(X1,active(X2))
r19: terms(mark(X)) -> mark(terms(X))
r20: cons(mark(X1),X2) -> mark(cons(X1,X2))
r21: recip(mark(X)) -> mark(recip(X))
r22: sqr(mark(X)) -> mark(sqr(X))
r23: add(mark(X1),X2) -> mark(add(X1,X2))
r24: add(X1,mark(X2)) -> mark(add(X1,X2))
r25: dbl(mark(X)) -> mark(dbl(X))
r26: first(mark(X1),X2) -> mark(first(X1,X2))
r27: first(X1,mark(X2)) -> mark(first(X1,X2))
r28: proper(terms(X)) -> terms(proper(X))
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(recip(X)) -> recip(proper(X))
r31: proper(sqr(X)) -> sqr(proper(X))
r32: proper(s(X)) -> s(proper(X))
r33: proper(|0|()) -> ok(|0|())
r34: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r35: proper(dbl(X)) -> dbl(proper(X))
r36: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r37: proper(nil()) -> ok(nil())
r38: terms(ok(X)) -> ok(terms(X))
r39: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r40: recip(ok(X)) -> ok(recip(X))
r41: sqr(ok(X)) -> ok(sqr(X))
r42: s(ok(X)) -> ok(s(X))
r43: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r44: dbl(ok(X)) -> ok(dbl(X))
r45: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r46: top(mark(X)) -> top(proper(X))
r47: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      recip#_A(x1) = ((1,0),(1,0)) x1
      mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      ok_A(x1) = ((1,0),(1,1)) x1 + (1,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: sqr#(mark(X)) -> sqr#(X)
p2: sqr#(ok(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(terms(X)) -> terms(active(X))
r11: active(cons(X1,X2)) -> cons(active(X1),X2)
r12: active(recip(X)) -> recip(active(X))
r13: active(sqr(X)) -> sqr(active(X))
r14: active(add(X1,X2)) -> add(active(X1),X2)
r15: active(add(X1,X2)) -> add(X1,active(X2))
r16: active(dbl(X)) -> dbl(active(X))
r17: active(first(X1,X2)) -> first(active(X1),X2)
r18: active(first(X1,X2)) -> first(X1,active(X2))
r19: terms(mark(X)) -> mark(terms(X))
r20: cons(mark(X1),X2) -> mark(cons(X1,X2))
r21: recip(mark(X)) -> mark(recip(X))
r22: sqr(mark(X)) -> mark(sqr(X))
r23: add(mark(X1),X2) -> mark(add(X1,X2))
r24: add(X1,mark(X2)) -> mark(add(X1,X2))
r25: dbl(mark(X)) -> mark(dbl(X))
r26: first(mark(X1),X2) -> mark(first(X1,X2))
r27: first(X1,mark(X2)) -> mark(first(X1,X2))
r28: proper(terms(X)) -> terms(proper(X))
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(recip(X)) -> recip(proper(X))
r31: proper(sqr(X)) -> sqr(proper(X))
r32: proper(s(X)) -> s(proper(X))
r33: proper(|0|()) -> ok(|0|())
r34: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r35: proper(dbl(X)) -> dbl(proper(X))
r36: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r37: proper(nil()) -> ok(nil())
r38: terms(ok(X)) -> ok(terms(X))
r39: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r40: recip(ok(X)) -> ok(recip(X))
r41: sqr(ok(X)) -> ok(sqr(X))
r42: s(ok(X)) -> ok(s(X))
r43: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r44: dbl(ok(X)) -> ok(dbl(X))
r45: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r46: top(mark(X)) -> top(proper(X))
r47: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      sqr#_A(x1) = x1
      mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      ok_A(x1) = ((1,0),(1,1)) x1 + (1,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: terms#(mark(X)) -> terms#(X)
p2: terms#(ok(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(terms(X)) -> terms(active(X))
r11: active(cons(X1,X2)) -> cons(active(X1),X2)
r12: active(recip(X)) -> recip(active(X))
r13: active(sqr(X)) -> sqr(active(X))
r14: active(add(X1,X2)) -> add(active(X1),X2)
r15: active(add(X1,X2)) -> add(X1,active(X2))
r16: active(dbl(X)) -> dbl(active(X))
r17: active(first(X1,X2)) -> first(active(X1),X2)
r18: active(first(X1,X2)) -> first(X1,active(X2))
r19: terms(mark(X)) -> mark(terms(X))
r20: cons(mark(X1),X2) -> mark(cons(X1,X2))
r21: recip(mark(X)) -> mark(recip(X))
r22: sqr(mark(X)) -> mark(sqr(X))
r23: add(mark(X1),X2) -> mark(add(X1,X2))
r24: add(X1,mark(X2)) -> mark(add(X1,X2))
r25: dbl(mark(X)) -> mark(dbl(X))
r26: first(mark(X1),X2) -> mark(first(X1,X2))
r27: first(X1,mark(X2)) -> mark(first(X1,X2))
r28: proper(terms(X)) -> terms(proper(X))
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(recip(X)) -> recip(proper(X))
r31: proper(sqr(X)) -> sqr(proper(X))
r32: proper(s(X)) -> s(proper(X))
r33: proper(|0|()) -> ok(|0|())
r34: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r35: proper(dbl(X)) -> dbl(proper(X))
r36: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r37: proper(nil()) -> ok(nil())
r38: terms(ok(X)) -> ok(terms(X))
r39: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r40: recip(ok(X)) -> ok(recip(X))
r41: sqr(ok(X)) -> ok(sqr(X))
r42: s(ok(X)) -> ok(s(X))
r43: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r44: dbl(ok(X)) -> ok(dbl(X))
r45: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r46: top(mark(X)) -> top(proper(X))
r47: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      terms#_A(x1) = x1
      mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      ok_A(x1) = ((1,0),(1,1)) x1 + (1,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: s#(ok(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(terms(X)) -> terms(active(X))
r11: active(cons(X1,X2)) -> cons(active(X1),X2)
r12: active(recip(X)) -> recip(active(X))
r13: active(sqr(X)) -> sqr(active(X))
r14: active(add(X1,X2)) -> add(active(X1),X2)
r15: active(add(X1,X2)) -> add(X1,active(X2))
r16: active(dbl(X)) -> dbl(active(X))
r17: active(first(X1,X2)) -> first(active(X1),X2)
r18: active(first(X1,X2)) -> first(X1,active(X2))
r19: terms(mark(X)) -> mark(terms(X))
r20: cons(mark(X1),X2) -> mark(cons(X1,X2))
r21: recip(mark(X)) -> mark(recip(X))
r22: sqr(mark(X)) -> mark(sqr(X))
r23: add(mark(X1),X2) -> mark(add(X1,X2))
r24: add(X1,mark(X2)) -> mark(add(X1,X2))
r25: dbl(mark(X)) -> mark(dbl(X))
r26: first(mark(X1),X2) -> mark(first(X1,X2))
r27: first(X1,mark(X2)) -> mark(first(X1,X2))
r28: proper(terms(X)) -> terms(proper(X))
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(recip(X)) -> recip(proper(X))
r31: proper(sqr(X)) -> sqr(proper(X))
r32: proper(s(X)) -> s(proper(X))
r33: proper(|0|()) -> ok(|0|())
r34: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r35: proper(dbl(X)) -> dbl(proper(X))
r36: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r37: proper(nil()) -> ok(nil())
r38: terms(ok(X)) -> ok(terms(X))
r39: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r40: recip(ok(X)) -> ok(recip(X))
r41: sqr(ok(X)) -> ok(sqr(X))
r42: s(ok(X)) -> ok(s(X))
r43: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r44: dbl(ok(X)) -> ok(dbl(X))
r45: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r46: top(mark(X)) -> top(proper(X))
r47: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      s#_A(x1) = x1
      ok_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1
  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

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      add#_A(x1,x2) = x1 + ((1,0),(1,1)) x2
      mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      ok_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2, p3

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      dbl#_A(x1) = x1
      mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      ok_A(x1) = ((1,0),(1,1)) x1 + (1,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: first#(mark(X1),X2) -> first#(X1,X2)
p2: first#(ok(X1),ok(X2)) -> first#(X1,X2)
p3: 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(terms(X)) -> terms(active(X))
r11: active(cons(X1,X2)) -> cons(active(X1),X2)
r12: active(recip(X)) -> recip(active(X))
r13: active(sqr(X)) -> sqr(active(X))
r14: active(add(X1,X2)) -> add(active(X1),X2)
r15: active(add(X1,X2)) -> add(X1,active(X2))
r16: active(dbl(X)) -> dbl(active(X))
r17: active(first(X1,X2)) -> first(active(X1),X2)
r18: active(first(X1,X2)) -> first(X1,active(X2))
r19: terms(mark(X)) -> mark(terms(X))
r20: cons(mark(X1),X2) -> mark(cons(X1,X2))
r21: recip(mark(X)) -> mark(recip(X))
r22: sqr(mark(X)) -> mark(sqr(X))
r23: add(mark(X1),X2) -> mark(add(X1,X2))
r24: add(X1,mark(X2)) -> mark(add(X1,X2))
r25: dbl(mark(X)) -> mark(dbl(X))
r26: first(mark(X1),X2) -> mark(first(X1,X2))
r27: first(X1,mark(X2)) -> mark(first(X1,X2))
r28: proper(terms(X)) -> terms(proper(X))
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(recip(X)) -> recip(proper(X))
r31: proper(sqr(X)) -> sqr(proper(X))
r32: proper(s(X)) -> s(proper(X))
r33: proper(|0|()) -> ok(|0|())
r34: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r35: proper(dbl(X)) -> dbl(proper(X))
r36: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r37: proper(nil()) -> ok(nil())
r38: terms(ok(X)) -> ok(terms(X))
r39: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r40: recip(ok(X)) -> ok(recip(X))
r41: sqr(ok(X)) -> ok(sqr(X))
r42: s(ok(X)) -> ok(s(X))
r43: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r44: dbl(ok(X)) -> ok(dbl(X))
r45: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r46: top(mark(X)) -> top(proper(X))
r47: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      first#_A(x1,x2) = x1 + ((1,0),(1,1)) x2
      mark_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      ok_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2, p3

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