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

The estimated dependency graph contains the following SCCs:

  {p74, p76}
  {p18, p20, p22, p24, p26, p28, p30, p32, p34, p36}
  {p48, p50, p51, p53, p55, p57, p59, p60, p62, p64, p65}
  {p38, p67}
  {p39, p68}
  {p40, p69}
  {p37, p66}
  {p41, p70}
  {p42, p43, p71}
  {p44, p72}
  {p45, p46, p73}


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

Take the reduction pair:

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

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

Take the reduction pair:

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

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1, p2, p4, p5

We remove them from the problem.

-- SCC decomposition.

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

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6}


-- Reduction pair.

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

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order
  
    precedence:
    
      active# > s > sqr > recip > cons > terms > dbl
    
  
    argument filter:
  
    pi(active#) = [1]
    pi(dbl) = 1
    pi(terms) = 1
    pi(cons) = [1, 2]
    pi(recip) = 1
    pi(sqr) = 1
    pi(s) = 1

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5}


-- Reduction pair.

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

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order
  
    precedence:
    
      active# > terms > recip > sqr > s > dbl
    
  
    argument filter:
  
    pi(active#) = 1
    pi(dbl) = [1]
    pi(s) = [1]
    pi(sqr) = [1]
    pi(recip) = 1
    pi(terms) = [1]

The next rules are strictly ordered:

  p1, p2, p3, p5

We remove them from the problem.

-- SCC decomposition.

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

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order
  
    precedence:
    
      recip > active#
    
  
    argument filter:
  
    pi(active#) = [1]
    pi(recip) = [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: 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(s(X)) -> s(active(X))
r15: active(add(X1,X2)) -> add(active(X1),X2)
r16: active(add(X1,X2)) -> add(X1,active(X2))
r17: active(dbl(X)) -> dbl(active(X))
r18: active(first(X1,X2)) -> first(active(X1),X2)
r19: active(first(X1,X2)) -> first(X1,active(X2))
r20: terms(mark(X)) -> mark(terms(X))
r21: cons(mark(X1),X2) -> mark(cons(X1,X2))
r22: recip(mark(X)) -> mark(recip(X))
r23: sqr(mark(X)) -> mark(sqr(X))
r24: s(mark(X)) -> mark(s(X))
r25: add(mark(X1),X2) -> mark(add(X1,X2))
r26: add(X1,mark(X2)) -> mark(add(X1,X2))
r27: dbl(mark(X)) -> mark(dbl(X))
r28: first(mark(X1),X2) -> mark(first(X1,X2))
r29: first(X1,mark(X2)) -> mark(first(X1,X2))
r30: proper(terms(X)) -> terms(proper(X))
r31: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r32: proper(recip(X)) -> recip(proper(X))
r33: proper(sqr(X)) -> sqr(proper(X))
r34: proper(s(X)) -> s(proper(X))
r35: proper(|0|()) -> ok(|0|())
r36: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r37: proper(dbl(X)) -> dbl(proper(X))
r38: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r39: proper(nil()) -> ok(nil())
r40: terms(ok(X)) -> ok(terms(X))
r41: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r42: recip(ok(X)) -> ok(recip(X))
r43: sqr(ok(X)) -> ok(sqr(X))
r44: s(ok(X)) -> ok(s(X))
r45: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r46: dbl(ok(X)) -> ok(dbl(X))
r47: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r48: top(mark(X)) -> top(proper(X))
r49: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order
  
    precedence:
    
      proper# > terms > cons > recip > sqr > s > add > dbl > first
    
  
    argument filter:
  
    pi(proper#) = 1
    pi(first) = [1, 2]
    pi(dbl) = [1]
    pi(add) = [1, 2]
    pi(s) = [1]
    pi(sqr) = [1]
    pi(recip) = [1]
    pi(cons) = [1, 2]
    pi(terms) = [1]

The next rules are strictly ordered:

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

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order
  
    precedence:
    
      cons# > ok > mark
    
  
    argument filter:
  
    pi(cons#) = 2
    pi(mark) = []
    pi(ok) = [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: cons#(mark(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(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(s(X)) -> s(active(X))
r15: active(add(X1,X2)) -> add(active(X1),X2)
r16: active(add(X1,X2)) -> add(X1,active(X2))
r17: active(dbl(X)) -> dbl(active(X))
r18: active(first(X1,X2)) -> first(active(X1),X2)
r19: active(first(X1,X2)) -> first(X1,active(X2))
r20: terms(mark(X)) -> mark(terms(X))
r21: cons(mark(X1),X2) -> mark(cons(X1,X2))
r22: recip(mark(X)) -> mark(recip(X))
r23: sqr(mark(X)) -> mark(sqr(X))
r24: s(mark(X)) -> mark(s(X))
r25: add(mark(X1),X2) -> mark(add(X1,X2))
r26: add(X1,mark(X2)) -> mark(add(X1,X2))
r27: dbl(mark(X)) -> mark(dbl(X))
r28: first(mark(X1),X2) -> mark(first(X1,X2))
r29: first(X1,mark(X2)) -> mark(first(X1,X2))
r30: proper(terms(X)) -> terms(proper(X))
r31: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r32: proper(recip(X)) -> recip(proper(X))
r33: proper(sqr(X)) -> sqr(proper(X))
r34: proper(s(X)) -> s(proper(X))
r35: proper(|0|()) -> ok(|0|())
r36: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r37: proper(dbl(X)) -> dbl(proper(X))
r38: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r39: proper(nil()) -> ok(nil())
r40: terms(ok(X)) -> ok(terms(X))
r41: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r42: recip(ok(X)) -> ok(recip(X))
r43: sqr(ok(X)) -> ok(sqr(X))
r44: s(ok(X)) -> ok(s(X))
r45: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r46: dbl(ok(X)) -> ok(dbl(X))
r47: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r48: top(mark(X)) -> top(proper(X))
r49: 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: cons#(mark(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(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(s(X)) -> s(active(X))
r15: active(add(X1,X2)) -> add(active(X1),X2)
r16: active(add(X1,X2)) -> add(X1,active(X2))
r17: active(dbl(X)) -> dbl(active(X))
r18: active(first(X1,X2)) -> first(active(X1),X2)
r19: active(first(X1,X2)) -> first(X1,active(X2))
r20: terms(mark(X)) -> mark(terms(X))
r21: cons(mark(X1),X2) -> mark(cons(X1,X2))
r22: recip(mark(X)) -> mark(recip(X))
r23: sqr(mark(X)) -> mark(sqr(X))
r24: s(mark(X)) -> mark(s(X))
r25: add(mark(X1),X2) -> mark(add(X1,X2))
r26: add(X1,mark(X2)) -> mark(add(X1,X2))
r27: dbl(mark(X)) -> mark(dbl(X))
r28: first(mark(X1),X2) -> mark(first(X1,X2))
r29: first(X1,mark(X2)) -> mark(first(X1,X2))
r30: proper(terms(X)) -> terms(proper(X))
r31: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r32: proper(recip(X)) -> recip(proper(X))
r33: proper(sqr(X)) -> sqr(proper(X))
r34: proper(s(X)) -> s(proper(X))
r35: proper(|0|()) -> ok(|0|())
r36: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r37: proper(dbl(X)) -> dbl(proper(X))
r38: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r39: proper(nil()) -> ok(nil())
r40: terms(ok(X)) -> ok(terms(X))
r41: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r42: recip(ok(X)) -> ok(recip(X))
r43: sqr(ok(X)) -> ok(sqr(X))
r44: s(ok(X)) -> ok(s(X))
r45: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r46: dbl(ok(X)) -> ok(dbl(X))
r47: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r48: top(mark(X)) -> top(proper(X))
r49: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order
  
    precedence:
    
      mark > cons#
    
  
    argument filter:
  
    pi(cons#) = [1, 2]
    pi(mark) = [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: 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(s(X)) -> s(active(X))
r15: active(add(X1,X2)) -> add(active(X1),X2)
r16: active(add(X1,X2)) -> add(X1,active(X2))
r17: active(dbl(X)) -> dbl(active(X))
r18: active(first(X1,X2)) -> first(active(X1),X2)
r19: active(first(X1,X2)) -> first(X1,active(X2))
r20: terms(mark(X)) -> mark(terms(X))
r21: cons(mark(X1),X2) -> mark(cons(X1,X2))
r22: recip(mark(X)) -> mark(recip(X))
r23: sqr(mark(X)) -> mark(sqr(X))
r24: s(mark(X)) -> mark(s(X))
r25: add(mark(X1),X2) -> mark(add(X1,X2))
r26: add(X1,mark(X2)) -> mark(add(X1,X2))
r27: dbl(mark(X)) -> mark(dbl(X))
r28: first(mark(X1),X2) -> mark(first(X1,X2))
r29: first(X1,mark(X2)) -> mark(first(X1,X2))
r30: proper(terms(X)) -> terms(proper(X))
r31: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r32: proper(recip(X)) -> recip(proper(X))
r33: proper(sqr(X)) -> sqr(proper(X))
r34: proper(s(X)) -> s(proper(X))
r35: proper(|0|()) -> ok(|0|())
r36: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r37: proper(dbl(X)) -> dbl(proper(X))
r38: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r39: proper(nil()) -> ok(nil())
r40: terms(ok(X)) -> ok(terms(X))
r41: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r42: recip(ok(X)) -> ok(recip(X))
r43: sqr(ok(X)) -> ok(sqr(X))
r44: s(ok(X)) -> ok(s(X))
r45: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r46: dbl(ok(X)) -> ok(dbl(X))
r47: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r48: top(mark(X)) -> top(proper(X))
r49: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order
  
    precedence:
    
      recip# > ok > mark
    
  
    argument filter:
  
    pi(recip#) = 1
    pi(mark) = [1]
    pi(ok) = [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(s(X)) -> s(active(X))
r15: active(add(X1,X2)) -> add(active(X1),X2)
r16: active(add(X1,X2)) -> add(X1,active(X2))
r17: active(dbl(X)) -> dbl(active(X))
r18: active(first(X1,X2)) -> first(active(X1),X2)
r19: active(first(X1,X2)) -> first(X1,active(X2))
r20: terms(mark(X)) -> mark(terms(X))
r21: cons(mark(X1),X2) -> mark(cons(X1,X2))
r22: recip(mark(X)) -> mark(recip(X))
r23: sqr(mark(X)) -> mark(sqr(X))
r24: s(mark(X)) -> mark(s(X))
r25: add(mark(X1),X2) -> mark(add(X1,X2))
r26: add(X1,mark(X2)) -> mark(add(X1,X2))
r27: dbl(mark(X)) -> mark(dbl(X))
r28: first(mark(X1),X2) -> mark(first(X1,X2))
r29: first(X1,mark(X2)) -> mark(first(X1,X2))
r30: proper(terms(X)) -> terms(proper(X))
r31: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r32: proper(recip(X)) -> recip(proper(X))
r33: proper(sqr(X)) -> sqr(proper(X))
r34: proper(s(X)) -> s(proper(X))
r35: proper(|0|()) -> ok(|0|())
r36: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r37: proper(dbl(X)) -> dbl(proper(X))
r38: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r39: proper(nil()) -> ok(nil())
r40: terms(ok(X)) -> ok(terms(X))
r41: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r42: recip(ok(X)) -> ok(recip(X))
r43: sqr(ok(X)) -> ok(sqr(X))
r44: s(ok(X)) -> ok(s(X))
r45: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r46: dbl(ok(X)) -> ok(dbl(X))
r47: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r48: top(mark(X)) -> top(proper(X))
r49: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order
  
    precedence:
    
      sqr# > ok > mark
    
  
    argument filter:
  
    pi(sqr#) = 1
    pi(mark) = [1]
    pi(ok) = [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(s(X)) -> s(active(X))
r15: active(add(X1,X2)) -> add(active(X1),X2)
r16: active(add(X1,X2)) -> add(X1,active(X2))
r17: active(dbl(X)) -> dbl(active(X))
r18: active(first(X1,X2)) -> first(active(X1),X2)
r19: active(first(X1,X2)) -> first(X1,active(X2))
r20: terms(mark(X)) -> mark(terms(X))
r21: cons(mark(X1),X2) -> mark(cons(X1,X2))
r22: recip(mark(X)) -> mark(recip(X))
r23: sqr(mark(X)) -> mark(sqr(X))
r24: s(mark(X)) -> mark(s(X))
r25: add(mark(X1),X2) -> mark(add(X1,X2))
r26: add(X1,mark(X2)) -> mark(add(X1,X2))
r27: dbl(mark(X)) -> mark(dbl(X))
r28: first(mark(X1),X2) -> mark(first(X1,X2))
r29: first(X1,mark(X2)) -> mark(first(X1,X2))
r30: proper(terms(X)) -> terms(proper(X))
r31: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r32: proper(recip(X)) -> recip(proper(X))
r33: proper(sqr(X)) -> sqr(proper(X))
r34: proper(s(X)) -> s(proper(X))
r35: proper(|0|()) -> ok(|0|())
r36: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r37: proper(dbl(X)) -> dbl(proper(X))
r38: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r39: proper(nil()) -> ok(nil())
r40: terms(ok(X)) -> ok(terms(X))
r41: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r42: recip(ok(X)) -> ok(recip(X))
r43: sqr(ok(X)) -> ok(sqr(X))
r44: s(ok(X)) -> ok(s(X))
r45: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r46: dbl(ok(X)) -> ok(dbl(X))
r47: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r48: top(mark(X)) -> top(proper(X))
r49: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order
  
    precedence:
    
      terms# > ok > mark
    
  
    argument filter:
  
    pi(terms#) = 1
    pi(mark) = [1]
    pi(ok) = [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#(mark(X)) -> s#(X)
p2: 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(s(X)) -> s(active(X))
r15: active(add(X1,X2)) -> add(active(X1),X2)
r16: active(add(X1,X2)) -> add(X1,active(X2))
r17: active(dbl(X)) -> dbl(active(X))
r18: active(first(X1,X2)) -> first(active(X1),X2)
r19: active(first(X1,X2)) -> first(X1,active(X2))
r20: terms(mark(X)) -> mark(terms(X))
r21: cons(mark(X1),X2) -> mark(cons(X1,X2))
r22: recip(mark(X)) -> mark(recip(X))
r23: sqr(mark(X)) -> mark(sqr(X))
r24: s(mark(X)) -> mark(s(X))
r25: add(mark(X1),X2) -> mark(add(X1,X2))
r26: add(X1,mark(X2)) -> mark(add(X1,X2))
r27: dbl(mark(X)) -> mark(dbl(X))
r28: first(mark(X1),X2) -> mark(first(X1,X2))
r29: first(X1,mark(X2)) -> mark(first(X1,X2))
r30: proper(terms(X)) -> terms(proper(X))
r31: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r32: proper(recip(X)) -> recip(proper(X))
r33: proper(sqr(X)) -> sqr(proper(X))
r34: proper(s(X)) -> s(proper(X))
r35: proper(|0|()) -> ok(|0|())
r36: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r37: proper(dbl(X)) -> dbl(proper(X))
r38: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r39: proper(nil()) -> ok(nil())
r40: terms(ok(X)) -> ok(terms(X))
r41: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r42: recip(ok(X)) -> ok(recip(X))
r43: sqr(ok(X)) -> ok(sqr(X))
r44: s(ok(X)) -> ok(s(X))
r45: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r46: dbl(ok(X)) -> ok(dbl(X))
r47: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r48: top(mark(X)) -> top(proper(X))
r49: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order
  
    precedence:
    
      s# > ok > mark
    
  
    argument filter:
  
    pi(s#) = 1
    pi(mark) = [1]
    pi(ok) = [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: 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(s(X)) -> s(active(X))
r15: active(add(X1,X2)) -> add(active(X1),X2)
r16: active(add(X1,X2)) -> add(X1,active(X2))
r17: active(dbl(X)) -> dbl(active(X))
r18: active(first(X1,X2)) -> first(active(X1),X2)
r19: active(first(X1,X2)) -> first(X1,active(X2))
r20: terms(mark(X)) -> mark(terms(X))
r21: cons(mark(X1),X2) -> mark(cons(X1,X2))
r22: recip(mark(X)) -> mark(recip(X))
r23: sqr(mark(X)) -> mark(sqr(X))
r24: s(mark(X)) -> mark(s(X))
r25: add(mark(X1),X2) -> mark(add(X1,X2))
r26: add(X1,mark(X2)) -> mark(add(X1,X2))
r27: dbl(mark(X)) -> mark(dbl(X))
r28: first(mark(X1),X2) -> mark(first(X1,X2))
r29: first(X1,mark(X2)) -> mark(first(X1,X2))
r30: proper(terms(X)) -> terms(proper(X))
r31: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r32: proper(recip(X)) -> recip(proper(X))
r33: proper(sqr(X)) -> sqr(proper(X))
r34: proper(s(X)) -> s(proper(X))
r35: proper(|0|()) -> ok(|0|())
r36: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r37: proper(dbl(X)) -> dbl(proper(X))
r38: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r39: proper(nil()) -> ok(nil())
r40: terms(ok(X)) -> ok(terms(X))
r41: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r42: recip(ok(X)) -> ok(recip(X))
r43: sqr(ok(X)) -> ok(sqr(X))
r44: s(ok(X)) -> ok(s(X))
r45: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r46: dbl(ok(X)) -> ok(dbl(X))
r47: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r48: top(mark(X)) -> top(proper(X))
r49: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p2, p3

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)

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order
  
    precedence:
    
      mark > add#
    
  
    argument filter:
  
    pi(add#) = [1, 2]
    pi(mark) = [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: 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(s(X)) -> s(active(X))
r15: active(add(X1,X2)) -> add(active(X1),X2)
r16: active(add(X1,X2)) -> add(X1,active(X2))
r17: active(dbl(X)) -> dbl(active(X))
r18: active(first(X1,X2)) -> first(active(X1),X2)
r19: active(first(X1,X2)) -> first(X1,active(X2))
r20: terms(mark(X)) -> mark(terms(X))
r21: cons(mark(X1),X2) -> mark(cons(X1,X2))
r22: recip(mark(X)) -> mark(recip(X))
r23: sqr(mark(X)) -> mark(sqr(X))
r24: s(mark(X)) -> mark(s(X))
r25: add(mark(X1),X2) -> mark(add(X1,X2))
r26: add(X1,mark(X2)) -> mark(add(X1,X2))
r27: dbl(mark(X)) -> mark(dbl(X))
r28: first(mark(X1),X2) -> mark(first(X1,X2))
r29: first(X1,mark(X2)) -> mark(first(X1,X2))
r30: proper(terms(X)) -> terms(proper(X))
r31: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r32: proper(recip(X)) -> recip(proper(X))
r33: proper(sqr(X)) -> sqr(proper(X))
r34: proper(s(X)) -> s(proper(X))
r35: proper(|0|()) -> ok(|0|())
r36: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r37: proper(dbl(X)) -> dbl(proper(X))
r38: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r39: proper(nil()) -> ok(nil())
r40: terms(ok(X)) -> ok(terms(X))
r41: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r42: recip(ok(X)) -> ok(recip(X))
r43: sqr(ok(X)) -> ok(sqr(X))
r44: s(ok(X)) -> ok(s(X))
r45: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r46: dbl(ok(X)) -> ok(dbl(X))
r47: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r48: top(mark(X)) -> top(proper(X))
r49: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order
  
    precedence:
    
      dbl# > ok > mark
    
  
    argument filter:
  
    pi(dbl#) = 1
    pi(mark) = [1]
    pi(ok) = [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(s(X)) -> s(active(X))
r15: active(add(X1,X2)) -> add(active(X1),X2)
r16: active(add(X1,X2)) -> add(X1,active(X2))
r17: active(dbl(X)) -> dbl(active(X))
r18: active(first(X1,X2)) -> first(active(X1),X2)
r19: active(first(X1,X2)) -> first(X1,active(X2))
r20: terms(mark(X)) -> mark(terms(X))
r21: cons(mark(X1),X2) -> mark(cons(X1,X2))
r22: recip(mark(X)) -> mark(recip(X))
r23: sqr(mark(X)) -> mark(sqr(X))
r24: s(mark(X)) -> mark(s(X))
r25: add(mark(X1),X2) -> mark(add(X1,X2))
r26: add(X1,mark(X2)) -> mark(add(X1,X2))
r27: dbl(mark(X)) -> mark(dbl(X))
r28: first(mark(X1),X2) -> mark(first(X1,X2))
r29: first(X1,mark(X2)) -> mark(first(X1,X2))
r30: proper(terms(X)) -> terms(proper(X))
r31: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r32: proper(recip(X)) -> recip(proper(X))
r33: proper(sqr(X)) -> sqr(proper(X))
r34: proper(s(X)) -> s(proper(X))
r35: proper(|0|()) -> ok(|0|())
r36: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r37: proper(dbl(X)) -> dbl(proper(X))
r38: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r39: proper(nil()) -> ok(nil())
r40: terms(ok(X)) -> ok(terms(X))
r41: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r42: recip(ok(X)) -> ok(recip(X))
r43: sqr(ok(X)) -> ok(sqr(X))
r44: s(ok(X)) -> ok(s(X))
r45: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r46: dbl(ok(X)) -> ok(dbl(X))
r47: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r48: top(mark(X)) -> top(proper(X))
r49: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p2, p3

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)

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

  p1

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