YES

We show the termination of the TRS R:

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

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: top#(ok(X)) -> top#(active(X))
p2: top#(mark(X)) -> top#(proper(X))

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          top#_A(x1) = x1
          ok_A(x1) = x1
          active_A(x1) = x1
          mark_A(x1) = x1 + 2
          proper_A(x1) = x1
          terms_A(x1) = x1 + 12
          cons_A(x1,x2) = x1 + 5
          recip_A(x1) = x1 + 1
          sqr_A(x1) = x1 + 3
          add_A(x1,x2) = x1 + x2 + 5
          dbl_A(x1) = x1 + 5
          first_A(x1,x2) = x1 + x2 + 6
          s_A(x1) = 4
          |0|_A() = 3
          nil_A() = 6
  
    precedence:
    
      top# > ok = active = mark = terms = cons = recip = sqr = add = dbl = first = s = |0| = nil > proper
    
    partial status:
  
      pi(top#) = [1]
      pi(ok) = []
      pi(active) = []
      pi(mark) = []
      pi(proper) = [1]
      pi(terms) = []
      pi(cons) = []
      pi(recip) = []
      pi(sqr) = []
      pi(add) = []
      pi(dbl) = []
      pi(first) = []
      pi(s) = []
      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(add(X1,X2)) -> add(active(X1),X2)
r15: active(add(X1,X2)) -> add(X1,active(X2))
r16: active(dbl(X)) -> dbl(active(X))
r17: active(first(X1,X2)) -> first(active(X1),X2)
r18: active(first(X1,X2)) -> first(X1,active(X2))
r19: terms(mark(X)) -> mark(terms(X))
r20: cons(mark(X1),X2) -> mark(cons(X1,X2))
r21: recip(mark(X)) -> mark(recip(X))
r22: sqr(mark(X)) -> mark(sqr(X))
r23: add(mark(X1),X2) -> mark(add(X1,X2))
r24: add(X1,mark(X2)) -> mark(add(X1,X2))
r25: dbl(mark(X)) -> mark(dbl(X))
r26: first(mark(X1),X2) -> mark(first(X1,X2))
r27: first(X1,mark(X2)) -> mark(first(X1,X2))
r28: proper(terms(X)) -> terms(proper(X))
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(recip(X)) -> recip(proper(X))
r31: proper(sqr(X)) -> sqr(proper(X))
r32: proper(s(X)) -> s(proper(X))
r33: proper(|0|()) -> ok(|0|())
r34: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r35: proper(dbl(X)) -> dbl(proper(X))
r36: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r37: proper(nil()) -> ok(nil())
r38: terms(ok(X)) -> ok(terms(X))
r39: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r40: recip(ok(X)) -> ok(recip(X))
r41: sqr(ok(X)) -> ok(sqr(X))
r42: s(ok(X)) -> ok(s(X))
r43: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r44: dbl(ok(X)) -> ok(dbl(X))
r45: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r46: top(mark(X)) -> top(proper(X))
r47: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: top#(ok(X)) -> top#(active(X))

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r38, r39, r40, r41, r42, r43, r44, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          top#_A(x1) = x1 + 1
          ok_A(x1) = x1 + 6
          active_A(x1) = x1
          terms_A(x1) = x1 + 5
          mark_A(x1) = 0
          cons_A(x1,x2) = x1 + 3
          recip_A(x1) = x1 + 1
          sqr_A(x1) = x1
          add_A(x1,x2) = x1
          dbl_A(x1) = x1 + 1
          first_A(x1,x2) = x1 + x2 + 7
          s_A(x1) = x1 + 2
          |0|_A() = 1
          nil_A() = 7
  
    precedence:
    
      terms = cons > ok = recip = dbl = s > top# = active = sqr > first > add > mark = |0| = nil
    
    partial status:
  
      pi(top#) = [1]
      pi(ok) = []
      pi(active) = [1]
      pi(terms) = []
      pi(mark) = []
      pi(cons) = []
      pi(recip) = []
      pi(sqr) = [1]
      pi(add) = [1]
      pi(dbl) = []
      pi(first) = []
      pi(s) = []
      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#(sqr(X)) -> active#(X)
p7: active#(recip(X)) -> active#(X)
p8: active#(cons(X1,X2)) -> active#(X1)
p9: active#(terms(X)) -> active#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          active#_A(x1) = x1
          first_A(x1,x2) = x1 + x2 + 1
          dbl_A(x1) = x1 + 1
          add_A(x1,x2) = x1 + x2 + 1
          sqr_A(x1) = x1 + 1
          recip_A(x1) = x1 + 1
          cons_A(x1,x2) = x1 + x2 + 1
          terms_A(x1) = x1 + 1
  
    precedence:
    
      active# = first = dbl = add = sqr = recip = cons = terms
    
    partial status:
  
      pi(active#) = [1]
      pi(first) = [1, 2]
      pi(dbl) = [1]
      pi(add) = [1, 2]
      pi(sqr) = [1]
      pi(recip) = [1]
      pi(cons) = [1, 2]
      pi(terms) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: active#(first(X1,X2)) -> active#(X1)
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#(add(X1,X2)) -> active#(X1)
p7: active#(add(X1,X2)) -> active#(X2)
p8: active#(dbl(X)) -> active#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          active#_A(x1) = x1
          first_A(x1,x2) = x1 + x2 + 1
          terms_A(x1) = x1 + 1
          cons_A(x1,x2) = x1 + x2 + 1
          recip_A(x1) = x1 + 1
          sqr_A(x1) = x1 + 1
          add_A(x1,x2) = x1 + x2 + 1
          dbl_A(x1) = x1 + 1
  
    precedence:
    
      active# = first = terms = cons = sqr = add > recip = dbl
    
    partial status:
  
      pi(active#) = [1]
      pi(first) = [1, 2]
      pi(terms) = [1]
      pi(cons) = [1, 2]
      pi(recip) = [1]
      pi(sqr) = [1]
      pi(add) = [1, 2]
      pi(dbl) = []

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(terms(X)) -> active#(X)
p2: active#(cons(X1,X2)) -> active#(X1)
p3: active#(recip(X)) -> active#(X)
p4: active#(sqr(X)) -> active#(X)
p5: active#(add(X1,X2)) -> active#(X1)
p6: active#(add(X1,X2)) -> active#(X2)
p7: active#(dbl(X)) -> active#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          active#_A(x1) = x1
          terms_A(x1) = x1 + 1
          dbl_A(x1) = x1 + 1
          add_A(x1,x2) = x1 + x2 + 1
          sqr_A(x1) = x1 + 1
          recip_A(x1) = x1 + 1
          cons_A(x1,x2) = x1 + x2 + 1
  
    precedence:
    
      active# = terms = dbl = add = sqr = recip = cons
    
    partial status:
  
      pi(active#) = []
      pi(terms) = [1]
      pi(dbl) = [1]
      pi(add) = [2]
      pi(sqr) = [1]
      pi(recip) = [1]
      pi(cons) = [2]

The next rules are strictly ordered:

  p1

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

The estimated dependency graph contains the following SCCs:

  {p1, 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#(cons(X1,X2)) -> active#(X1)
p3: active#(recip(X)) -> active#(X)
p4: active#(sqr(X)) -> active#(X)
p5: active#(add(X1,X2)) -> active#(X1)
p6: active#(add(X1,X2)) -> active#(X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          active#_A(x1) = x1
          dbl_A(x1) = x1 + 1
          cons_A(x1,x2) = x1 + 1
          recip_A(x1) = x1 + 1
          sqr_A(x1) = x1 + 1
          add_A(x1,x2) = x1 + x2 + 1
  
    precedence:
    
      add > dbl > active# = cons = sqr > recip
    
    partial status:
  
      pi(active#) = [1]
      pi(dbl) = [1]
      pi(cons) = []
      pi(recip) = []
      pi(sqr) = [1]
      pi(add) = [1, 2]

The next rules are strictly ordered:

  p6

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

The estimated dependency graph contains the following SCCs:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          active#_A(x1) = x1
          dbl_A(x1) = x1 + 1
          add_A(x1,x2) = x1 + x2 + 1
          sqr_A(x1) = x1 + 1
          recip_A(x1) = x1 + 1
          cons_A(x1,x2) = x1 + x2 + 1
  
    precedence:
    
      active# = dbl = add = sqr = recip = cons
    
    partial status:
  
      pi(active#) = []
      pi(dbl) = [1]
      pi(add) = [2]
      pi(sqr) = [1]
      pi(recip) = [1]
      pi(cons) = [2]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4}


-- Reduction pair.

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

p1: active#(add(X1,X2)) -> active#(X1)
p2: active#(cons(X1,X2)) -> active#(X1)
p3: active#(recip(X)) -> active#(X)
p4: active#(sqr(X)) -> active#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          active#_A(x1) = x1
          add_A(x1,x2) = x1 + x2 + 1
          cons_A(x1,x2) = x1 + x2 + 1
          recip_A(x1) = x1 + 1
          sqr_A(x1) = x1 + 1
  
    precedence:
    
      active# = cons = recip > add = sqr
    
    partial status:
  
      pi(active#) = [1]
      pi(add) = [1, 2]
      pi(cons) = [1, 2]
      pi(recip) = [1]
      pi(sqr) = []

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: active#(add(X1,X2)) -> active#(X1)
p2: active#(recip(X)) -> active#(X)
p3: active#(sqr(X)) -> active#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          active#_A(x1) = x1
          add_A(x1,x2) = x1 + x2 + 1
          sqr_A(x1) = x1 + 1
          recip_A(x1) = x1 + 1
  
    precedence:
    
      active# = add = sqr = recip
    
    partial status:
  
      pi(active#) = [1]
      pi(add) = [1, 2]
      pi(sqr) = [1]
      pi(recip) = [1]

The next rules are strictly ordered:

  p1

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

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          active#_A(x1) = x1
          sqr_A(x1) = x1 + 1
          recip_A(x1) = x1 + 1
  
    precedence:
    
      active# = sqr = recip
    
    partial status:
  
      pi(active#) = [1]
      pi(sqr) = [1]
      pi(recip) = [1]

The next rules are strictly ordered:

  p1

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          proper#_A(x1) = x1
          first_A(x1,x2) = x1 + x2 + 1
          dbl_A(x1) = x1 + 1
          add_A(x1,x2) = x1 + x2 + 1
          s_A(x1) = x1 + 1
          sqr_A(x1) = x1 + 1
          recip_A(x1) = x1 + 1
          cons_A(x1,x2) = x1 + x2 + 1
          terms_A(x1) = x1 + 1
  
    precedence:
    
      proper# = dbl = add = s = sqr = recip = cons > first = terms
    
    partial status:
  
      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) = []

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          proper#_A(x1) = x1
          first_A(x1,x2) = x1 + x2 + 1
          terms_A(x1) = x1 + 1
          cons_A(x1,x2) = x1 + x2 + 1
          recip_A(x1) = x1 + 1
          sqr_A(x1) = x1 + 1
          s_A(x1) = x1 + 1
          add_A(x1,x2) = x1 + x2 + 1
          dbl_A(x1) = x1 + 1
  
    precedence:
    
      proper# = first = terms = cons = recip = sqr = s = add = dbl
    
    partial status:
  
      pi(proper#) = []
      pi(first) = [2]
      pi(terms) = [1]
      pi(cons) = [2]
      pi(recip) = [1]
      pi(sqr) = [1]
      pi(s) = [1]
      pi(add) = [2]
      pi(dbl) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          proper#_A(x1) = x1
          terms_A(x1) = x1 + 1
          dbl_A(x1) = x1 + 1
          add_A(x1,x2) = x1 + x2 + 1
          s_A(x1) = x1 + 1
          sqr_A(x1) = x1 + 1
          recip_A(x1) = x1 + 1
          cons_A(x1,x2) = x1 + x2 + 1
  
    precedence:
    
      proper# = terms = dbl = add = s = sqr = recip = cons
    
    partial status:
  
      pi(proper#) = [1]
      pi(terms) = [1]
      pi(dbl) = [1]
      pi(add) = [1, 2]
      pi(s) = [1]
      pi(sqr) = [1]
      pi(recip) = [1]
      pi(cons) = [1, 2]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: proper#(dbl(X)) -> proper#(X)
p2: proper#(cons(X1,X2)) -> proper#(X1)
p3: proper#(cons(X1,X2)) -> proper#(X2)
p4: proper#(recip(X)) -> proper#(X)
p5: proper#(sqr(X)) -> proper#(X)
p6: proper#(s(X)) -> proper#(X)
p7: proper#(add(X1,X2)) -> proper#(X1)
p8: proper#(add(X1,X2)) -> proper#(X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          proper#_A(x1) = x1
          dbl_A(x1) = x1 + 1
          cons_A(x1,x2) = x1 + x2 + 1
          recip_A(x1) = x1 + 1
          sqr_A(x1) = x1 + 1
          s_A(x1) = x1 + 1
          add_A(x1,x2) = x1 + x2 + 1
  
    precedence:
    
      proper# = dbl = cons = recip = sqr = s = add
    
    partial status:
  
      pi(proper#) = []
      pi(dbl) = [1]
      pi(cons) = [2]
      pi(recip) = [1]
      pi(sqr) = [1]
      pi(s) = [1]
      pi(add) = [2]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: proper#(cons(X1,X2)) -> proper#(X1)
p2: proper#(cons(X1,X2)) -> proper#(X2)
p3: proper#(recip(X)) -> proper#(X)
p4: proper#(sqr(X)) -> proper#(X)
p5: proper#(s(X)) -> proper#(X)
p6: proper#(add(X1,X2)) -> proper#(X1)
p7: proper#(add(X1,X2)) -> proper#(X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: proper#(cons(X1,X2)) -> proper#(X1)
p2: proper#(add(X1,X2)) -> proper#(X2)
p3: proper#(add(X1,X2)) -> proper#(X1)
p4: proper#(s(X)) -> proper#(X)
p5: proper#(sqr(X)) -> proper#(X)
p6: proper#(recip(X)) -> proper#(X)
p7: proper#(cons(X1,X2)) -> proper#(X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          proper#_A(x1) = x1
          cons_A(x1,x2) = x1 + x2 + 1
          add_A(x1,x2) = x1 + x2 + 1
          s_A(x1) = x1 + 1
          sqr_A(x1) = x1 + 1
          recip_A(x1) = x1 + 1
  
    precedence:
    
      proper# = cons = add = s = sqr > recip
    
    partial status:
  
      pi(proper#) = []
      pi(cons) = [2]
      pi(add) = [2]
      pi(s) = [1]
      pi(sqr) = []
      pi(recip) = []

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: proper#(add(X1,X2)) -> proper#(X2)
p2: proper#(add(X1,X2)) -> proper#(X1)
p3: proper#(s(X)) -> proper#(X)
p4: proper#(sqr(X)) -> proper#(X)
p5: proper#(recip(X)) -> proper#(X)
p6: proper#(cons(X1,X2)) -> proper#(X2)

and R consists of:

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

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          proper#_A(x1) = x1 + 1
          add_A(x1,x2) = x1 + x2 + 2
          cons_A(x1,x2) = x1 + x2 + 2
          recip_A(x1) = x1 + 2
          sqr_A(x1) = x1 + 2
          s_A(x1) = x1 + 2
  
    precedence:
    
      proper# = add = cons = recip = sqr = s
    
    partial status:
  
      pi(proper#) = [1]
      pi(add) = [1, 2]
      pi(cons) = [2]
      pi(recip) = [1]
      pi(sqr) = [1]
      pi(s) = [1]

The next rules are strictly ordered:

  p6

We remove them from the problem.

-- SCC decomposition.

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

p1: proper#(add(X1,X2)) -> proper#(X2)
p2: proper#(cons(X1,X2)) -> proper#(X2)
p3: proper#(recip(X)) -> proper#(X)
p4: proper#(sqr(X)) -> proper#(X)
p5: proper#(s(X)) -> proper#(X)

and R consists of:

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

The 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: proper#(add(X1,X2)) -> proper#(X2)
p2: proper#(s(X)) -> proper#(X)
p3: proper#(sqr(X)) -> proper#(X)
p4: proper#(recip(X)) -> proper#(X)
p5: proper#(cons(X1,X2)) -> proper#(X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          proper#_A(x1) = x1
          add_A(x1,x2) = x1 + x2 + 1
          s_A(x1) = x1 + 1
          sqr_A(x1) = x1 + 1
          recip_A(x1) = x1 + 1
          cons_A(x1,x2) = x1 + x2 + 1
  
    precedence:
    
      proper# = add = s = sqr = recip = cons
    
    partial status:
  
      pi(proper#) = []
      pi(add) = [2]
      pi(s) = [1]
      pi(sqr) = [1]
      pi(recip) = [1]
      pi(cons) = [2]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: proper#(s(X)) -> proper#(X)
p2: proper#(sqr(X)) -> proper#(X)
p3: proper#(recip(X)) -> proper#(X)
p4: proper#(cons(X1,X2)) -> proper#(X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4}


-- Reduction pair.

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

p1: proper#(s(X)) -> proper#(X)
p2: proper#(cons(X1,X2)) -> proper#(X2)
p3: proper#(recip(X)) -> proper#(X)
p4: proper#(sqr(X)) -> proper#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          proper#_A(x1) = x1
          s_A(x1) = x1 + 1
          cons_A(x1,x2) = x1 + x2 + 1
          recip_A(x1) = x1 + 1
          sqr_A(x1) = x1 + 1
  
    precedence:
    
      proper# = s = cons = recip = sqr
    
    partial status:
  
      pi(proper#) = [1]
      pi(s) = [1]
      pi(cons) = [2]
      pi(recip) = [1]
      pi(sqr) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: proper#(cons(X1,X2)) -> proper#(X2)
p2: proper#(recip(X)) -> proper#(X)
p3: proper#(sqr(X)) -> proper#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

p1: proper#(cons(X1,X2)) -> proper#(X2)
p2: proper#(sqr(X)) -> proper#(X)
p3: proper#(recip(X)) -> proper#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          proper#_A(x1) = x1
          cons_A(x1,x2) = x1 + x2 + 1
          sqr_A(x1) = x1 + 1
          recip_A(x1) = x1 + 1
  
    precedence:
    
      proper# = cons = sqr = recip
    
    partial status:
  
      pi(proper#) = [1]
      pi(cons) = [2]
      pi(sqr) = [1]
      pi(recip) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: proper#(sqr(X)) -> proper#(X)
p2: proper#(recip(X)) -> proper#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

p1: proper#(sqr(X)) -> proper#(X)
p2: proper#(recip(X)) -> proper#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          proper#_A(x1) = x1
          sqr_A(x1) = x1 + 1
          recip_A(x1) = x1 + 1
  
    precedence:
    
      proper# = sqr = recip
    
    partial status:
  
      pi(proper#) = [1]
      pi(sqr) = [1]
      pi(recip) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: proper#(recip(X)) -> proper#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: proper#(recip(X)) -> proper#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          proper#_A(x1) = x1
          recip_A(x1) = x1 + 1
  
    precedence:
    
      proper# = recip
    
    partial status:
  
      pi(proper#) = [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: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(ok(X1),ok(X2)) -> cons#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          cons#_A(x1,x2) = x1 + x2 + 2
          mark_A(x1) = x1 + 1
          ok_A(x1) = x1 + 1
  
    precedence:
    
      cons# = mark = ok
    
    partial status:
  
      pi(cons#) = []
      pi(mark) = [1]
      pi(ok) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          recip#_A(x1) = x1
          mark_A(x1) = x1 + 1
          ok_A(x1) = x1 + 1
  
    precedence:
    
      recip# = mark = ok
    
    partial status:
  
      pi(recip#) = [1]
      pi(mark) = [1]
      pi(ok) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: recip#(ok(X)) -> recip#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: recip#(ok(X)) -> recip#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          recip#_A(x1) = x1
          ok_A(x1) = x1 + 1
  
    precedence:
    
      recip# = ok
    
    partial status:
  
      pi(recip#) = [1]
      pi(ok) = [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: sqr#(mark(X)) -> sqr#(X)
p2: sqr#(ok(X)) -> sqr#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          sqr#_A(x1) = x1
          mark_A(x1) = x1 + 1
          ok_A(x1) = x1 + 1
  
    precedence:
    
      sqr# = mark = ok
    
    partial status:
  
      pi(sqr#) = [1]
      pi(mark) = [1]
      pi(ok) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: sqr#(ok(X)) -> sqr#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: sqr#(ok(X)) -> sqr#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          sqr#_A(x1) = x1
          ok_A(x1) = x1 + 1
  
    precedence:
    
      sqr# = ok
    
    partial status:
  
      pi(sqr#) = [1]
      pi(ok) = [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: terms#(mark(X)) -> terms#(X)
p2: terms#(ok(X)) -> terms#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          terms#_A(x1) = x1
          mark_A(x1) = x1 + 1
          ok_A(x1) = x1 + 1
  
    precedence:
    
      terms# = mark = ok
    
    partial status:
  
      pi(terms#) = [1]
      pi(mark) = [1]
      pi(ok) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: terms#(ok(X)) -> terms#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: terms#(ok(X)) -> terms#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          terms#_A(x1) = x1
          ok_A(x1) = x1 + 1
  
    precedence:
    
      terms# = ok
    
    partial status:
  
      pi(terms#) = [1]
      pi(ok) = [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: s#(ok(X)) -> s#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          s#_A(x1) = x1
          ok_A(x1) = x1 + 1
  
    precedence:
    
      s# = ok
    
    partial status:
  
      pi(s#) = [1]
      pi(ok) = [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: add#(mark(X1),X2) -> add#(X1,X2)
p2: add#(ok(X1),ok(X2)) -> add#(X1,X2)
p3: add#(X1,mark(X2)) -> add#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          add#_A(x1,x2) = x2 + 2
          mark_A(x1) = x1 + 1
          ok_A(x1) = x1 + 3
  
    precedence:
    
      add# > mark = ok
    
    partial status:
  
      pi(add#) = [2]
      pi(mark) = [1]
      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: add#(mark(X1),X2) -> add#(X1,X2)
p2: add#(X1,mark(X2)) -> add#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          add#_A(x1,x2) = x1 + x2 + 2
          mark_A(x1) = x1 + 1
  
    precedence:
    
      add# = mark
    
    partial status:
  
      pi(add#) = []
      pi(mark) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          dbl#_A(x1) = x1
          mark_A(x1) = x1 + 1
          ok_A(x1) = x1 + 1
  
    precedence:
    
      dbl# = mark = ok
    
    partial status:
  
      pi(dbl#) = [1]
      pi(mark) = [1]
      pi(ok) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: dbl#(ok(X)) -> dbl#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: dbl#(ok(X)) -> dbl#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          dbl#_A(x1) = x1
          ok_A(x1) = x1 + 1
  
    precedence:
    
      dbl# = ok
    
    partial status:
  
      pi(dbl#) = [1]
      pi(ok) = [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: first#(mark(X1),X2) -> first#(X1,X2)
p2: first#(ok(X1),ok(X2)) -> first#(X1,X2)
p3: first#(X1,mark(X2)) -> first#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          first#_A(x1,x2) = x2 + 2
          mark_A(x1) = x1 + 1
          ok_A(x1) = x1 + 3
  
    precedence:
    
      first# > mark = ok
    
    partial status:
  
      pi(first#) = [2]
      pi(mark) = [1]
      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: first#(mark(X1),X2) -> first#(X1,X2)
p2: first#(X1,mark(X2)) -> first#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          first#_A(x1,x2) = x1 + x2 + 2
          mark_A(x1) = x1 + 1
  
    precedence:
    
      first# = mark
    
    partial status:
  
      pi(first#) = []
      pi(mark) = [1]

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^1
        order: lexicographic order
        interpretations:
          first#_A(x1,x2) = x2
          mark_A(x1) = x1 + 1
  
    precedence:
    
      first# = mark
    
    partial status:
  
      pi(first#) = []
      pi(mark) = [1]

The next rules are strictly ordered:

  p1

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