YES

We show the termination of the TRS R:

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

The estimated dependency graph contains the following SCCs:

  {p82, p84}
  {p20, p22, p24, p26, p28, p30, p32, p34, p36, p38, p40}
  {p53, p55, p56, p58, p60, p62, p64, p65, p67, p69, p70, p72}
  {p42, p74}
  {p43, p75}
  {p44, p76}
  {p41, p73}
  {p45, p77}
  {p46, p47, p78}
  {p48, p79}
  {p49, p50, p80}
  {p51, p81}


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

Take the reduction pair:

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

Take the reduction pair:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      active# > terms > cons > recip > sqr > s > add > dbl > first > half
    
    argument filter:
  
      pi(active#) = 1
      pi(half) = [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, p3, p4, p5, p6, p7, p9, p11

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: active(terms(X)) -> terms(active(X))
r15: active(cons(X1,X2)) -> cons(active(X1),X2)
r16: active(recip(X)) -> recip(active(X))
r17: active(sqr(X)) -> sqr(active(X))
r18: active(s(X)) -> s(active(X))
r19: active(add(X1,X2)) -> add(active(X1),X2)
r20: active(add(X1,X2)) -> add(X1,active(X2))
r21: active(dbl(X)) -> dbl(active(X))
r22: active(first(X1,X2)) -> first(active(X1),X2)
r23: active(first(X1,X2)) -> first(X1,active(X2))
r24: active(half(X)) -> half(active(X))
r25: terms(mark(X)) -> mark(terms(X))
r26: cons(mark(X1),X2) -> mark(cons(X1,X2))
r27: recip(mark(X)) -> mark(recip(X))
r28: sqr(mark(X)) -> mark(sqr(X))
r29: s(mark(X)) -> mark(s(X))
r30: add(mark(X1),X2) -> mark(add(X1,X2))
r31: add(X1,mark(X2)) -> mark(add(X1,X2))
r32: dbl(mark(X)) -> mark(dbl(X))
r33: first(mark(X1),X2) -> mark(first(X1,X2))
r34: first(X1,mark(X2)) -> mark(first(X1,X2))
r35: half(mark(X)) -> mark(half(X))
r36: proper(terms(X)) -> terms(proper(X))
r37: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r38: proper(recip(X)) -> recip(proper(X))
r39: proper(sqr(X)) -> sqr(proper(X))
r40: proper(s(X)) -> s(proper(X))
r41: proper(|0|()) -> ok(|0|())
r42: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r43: proper(dbl(X)) -> dbl(proper(X))
r44: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r45: proper(nil()) -> ok(nil())
r46: proper(half(X)) -> half(proper(X))
r47: terms(ok(X)) -> ok(terms(X))
r48: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r49: recip(ok(X)) -> ok(recip(X))
r50: sqr(ok(X)) -> ok(sqr(X))
r51: s(ok(X)) -> ok(s(X))
r52: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r53: dbl(ok(X)) -> ok(dbl(X))
r54: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r55: half(ok(X)) -> ok(half(X))
r56: top(mark(X)) -> top(proper(X))
r57: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

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

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: active(terms(X)) -> terms(active(X))
r15: active(cons(X1,X2)) -> cons(active(X1),X2)
r16: active(recip(X)) -> recip(active(X))
r17: active(sqr(X)) -> sqr(active(X))
r18: active(s(X)) -> s(active(X))
r19: active(add(X1,X2)) -> add(active(X1),X2)
r20: active(add(X1,X2)) -> add(X1,active(X2))
r21: active(dbl(X)) -> dbl(active(X))
r22: active(first(X1,X2)) -> first(active(X1),X2)
r23: active(first(X1,X2)) -> first(X1,active(X2))
r24: active(half(X)) -> half(active(X))
r25: terms(mark(X)) -> mark(terms(X))
r26: cons(mark(X1),X2) -> mark(cons(X1,X2))
r27: recip(mark(X)) -> mark(recip(X))
r28: sqr(mark(X)) -> mark(sqr(X))
r29: s(mark(X)) -> mark(s(X))
r30: add(mark(X1),X2) -> mark(add(X1,X2))
r31: add(X1,mark(X2)) -> mark(add(X1,X2))
r32: dbl(mark(X)) -> mark(dbl(X))
r33: first(mark(X1),X2) -> mark(first(X1,X2))
r34: first(X1,mark(X2)) -> mark(first(X1,X2))
r35: half(mark(X)) -> mark(half(X))
r36: proper(terms(X)) -> terms(proper(X))
r37: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r38: proper(recip(X)) -> recip(proper(X))
r39: proper(sqr(X)) -> sqr(proper(X))
r40: proper(s(X)) -> s(proper(X))
r41: proper(|0|()) -> ok(|0|())
r42: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r43: proper(dbl(X)) -> dbl(proper(X))
r44: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r45: proper(nil()) -> ok(nil())
r46: proper(half(X)) -> half(proper(X))
r47: terms(ok(X)) -> ok(terms(X))
r48: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r49: recip(ok(X)) -> ok(recip(X))
r50: sqr(ok(X)) -> ok(sqr(X))
r51: s(ok(X)) -> ok(s(X))
r52: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r53: dbl(ok(X)) -> ok(dbl(X))
r54: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r55: half(ok(X)) -> ok(half(X))
r56: top(mark(X)) -> top(proper(X))
r57: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      proper# > terms > cons > recip > sqr > s > add > dbl > first > half
    
    argument filter:
  
      pi(proper#) = 1
      pi(half) = [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, p12
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    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(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: active(terms(X)) -> terms(active(X))
r15: active(cons(X1,X2)) -> cons(active(X1),X2)
r16: active(recip(X)) -> recip(active(X))
r17: active(sqr(X)) -> sqr(active(X))
r18: active(s(X)) -> s(active(X))
r19: active(add(X1,X2)) -> add(active(X1),X2)
r20: active(add(X1,X2)) -> add(X1,active(X2))
r21: active(dbl(X)) -> dbl(active(X))
r22: active(first(X1,X2)) -> first(active(X1),X2)
r23: active(first(X1,X2)) -> first(X1,active(X2))
r24: active(half(X)) -> half(active(X))
r25: terms(mark(X)) -> mark(terms(X))
r26: cons(mark(X1),X2) -> mark(cons(X1,X2))
r27: recip(mark(X)) -> mark(recip(X))
r28: sqr(mark(X)) -> mark(sqr(X))
r29: s(mark(X)) -> mark(s(X))
r30: add(mark(X1),X2) -> mark(add(X1,X2))
r31: add(X1,mark(X2)) -> mark(add(X1,X2))
r32: dbl(mark(X)) -> mark(dbl(X))
r33: first(mark(X1),X2) -> mark(first(X1,X2))
r34: first(X1,mark(X2)) -> mark(first(X1,X2))
r35: half(mark(X)) -> mark(half(X))
r36: proper(terms(X)) -> terms(proper(X))
r37: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r38: proper(recip(X)) -> recip(proper(X))
r39: proper(sqr(X)) -> sqr(proper(X))
r40: proper(s(X)) -> s(proper(X))
r41: proper(|0|()) -> ok(|0|())
r42: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r43: proper(dbl(X)) -> dbl(proper(X))
r44: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r45: proper(nil()) -> ok(nil())
r46: proper(half(X)) -> half(proper(X))
r47: terms(ok(X)) -> ok(terms(X))
r48: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r49: recip(ok(X)) -> ok(recip(X))
r50: sqr(ok(X)) -> ok(sqr(X))
r51: s(ok(X)) -> ok(s(X))
r52: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r53: dbl(ok(X)) -> ok(dbl(X))
r54: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r55: half(ok(X)) -> ok(half(X))
r56: top(mark(X)) -> top(proper(X))
r57: 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(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: active(terms(X)) -> terms(active(X))
r15: active(cons(X1,X2)) -> cons(active(X1),X2)
r16: active(recip(X)) -> recip(active(X))
r17: active(sqr(X)) -> sqr(active(X))
r18: active(s(X)) -> s(active(X))
r19: active(add(X1,X2)) -> add(active(X1),X2)
r20: active(add(X1,X2)) -> add(X1,active(X2))
r21: active(dbl(X)) -> dbl(active(X))
r22: active(first(X1,X2)) -> first(active(X1),X2)
r23: active(first(X1,X2)) -> first(X1,active(X2))
r24: active(half(X)) -> half(active(X))
r25: terms(mark(X)) -> mark(terms(X))
r26: cons(mark(X1),X2) -> mark(cons(X1,X2))
r27: recip(mark(X)) -> mark(recip(X))
r28: sqr(mark(X)) -> mark(sqr(X))
r29: s(mark(X)) -> mark(s(X))
r30: add(mark(X1),X2) -> mark(add(X1,X2))
r31: add(X1,mark(X2)) -> mark(add(X1,X2))
r32: dbl(mark(X)) -> mark(dbl(X))
r33: first(mark(X1),X2) -> mark(first(X1,X2))
r34: first(X1,mark(X2)) -> mark(first(X1,X2))
r35: half(mark(X)) -> mark(half(X))
r36: proper(terms(X)) -> terms(proper(X))
r37: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r38: proper(recip(X)) -> recip(proper(X))
r39: proper(sqr(X)) -> sqr(proper(X))
r40: proper(s(X)) -> s(proper(X))
r41: proper(|0|()) -> ok(|0|())
r42: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r43: proper(dbl(X)) -> dbl(proper(X))
r44: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r45: proper(nil()) -> ok(nil())
r46: proper(half(X)) -> half(proper(X))
r47: terms(ok(X)) -> ok(terms(X))
r48: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r49: recip(ok(X)) -> ok(recip(X))
r50: sqr(ok(X)) -> ok(sqr(X))
r51: s(ok(X)) -> ok(s(X))
r52: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r53: dbl(ok(X)) -> ok(dbl(X))
r54: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r55: half(ok(X)) -> ok(half(X))
r56: top(mark(X)) -> top(proper(X))
r57: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      mark > cons#
    
    argument filter:
  
      pi(cons#) = [1, 2]
      pi(mark) = [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, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    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(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: active(terms(X)) -> terms(active(X))
r15: active(cons(X1,X2)) -> cons(active(X1),X2)
r16: active(recip(X)) -> recip(active(X))
r17: active(sqr(X)) -> sqr(active(X))
r18: active(s(X)) -> s(active(X))
r19: active(add(X1,X2)) -> add(active(X1),X2)
r20: active(add(X1,X2)) -> add(X1,active(X2))
r21: active(dbl(X)) -> dbl(active(X))
r22: active(first(X1,X2)) -> first(active(X1),X2)
r23: active(first(X1,X2)) -> first(X1,active(X2))
r24: active(half(X)) -> half(active(X))
r25: terms(mark(X)) -> mark(terms(X))
r26: cons(mark(X1),X2) -> mark(cons(X1,X2))
r27: recip(mark(X)) -> mark(recip(X))
r28: sqr(mark(X)) -> mark(sqr(X))
r29: s(mark(X)) -> mark(s(X))
r30: add(mark(X1),X2) -> mark(add(X1,X2))
r31: add(X1,mark(X2)) -> mark(add(X1,X2))
r32: dbl(mark(X)) -> mark(dbl(X))
r33: first(mark(X1),X2) -> mark(first(X1,X2))
r34: first(X1,mark(X2)) -> mark(first(X1,X2))
r35: half(mark(X)) -> mark(half(X))
r36: proper(terms(X)) -> terms(proper(X))
r37: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r38: proper(recip(X)) -> recip(proper(X))
r39: proper(sqr(X)) -> sqr(proper(X))
r40: proper(s(X)) -> s(proper(X))
r41: proper(|0|()) -> ok(|0|())
r42: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r43: proper(dbl(X)) -> dbl(proper(X))
r44: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r45: proper(nil()) -> ok(nil())
r46: proper(half(X)) -> half(proper(X))
r47: terms(ok(X)) -> ok(terms(X))
r48: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r49: recip(ok(X)) -> ok(recip(X))
r50: sqr(ok(X)) -> ok(sqr(X))
r51: s(ok(X)) -> ok(s(X))
r52: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r53: dbl(ok(X)) -> ok(dbl(X))
r54: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r55: half(ok(X)) -> ok(half(X))
r56: top(mark(X)) -> top(proper(X))
r57: 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(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: active(terms(X)) -> terms(active(X))
r15: active(cons(X1,X2)) -> cons(active(X1),X2)
r16: active(recip(X)) -> recip(active(X))
r17: active(sqr(X)) -> sqr(active(X))
r18: active(s(X)) -> s(active(X))
r19: active(add(X1,X2)) -> add(active(X1),X2)
r20: active(add(X1,X2)) -> add(X1,active(X2))
r21: active(dbl(X)) -> dbl(active(X))
r22: active(first(X1,X2)) -> first(active(X1),X2)
r23: active(first(X1,X2)) -> first(X1,active(X2))
r24: active(half(X)) -> half(active(X))
r25: terms(mark(X)) -> mark(terms(X))
r26: cons(mark(X1),X2) -> mark(cons(X1,X2))
r27: recip(mark(X)) -> mark(recip(X))
r28: sqr(mark(X)) -> mark(sqr(X))
r29: s(mark(X)) -> mark(s(X))
r30: add(mark(X1),X2) -> mark(add(X1,X2))
r31: add(X1,mark(X2)) -> mark(add(X1,X2))
r32: dbl(mark(X)) -> mark(dbl(X))
r33: first(mark(X1),X2) -> mark(first(X1,X2))
r34: first(X1,mark(X2)) -> mark(first(X1,X2))
r35: half(mark(X)) -> mark(half(X))
r36: proper(terms(X)) -> terms(proper(X))
r37: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r38: proper(recip(X)) -> recip(proper(X))
r39: proper(sqr(X)) -> sqr(proper(X))
r40: proper(s(X)) -> s(proper(X))
r41: proper(|0|()) -> ok(|0|())
r42: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r43: proper(dbl(X)) -> dbl(proper(X))
r44: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r45: proper(nil()) -> ok(nil())
r46: proper(half(X)) -> half(proper(X))
r47: terms(ok(X)) -> ok(terms(X))
r48: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r49: recip(ok(X)) -> ok(recip(X))
r50: sqr(ok(X)) -> ok(sqr(X))
r51: s(ok(X)) -> ok(s(X))
r52: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r53: dbl(ok(X)) -> ok(dbl(X))
r54: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r55: half(ok(X)) -> ok(half(X))
r56: top(mark(X)) -> top(proper(X))
r57: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      mark > add#
    
    argument filter:
  
      pi(add#) = [1, 2]
      pi(mark) = [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, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    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(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: active(terms(X)) -> terms(active(X))
r15: active(cons(X1,X2)) -> cons(active(X1),X2)
r16: active(recip(X)) -> recip(active(X))
r17: active(sqr(X)) -> sqr(active(X))
r18: active(s(X)) -> s(active(X))
r19: active(add(X1,X2)) -> add(active(X1),X2)
r20: active(add(X1,X2)) -> add(X1,active(X2))
r21: active(dbl(X)) -> dbl(active(X))
r22: active(first(X1,X2)) -> first(active(X1),X2)
r23: active(first(X1,X2)) -> first(X1,active(X2))
r24: active(half(X)) -> half(active(X))
r25: terms(mark(X)) -> mark(terms(X))
r26: cons(mark(X1),X2) -> mark(cons(X1,X2))
r27: recip(mark(X)) -> mark(recip(X))
r28: sqr(mark(X)) -> mark(sqr(X))
r29: s(mark(X)) -> mark(s(X))
r30: add(mark(X1),X2) -> mark(add(X1,X2))
r31: add(X1,mark(X2)) -> mark(add(X1,X2))
r32: dbl(mark(X)) -> mark(dbl(X))
r33: first(mark(X1),X2) -> mark(first(X1,X2))
r34: first(X1,mark(X2)) -> mark(first(X1,X2))
r35: half(mark(X)) -> mark(half(X))
r36: proper(terms(X)) -> terms(proper(X))
r37: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r38: proper(recip(X)) -> recip(proper(X))
r39: proper(sqr(X)) -> sqr(proper(X))
r40: proper(s(X)) -> s(proper(X))
r41: proper(|0|()) -> ok(|0|())
r42: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r43: proper(dbl(X)) -> dbl(proper(X))
r44: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r45: proper(nil()) -> ok(nil())
r46: proper(half(X)) -> half(proper(X))
r47: terms(ok(X)) -> ok(terms(X))
r48: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r49: recip(ok(X)) -> ok(recip(X))
r50: sqr(ok(X)) -> ok(sqr(X))
r51: s(ok(X)) -> ok(s(X))
r52: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r53: dbl(ok(X)) -> ok(dbl(X))
r54: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r55: half(ok(X)) -> ok(half(X))
r56: top(mark(X)) -> top(proper(X))
r57: 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(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: active(terms(X)) -> terms(active(X))
r15: active(cons(X1,X2)) -> cons(active(X1),X2)
r16: active(recip(X)) -> recip(active(X))
r17: active(sqr(X)) -> sqr(active(X))
r18: active(s(X)) -> s(active(X))
r19: active(add(X1,X2)) -> add(active(X1),X2)
r20: active(add(X1,X2)) -> add(X1,active(X2))
r21: active(dbl(X)) -> dbl(active(X))
r22: active(first(X1,X2)) -> first(active(X1),X2)
r23: active(first(X1,X2)) -> first(X1,active(X2))
r24: active(half(X)) -> half(active(X))
r25: terms(mark(X)) -> mark(terms(X))
r26: cons(mark(X1),X2) -> mark(cons(X1,X2))
r27: recip(mark(X)) -> mark(recip(X))
r28: sqr(mark(X)) -> mark(sqr(X))
r29: s(mark(X)) -> mark(s(X))
r30: add(mark(X1),X2) -> mark(add(X1,X2))
r31: add(X1,mark(X2)) -> mark(add(X1,X2))
r32: dbl(mark(X)) -> mark(dbl(X))
r33: first(mark(X1),X2) -> mark(first(X1,X2))
r34: first(X1,mark(X2)) -> mark(first(X1,X2))
r35: half(mark(X)) -> mark(half(X))
r36: proper(terms(X)) -> terms(proper(X))
r37: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r38: proper(recip(X)) -> recip(proper(X))
r39: proper(sqr(X)) -> sqr(proper(X))
r40: proper(s(X)) -> s(proper(X))
r41: proper(|0|()) -> ok(|0|())
r42: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r43: proper(dbl(X)) -> dbl(proper(X))
r44: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r45: proper(nil()) -> ok(nil())
r46: proper(half(X)) -> half(proper(X))
r47: terms(ok(X)) -> ok(terms(X))
r48: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r49: recip(ok(X)) -> ok(recip(X))
r50: sqr(ok(X)) -> ok(sqr(X))
r51: s(ok(X)) -> ok(s(X))
r52: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r53: dbl(ok(X)) -> ok(dbl(X))
r54: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r55: half(ok(X)) -> ok(half(X))
r56: top(mark(X)) -> top(proper(X))
r57: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      mark > first#
    
    argument filter:
  
      pi(first#) = [1, 2]
      pi(mark) = [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, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57

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

-- Reduction pair.

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

p1: half#(mark(X)) -> half#(X)
p2: half#(ok(X)) -> half#(X)

and R consists of:

r1: active(terms(N)) -> mark(cons(recip(sqr(N)),terms(s(N))))
r2: active(sqr(|0|())) -> mark(|0|())
r3: active(sqr(s(X))) -> mark(s(add(sqr(X),dbl(X))))
r4: active(dbl(|0|())) -> mark(|0|())
r5: active(dbl(s(X))) -> mark(s(s(dbl(X))))
r6: active(add(|0|(),X)) -> mark(X)
r7: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r8: active(first(|0|(),X)) -> mark(nil())
r9: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r10: active(half(|0|())) -> mark(|0|())
r11: active(half(s(|0|()))) -> mark(|0|())
r12: active(half(s(s(X)))) -> mark(s(half(X)))
r13: active(half(dbl(X))) -> mark(X)
r14: active(terms(X)) -> terms(active(X))
r15: active(cons(X1,X2)) -> cons(active(X1),X2)
r16: active(recip(X)) -> recip(active(X))
r17: active(sqr(X)) -> sqr(active(X))
r18: active(s(X)) -> s(active(X))
r19: active(add(X1,X2)) -> add(active(X1),X2)
r20: active(add(X1,X2)) -> add(X1,active(X2))
r21: active(dbl(X)) -> dbl(active(X))
r22: active(first(X1,X2)) -> first(active(X1),X2)
r23: active(first(X1,X2)) -> first(X1,active(X2))
r24: active(half(X)) -> half(active(X))
r25: terms(mark(X)) -> mark(terms(X))
r26: cons(mark(X1),X2) -> mark(cons(X1,X2))
r27: recip(mark(X)) -> mark(recip(X))
r28: sqr(mark(X)) -> mark(sqr(X))
r29: s(mark(X)) -> mark(s(X))
r30: add(mark(X1),X2) -> mark(add(X1,X2))
r31: add(X1,mark(X2)) -> mark(add(X1,X2))
r32: dbl(mark(X)) -> mark(dbl(X))
r33: first(mark(X1),X2) -> mark(first(X1,X2))
r34: first(X1,mark(X2)) -> mark(first(X1,X2))
r35: half(mark(X)) -> mark(half(X))
r36: proper(terms(X)) -> terms(proper(X))
r37: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r38: proper(recip(X)) -> recip(proper(X))
r39: proper(sqr(X)) -> sqr(proper(X))
r40: proper(s(X)) -> s(proper(X))
r41: proper(|0|()) -> ok(|0|())
r42: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r43: proper(dbl(X)) -> dbl(proper(X))
r44: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r45: proper(nil()) -> ok(nil())
r46: proper(half(X)) -> half(proper(X))
r47: terms(ok(X)) -> ok(terms(X))
r48: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r49: recip(ok(X)) -> ok(recip(X))
r50: sqr(ok(X)) -> ok(sqr(X))
r51: s(ok(X)) -> ok(s(X))
r52: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r53: dbl(ok(X)) -> ok(dbl(X))
r54: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r55: half(ok(X)) -> ok(half(X))
r56: top(mark(X)) -> top(proper(X))
r57: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57

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