YES

We show the termination of the TRS R:

  dbl(|0|()) -> |0|()
  dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
  dbls(nil()) -> nil()
  dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
  sel(|0|(),cons(X,Y)) -> activate(X)
  sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
  indx(nil(),X) -> nil()
  indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
  from(X) -> cons(activate(X),n__from(n__s(activate(X))))
  dbl1(|0|()) -> |01|()
  dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
  sel1(|0|(),cons(X,Y)) -> activate(X)
  sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
  quote(|0|()) -> |01|()
  quote(s(X)) -> s1(quote(activate(X)))
  quote(dbl(X)) -> dbl1(X)
  quote(sel(X,Y)) -> sel1(X,Y)
  s(X) -> n__s(X)
  dbl(X) -> n__dbl(X)
  dbls(X) -> n__dbls(X)
  sel(X1,X2) -> n__sel(X1,X2)
  indx(X1,X2) -> n__indx(X1,X2)
  from(X) -> n__from(X)
  activate(n__s(X)) -> s(X)
  activate(n__dbl(X)) -> dbl(X)
  activate(n__dbls(X)) -> dbls(X)
  activate(n__sel(X1,X2)) -> sel(X1,X2)
  activate(n__indx(X1,X2)) -> indx(X1,X2)
  activate(n__from(X)) -> from(X)
  activate(X) -> X

-- SCC decomposition.

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

p1: dbl#(s(X)) -> s#(n__s(n__dbl(activate(X))))
p2: dbl#(s(X)) -> activate#(X)
p3: dbls#(cons(X,Y)) -> activate#(X)
p4: dbls#(cons(X,Y)) -> activate#(Y)
p5: sel#(|0|(),cons(X,Y)) -> activate#(X)
p6: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p7: sel#(s(X),cons(Y,Z)) -> activate#(X)
p8: sel#(s(X),cons(Y,Z)) -> activate#(Z)
p9: indx#(cons(X,Y),Z) -> activate#(X)
p10: indx#(cons(X,Y),Z) -> activate#(Z)
p11: indx#(cons(X,Y),Z) -> activate#(Y)
p12: from#(X) -> activate#(X)
p13: dbl1#(s(X)) -> dbl1#(activate(X))
p14: dbl1#(s(X)) -> activate#(X)
p15: sel1#(|0|(),cons(X,Y)) -> activate#(X)
p16: sel1#(s(X),cons(Y,Z)) -> sel1#(activate(X),activate(Z))
p17: sel1#(s(X),cons(Y,Z)) -> activate#(X)
p18: sel1#(s(X),cons(Y,Z)) -> activate#(Z)
p19: quote#(s(X)) -> quote#(activate(X))
p20: quote#(s(X)) -> activate#(X)
p21: quote#(dbl(X)) -> dbl1#(X)
p22: quote#(sel(X,Y)) -> sel1#(X,Y)
p23: activate#(n__s(X)) -> s#(X)
p24: activate#(n__dbl(X)) -> dbl#(X)
p25: activate#(n__dbls(X)) -> dbls#(X)
p26: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p27: activate#(n__indx(X1,X2)) -> indx#(X1,X2)
p28: activate#(n__from(X)) -> from#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p19}
  {p16}
  {p13}
  {p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p24, p25, p26, p27, p28}


-- Reduction pair.

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

p1: quote#(s(X)) -> quote#(activate(X))

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        quote#_A(x1) = x1
        s_A(x1) = x1
        activate_A(x1) = x1
        dbl_A(x1) = x1 + 2
        |0|_A = 2
        n__s_A(x1) = x1
        n__dbl_A(x1) = x1 + 2
        dbls_A(x1) = max{3, x1 + 2}
        nil_A = 4
        cons_A(x1,x2) = max{x1 - 1, x2}
        n__dbls_A(x1) = max{3, x1 + 2}
        sel_A(x1,x2) = max{x1 + 5, x2 + 2}
        indx_A(x1,x2) = max{x1 + 6, x2 + 5}
        n__sel_A(x1,x2) = max{x1 + 5, x2 + 2}
        n__indx_A(x1,x2) = max{x1 + 6, x2 + 5}
        from_A(x1) = max{1, x1 - 1}
        n__from_A(x1) = max{1, x1 - 1}
  
    precedence:
    
      sel = n__sel > dbl = n__dbl > |0| > from = n__from > dbls = n__dbls = indx = n__indx > s = n__s > activate = nil > quote# = cons
    
    partial status:
  
      pi(quote#) = [1]
      pi(s) = [1]
      pi(activate) = [1]
      pi(dbl) = [1]
      pi(|0|) = []
      pi(n__s) = [1]
      pi(n__dbl) = [1]
      pi(dbls) = []
      pi(nil) = []
      pi(cons) = []
      pi(n__dbls) = []
      pi(sel) = []
      pi(indx) = [1]
      pi(n__sel) = []
      pi(n__indx) = [1]
      pi(from) = []
      pi(n__from) = []

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: sel1#(s(X),cons(Y,Z)) -> sel1#(activate(X),activate(Z))

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        sel1#_A(x1,x2) = max{x1 + 8, x2 + 4}
        s_A(x1) = max{4, x1}
        cons_A(x1,x2) = max{11, x1 + 10, x2}
        activate_A(x1) = max{3, x1}
        dbl_A(x1) = x1 + 9
        |0|_A = 0
        n__s_A(x1) = max{4, x1}
        n__dbl_A(x1) = x1 + 9
        dbls_A(x1) = x1 + 23
        nil_A = 24
        n__dbls_A(x1) = x1 + 23
        sel_A(x1,x2) = max{26, x1 + 19, x2 + 15}
        indx_A(x1,x2) = max{x1 + 37, x2 + 25}
        n__sel_A(x1,x2) = max{26, x1 + 19, x2 + 15}
        n__indx_A(x1,x2) = max{x1 + 37, x2 + 25}
        from_A(x1) = max{18, x1 + 14}
        n__from_A(x1) = max{18, x1 + 14}
  
    precedence:
    
      sel1# = dbl = |0| = n__dbl = dbls = nil = n__dbls = sel = indx = n__sel = n__indx > s = n__s = from = n__from > cons > activate
    
    partial status:
  
      pi(sel1#) = [1]
      pi(s) = [1]
      pi(cons) = []
      pi(activate) = [1]
      pi(dbl) = [1]
      pi(|0|) = []
      pi(n__s) = [1]
      pi(n__dbl) = [1]
      pi(dbls) = [1]
      pi(nil) = []
      pi(n__dbls) = [1]
      pi(sel) = []
      pi(indx) = [1]
      pi(n__sel) = []
      pi(n__indx) = [1]
      pi(from) = []
      pi(n__from) = []

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: dbl1#(s(X)) -> dbl1#(activate(X))

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        dbl1#_A(x1) = x1 + 4
        s_A(x1) = max{2, x1}
        activate_A(x1) = x1
        dbl_A(x1) = max{5, x1 + 3}
        |0|_A = 6
        n__s_A(x1) = max{2, x1}
        n__dbl_A(x1) = max{5, x1 + 3}
        dbls_A(x1) = max{11, x1 + 6}
        nil_A = 12
        cons_A(x1,x2) = max{4, x1, x2}
        n__dbls_A(x1) = max{11, x1 + 6}
        sel_A(x1,x2) = max{10, x1 + 1, x2}
        indx_A(x1,x2) = max{x1 + 11, x2 + 15}
        n__sel_A(x1,x2) = max{10, x1 + 1, x2}
        n__indx_A(x1,x2) = max{x1 + 11, x2 + 15}
        from_A(x1) = max{8, x1 + 5}
        n__from_A(x1) = max{8, x1 + 5}
  
    precedence:
    
      sel = n__sel > dbl = n__dbl > s = n__s > dbl1# = activate = |0| = dbls = nil = indx = from > cons = n__dbls > n__from > n__indx
    
    partial status:
  
      pi(dbl1#) = [1]
      pi(s) = [1]
      pi(activate) = [1]
      pi(dbl) = [1]
      pi(|0|) = []
      pi(n__s) = [1]
      pi(n__dbl) = [1]
      pi(dbls) = []
      pi(nil) = []
      pi(cons) = [1, 2]
      pi(n__dbls) = [1]
      pi(sel) = [1, 2]
      pi(indx) = []
      pi(n__sel) = [1, 2]
      pi(n__indx) = []
      pi(from) = []
      pi(n__from) = []

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#(s(X)) -> activate#(X)
p2: activate#(n__from(X)) -> from#(X)
p3: from#(X) -> activate#(X)
p4: activate#(n__indx(X1,X2)) -> indx#(X1,X2)
p5: indx#(cons(X,Y),Z) -> activate#(Y)
p6: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p7: sel#(s(X),cons(Y,Z)) -> activate#(Z)
p8: activate#(n__dbls(X)) -> dbls#(X)
p9: dbls#(cons(X,Y)) -> activate#(Y)
p10: activate#(n__dbl(X)) -> dbl#(X)
p11: dbls#(cons(X,Y)) -> activate#(X)
p12: sel#(s(X),cons(Y,Z)) -> activate#(X)
p13: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p14: sel#(|0|(),cons(X,Y)) -> activate#(X)
p15: indx#(cons(X,Y),Z) -> activate#(Z)
p16: indx#(cons(X,Y),Z) -> activate#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        dbl#_A(x1) = x1 + 1
        s_A(x1) = max{6, x1}
        activate#_A(x1) = x1
        n__from_A(x1) = x1
        from#_A(x1) = x1
        n__indx_A(x1,x2) = max{33, x1 + 27, x2 + 5}
        indx#_A(x1,x2) = max{x1 + 6, x2 + 1}
        cons_A(x1,x2) = max{6, x1 - 5, x2}
        n__sel_A(x1,x2) = max{x1 + 15, x2 + 10}
        sel#_A(x1,x2) = max{x1 + 14, x2 + 7}
        n__dbls_A(x1) = x1 + 20
        dbls#_A(x1) = x1 + 20
        n__dbl_A(x1) = x1 + 13
        activate_A(x1) = max{6, x1}
        |0|_A = 0
        dbl_A(x1) = x1 + 13
        n__s_A(x1) = max{6, x1}
        dbls_A(x1) = x1 + 20
        nil_A = 0
        sel_A(x1,x2) = max{x1 + 15, x2 + 10}
        indx_A(x1,x2) = max{33, x1 + 27, x2 + 5}
        from_A(x1) = max{6, x1}
  
    precedence:
    
      nil > n__dbl = dbl > s = n__s > activate = |0| = dbls = sel = indx > n__dbls > from > cons > n__indx > dbl# = activate# = n__from = from# = indx# = n__sel = sel# = dbls#
    
    partial status:
  
      pi(dbl#) = []
      pi(s) = [1]
      pi(activate#) = []
      pi(n__from) = []
      pi(from#) = []
      pi(n__indx) = [1]
      pi(indx#) = []
      pi(cons) = [2]
      pi(n__sel) = [1]
      pi(sel#) = []
      pi(n__dbls) = []
      pi(dbls#) = []
      pi(n__dbl) = [1]
      pi(activate) = [1]
      pi(|0|) = []
      pi(dbl) = [1]
      pi(n__s) = [1]
      pi(dbls) = [1]
      pi(nil) = []
      pi(sel) = []
      pi(indx) = []
      pi(from) = []

The next rules are strictly ordered:

  p7

We remove them from the problem.

-- SCC decomposition.

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

p1: dbl#(s(X)) -> activate#(X)
p2: activate#(n__from(X)) -> from#(X)
p3: from#(X) -> activate#(X)
p4: activate#(n__indx(X1,X2)) -> indx#(X1,X2)
p5: indx#(cons(X,Y),Z) -> activate#(Y)
p6: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p7: activate#(n__dbls(X)) -> dbls#(X)
p8: dbls#(cons(X,Y)) -> activate#(Y)
p9: activate#(n__dbl(X)) -> dbl#(X)
p10: dbls#(cons(X,Y)) -> activate#(X)
p11: sel#(s(X),cons(Y,Z)) -> activate#(X)
p12: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p13: sel#(|0|(),cons(X,Y)) -> activate#(X)
p14: indx#(cons(X,Y),Z) -> activate#(Z)
p15: indx#(cons(X,Y),Z) -> activate#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15}


-- Reduction pair.

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

p1: dbl#(s(X)) -> activate#(X)
p2: activate#(n__dbl(X)) -> dbl#(X)
p3: activate#(n__dbls(X)) -> dbls#(X)
p4: dbls#(cons(X,Y)) -> activate#(X)
p5: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p6: sel#(|0|(),cons(X,Y)) -> activate#(X)
p7: activate#(n__indx(X1,X2)) -> indx#(X1,X2)
p8: indx#(cons(X,Y),Z) -> activate#(X)
p9: activate#(n__from(X)) -> from#(X)
p10: from#(X) -> activate#(X)
p11: indx#(cons(X,Y),Z) -> activate#(Z)
p12: indx#(cons(X,Y),Z) -> activate#(Y)
p13: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p14: sel#(s(X),cons(Y,Z)) -> activate#(X)
p15: dbls#(cons(X,Y)) -> activate#(Y)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        dbl#_A(x1) = x1
        s_A(x1) = max{6, x1}
        activate#_A(x1) = max{6, x1}
        n__dbl_A(x1) = x1
        n__dbls_A(x1) = max{10, x1 + 7}
        dbls#_A(x1) = x1 + 6
        cons_A(x1,x2) = max{x1, x2}
        n__sel_A(x1,x2) = max{x1 + 9, x2 + 12}
        sel#_A(x1,x2) = max{x1 + 7, x2 + 11}
        |0|_A = 1
        n__indx_A(x1,x2) = max{18, x1 + 12, x2 + 15}
        indx#_A(x1,x2) = max{x1 + 6, x2 + 6}
        n__from_A(x1) = max{14, x1 + 8}
        from#_A(x1) = x1 + 7
        activate_A(x1) = max{2, x1}
        dbl_A(x1) = x1
        n__s_A(x1) = max{6, x1}
        dbls_A(x1) = max{10, x1 + 7}
        nil_A = 14
        sel_A(x1,x2) = max{x1 + 9, x2 + 12}
        indx_A(x1,x2) = max{18, x1 + 12, x2 + 15}
        from_A(x1) = max{14, x1 + 8}
  
    precedence:
    
      |0| = n__indx = indx > n__from = from > n__dbls = dbls > n__dbl = cons = dbl > s = n__s > nil > activate = sel > dbls# = indx# > dbl# = activate# > sel# > from# > n__sel
    
    partial status:
  
      pi(dbl#) = [1]
      pi(s) = [1]
      pi(activate#) = [1]
      pi(n__dbl) = [1]
      pi(n__dbls) = [1]
      pi(dbls#) = []
      pi(cons) = [1]
      pi(n__sel) = [1]
      pi(sel#) = [1]
      pi(|0|) = []
      pi(n__indx) = [2]
      pi(indx#) = []
      pi(n__from) = [1]
      pi(from#) = [1]
      pi(activate) = [1]
      pi(dbl) = [1]
      pi(n__s) = [1]
      pi(dbls) = [1]
      pi(nil) = []
      pi(sel) = [1, 2]
      pi(indx) = [2]
      pi(from) = [1]

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

p1: dbl#(s(X)) -> activate#(X)
p2: activate#(n__dbl(X)) -> dbl#(X)
p3: activate#(n__dbls(X)) -> dbls#(X)
p4: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p5: sel#(|0|(),cons(X,Y)) -> activate#(X)
p6: activate#(n__indx(X1,X2)) -> indx#(X1,X2)
p7: indx#(cons(X,Y),Z) -> activate#(X)
p8: activate#(n__from(X)) -> from#(X)
p9: from#(X) -> activate#(X)
p10: indx#(cons(X,Y),Z) -> activate#(Z)
p11: indx#(cons(X,Y),Z) -> activate#(Y)
p12: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p13: sel#(s(X),cons(Y,Z)) -> activate#(X)
p14: dbls#(cons(X,Y)) -> activate#(Y)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14}


-- Reduction pair.

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

p1: dbl#(s(X)) -> activate#(X)
p2: activate#(n__from(X)) -> from#(X)
p3: from#(X) -> activate#(X)
p4: activate#(n__indx(X1,X2)) -> indx#(X1,X2)
p5: indx#(cons(X,Y),Z) -> activate#(Y)
p6: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p7: sel#(s(X),cons(Y,Z)) -> activate#(X)
p8: activate#(n__dbls(X)) -> dbls#(X)
p9: dbls#(cons(X,Y)) -> activate#(Y)
p10: activate#(n__dbl(X)) -> dbl#(X)
p11: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p12: sel#(|0|(),cons(X,Y)) -> activate#(X)
p13: indx#(cons(X,Y),Z) -> activate#(Z)
p14: indx#(cons(X,Y),Z) -> activate#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        dbl#_A(x1) = max{2, x1 + 1}
        s_A(x1) = x1
        activate#_A(x1) = max{1, x1}
        n__from_A(x1) = x1 + 6
        from#_A(x1) = x1 + 2
        n__indx_A(x1,x2) = max{x1 + 17, x2 + 14}
        indx#_A(x1,x2) = max{13, x1 + 2, x2 + 2}
        cons_A(x1,x2) = max{x1 + 6, x2}
        n__sel_A(x1,x2) = max{x1 + 17, x2 + 4}
        sel#_A(x1,x2) = max{x1 + 3, x2 + 4}
        n__dbls_A(x1) = x1 + 13
        dbls#_A(x1) = max{4, x1 + 2}
        n__dbl_A(x1) = x1 + 5
        activate_A(x1) = x1
        |0|_A = 0
        dbl_A(x1) = x1 + 5
        n__s_A(x1) = x1
        dbls_A(x1) = x1 + 13
        nil_A = 13
        sel_A(x1,x2) = max{x1 + 17, x2 + 4}
        indx_A(x1,x2) = max{x1 + 17, x2 + 14}
        from_A(x1) = x1 + 6
  
    precedence:
    
      n__dbl = dbl > s = n__s > indx# = dbls# > n__sel = sel > sel# > activate = indx = from > dbls > cons > activate# > dbl# = from# = n__dbls > n__indx > n__from = |0| > nil
    
    partial status:
  
      pi(dbl#) = [1]
      pi(s) = [1]
      pi(activate#) = [1]
      pi(n__from) = [1]
      pi(from#) = []
      pi(n__indx) = []
      pi(indx#) = []
      pi(cons) = [1, 2]
      pi(n__sel) = []
      pi(sel#) = [1]
      pi(n__dbls) = []
      pi(dbls#) = [1]
      pi(n__dbl) = [1]
      pi(activate) = [1]
      pi(|0|) = []
      pi(dbl) = [1]
      pi(n__s) = [1]
      pi(dbls) = []
      pi(nil) = []
      pi(sel) = []
      pi(indx) = []
      pi(from) = [1]

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

p1: dbl#(s(X)) -> activate#(X)
p2: activate#(n__from(X)) -> from#(X)
p3: from#(X) -> activate#(X)
p4: indx#(cons(X,Y),Z) -> activate#(Y)
p5: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p6: sel#(s(X),cons(Y,Z)) -> activate#(X)
p7: activate#(n__dbls(X)) -> dbls#(X)
p8: dbls#(cons(X,Y)) -> activate#(Y)
p9: activate#(n__dbl(X)) -> dbl#(X)
p10: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p11: sel#(|0|(),cons(X,Y)) -> activate#(X)
p12: indx#(cons(X,Y),Z) -> activate#(Z)
p13: indx#(cons(X,Y),Z) -> activate#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: dbl#(s(X)) -> activate#(X)
p2: activate#(n__dbl(X)) -> dbl#(X)
p3: activate#(n__dbls(X)) -> dbls#(X)
p4: dbls#(cons(X,Y)) -> activate#(Y)
p5: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p6: sel#(|0|(),cons(X,Y)) -> activate#(X)
p7: activate#(n__from(X)) -> from#(X)
p8: from#(X) -> activate#(X)
p9: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p10: sel#(s(X),cons(Y,Z)) -> activate#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        dbl#_A(x1) = x1 + 6
        s_A(x1) = x1
        activate#_A(x1) = max{4, x1 + 1}
        n__dbl_A(x1) = x1 + 5
        n__dbls_A(x1) = x1 + 22
        dbls#_A(x1) = x1 + 6
        cons_A(x1,x2) = max{3, x1 - 1, x2}
        n__sel_A(x1,x2) = max{20, x1 + 11, x2 + 13}
        sel#_A(x1,x2) = max{x1 + 10, x2 + 6}
        |0|_A = 0
        n__from_A(x1) = x1 + 5
        from#_A(x1) = x1 + 5
        activate_A(x1) = x1
        dbl_A(x1) = x1 + 5
        n__s_A(x1) = x1
        dbls_A(x1) = x1 + 22
        nil_A = 21
        sel_A(x1,x2) = max{20, x1 + 11, x2 + 13}
        indx_A(x1,x2) = max{20, x1 + 15, x2 + 14}
        n__indx_A(x1,x2) = max{20, x1 + 15, x2 + 14}
        from_A(x1) = x1 + 5
  
    precedence:
    
      n__sel = sel > cons = |0| = n__from = activate = dbl = dbls = nil = indx = n__indx = from > n__dbl > s = dbls# = n__s > n__dbls = sel# > from# > activate# > dbl#
    
    partial status:
  
      pi(dbl#) = [1]
      pi(s) = [1]
      pi(activate#) = [1]
      pi(n__dbl) = []
      pi(n__dbls) = [1]
      pi(dbls#) = [1]
      pi(cons) = []
      pi(n__sel) = []
      pi(sel#) = []
      pi(|0|) = []
      pi(n__from) = []
      pi(from#) = [1]
      pi(activate) = [1]
      pi(dbl) = []
      pi(n__s) = [1]
      pi(dbls) = [1]
      pi(nil) = []
      pi(sel) = []
      pi(indx) = []
      pi(n__indx) = []
      pi(from) = []

The next rules are strictly ordered:

  p7

We remove them from the problem.

-- SCC decomposition.

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

p1: dbl#(s(X)) -> activate#(X)
p2: activate#(n__dbl(X)) -> dbl#(X)
p3: activate#(n__dbls(X)) -> dbls#(X)
p4: dbls#(cons(X,Y)) -> activate#(Y)
p5: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p6: sel#(|0|(),cons(X,Y)) -> activate#(X)
p7: from#(X) -> activate#(X)
p8: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p9: sel#(s(X),cons(Y,Z)) -> activate#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: dbl#(s(X)) -> activate#(X)
p2: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p3: sel#(s(X),cons(Y,Z)) -> activate#(X)
p4: activate#(n__dbls(X)) -> dbls#(X)
p5: dbls#(cons(X,Y)) -> activate#(Y)
p6: activate#(n__dbl(X)) -> dbl#(X)
p7: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p8: sel#(|0|(),cons(X,Y)) -> activate#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        dbl#_A(x1) = max{3, x1 + 1}
        s_A(x1) = max{6, x1}
        activate#_A(x1) = max{2, x1 - 1}
        n__sel_A(x1,x2) = max{33, x1 + 13, x2 + 11}
        sel#_A(x1,x2) = max{12, x1 - 1, x2 + 10}
        cons_A(x1,x2) = max{x1 - 11, x2}
        n__dbls_A(x1) = max{17, x1 + 16}
        dbls#_A(x1) = x1 + 2
        n__dbl_A(x1) = max{10, x1 + 5}
        activate_A(x1) = x1
        |0|_A = 11
        dbl_A(x1) = max{10, x1 + 5}
        n__s_A(x1) = max{6, x1}
        dbls_A(x1) = max{17, x1 + 16}
        nil_A = 23
        sel_A(x1,x2) = max{33, x1 + 13, x2 + 11}
        indx_A(x1,x2) = max{25, x1 + 23, x2 + 24}
        n__indx_A(x1,x2) = max{25, x1 + 23, x2 + 24}
        from_A(x1) = max{0, x1 - 11}
        n__from_A(x1) = max{0, x1 - 11}
  
    precedence:
    
      s = n__sel = n__dbl = activate = |0| = dbl = dbls = nil = sel = from = n__from > dbls# > activate# = sel# = n__dbls = n__s > dbl# > cons = indx > n__indx
    
    partial status:
  
      pi(dbl#) = [1]
      pi(s) = []
      pi(activate#) = []
      pi(n__sel) = []
      pi(sel#) = []
      pi(cons) = []
      pi(n__dbls) = []
      pi(dbls#) = [1]
      pi(n__dbl) = []
      pi(activate) = []
      pi(|0|) = []
      pi(dbl) = []
      pi(n__s) = []
      pi(dbls) = []
      pi(nil) = []
      pi(sel) = []
      pi(indx) = [1]
      pi(n__indx) = [1, 2]
      pi(from) = []
      pi(n__from) = []

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

p1: dbl#(s(X)) -> activate#(X)
p2: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p3: sel#(s(X),cons(Y,Z)) -> activate#(X)
p4: dbls#(cons(X,Y)) -> activate#(Y)
p5: activate#(n__dbl(X)) -> dbl#(X)
p6: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p7: sel#(|0|(),cons(X,Y)) -> activate#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: dbl#(s(X)) -> activate#(X)
p2: activate#(n__dbl(X)) -> dbl#(X)
p3: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p4: sel#(|0|(),cons(X,Y)) -> activate#(X)
p5: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p6: sel#(s(X),cons(Y,Z)) -> activate#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        dbl#_A(x1) = max{2, x1 + 1}
        s_A(x1) = max{2, x1}
        activate#_A(x1) = x1
        n__dbl_A(x1) = x1 + 2
        n__sel_A(x1,x2) = max{10, x1 + 8, x2 + 7}
        sel#_A(x1,x2) = max{6, x1 + 1, x2 + 2}
        |0|_A = 0
        cons_A(x1,x2) = max{x1 + 4, x2}
        activate_A(x1) = x1
        dbl_A(x1) = x1 + 2
        n__s_A(x1) = max{2, x1}
        dbls_A(x1) = x1 + 2
        nil_A = 0
        n__dbls_A(x1) = x1 + 2
        sel_A(x1,x2) = max{10, x1 + 8, x2 + 7}
        indx_A(x1,x2) = max{x1 + 15, x2 + 19}
        n__indx_A(x1,x2) = max{x1 + 15, x2 + 19}
        from_A(x1) = max{7, x1 + 4}
        n__from_A(x1) = max{7, x1 + 4}
  
    precedence:
    
      dbls = n__dbls > nil > n__dbl = n__sel = dbl = sel = indx = n__indx > s = sel# = n__s > |0| = activate = from > cons > activate# > dbl# > n__from
    
    partial status:
  
      pi(dbl#) = [1]
      pi(s) = [1]
      pi(activate#) = [1]
      pi(n__dbl) = [1]
      pi(n__sel) = [1, 2]
      pi(sel#) = [1, 2]
      pi(|0|) = []
      pi(cons) = []
      pi(activate) = [1]
      pi(dbl) = [1]
      pi(n__s) = [1]
      pi(dbls) = []
      pi(nil) = []
      pi(n__dbls) = []
      pi(sel) = [1, 2]
      pi(indx) = [1]
      pi(n__indx) = [1]
      pi(from) = []
      pi(n__from) = [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: dbl#(s(X)) -> activate#(X)
p2: activate#(n__dbl(X)) -> dbl#(X)
p3: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p4: sel#(|0|(),cons(X,Y)) -> activate#(X)
p5: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> 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: dbl#(s(X)) -> activate#(X)
p2: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p3: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p4: sel#(|0|(),cons(X,Y)) -> activate#(X)
p5: activate#(n__dbl(X)) -> dbl#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        dbl#_A(x1) = x1 + 11
        s_A(x1) = max{9, x1}
        activate#_A(x1) = x1 + 11
        n__sel_A(x1,x2) = max{x1 + 16, x2 + 12}
        sel#_A(x1,x2) = max{x1 + 17, x2 + 22}
        cons_A(x1,x2) = max{1, x1 - 7, x2}
        activate_A(x1) = max{4, x1}
        |0|_A = 2
        n__dbl_A(x1) = x1
        dbl_A(x1) = max{3, x1}
        n__s_A(x1) = max{9, x1}
        dbls_A(x1) = max{4, x1}
        nil_A = 0
        n__dbls_A(x1) = x1
        sel_A(x1,x2) = max{x1 + 16, x2 + 12}
        indx_A(x1,x2) = max{37, x1 + 28, x2 + 33}
        n__indx_A(x1,x2) = max{37, x1 + 28, x2 + 33}
        from_A(x1) = max{3, x1 - 7}
        n__from_A(x1) = max{2, x1 - 7}
  
    precedence:
    
      dbl# = s = activate# = n__sel = sel# = activate = |0| = n__dbl = dbl = n__s = dbls = n__dbls = sel = from > nil = n__from > cons = indx = n__indx
    
    partial status:
  
      pi(dbl#) = []
      pi(s) = []
      pi(activate#) = []
      pi(n__sel) = []
      pi(sel#) = []
      pi(cons) = []
      pi(activate) = []
      pi(|0|) = []
      pi(n__dbl) = []
      pi(dbl) = []
      pi(n__s) = []
      pi(dbls) = []
      pi(nil) = []
      pi(n__dbls) = []
      pi(sel) = []
      pi(indx) = [2]
      pi(n__indx) = [2]
      pi(from) = []
      pi(n__from) = []

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

p1: dbl#(s(X)) -> activate#(X)
p2: activate#(n__sel(X1,X2)) -> sel#(X1,X2)
p3: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))
p4: activate#(n__dbl(X)) -> dbl#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p4}
  {p3}


-- Reduction pair.

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

p1: dbl#(s(X)) -> activate#(X)
p2: activate#(n__dbl(X)) -> dbl#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        dbl#_A(x1) = max{3, x1 + 2}
        s_A(x1) = x1
        activate#_A(x1) = x1 + 2
        n__dbl_A(x1) = x1 + 1
  
    precedence:
    
      dbl# = s = activate# = n__dbl
    
    partial status:
  
      pi(dbl#) = [1]
      pi(s) = [1]
      pi(activate#) = [1]
      pi(n__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: activate#(n__dbl(X)) -> dbl#(X)

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  (no SCCs)

-- Reduction pair.

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

p1: sel#(s(X),cons(Y,Z)) -> sel#(activate(X),activate(Z))

and R consists of:

r1: dbl(|0|()) -> |0|()
r2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
r3: dbls(nil()) -> nil()
r4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
r5: sel(|0|(),cons(X,Y)) -> activate(X)
r6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
r7: indx(nil(),X) -> nil()
r8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
r9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
r10: dbl1(|0|()) -> |01|()
r11: dbl1(s(X)) -> s1(s1(dbl1(activate(X))))
r12: sel1(|0|(),cons(X,Y)) -> activate(X)
r13: sel1(s(X),cons(Y,Z)) -> sel1(activate(X),activate(Z))
r14: quote(|0|()) -> |01|()
r15: quote(s(X)) -> s1(quote(activate(X)))
r16: quote(dbl(X)) -> dbl1(X)
r17: quote(sel(X,Y)) -> sel1(X,Y)
r18: s(X) -> n__s(X)
r19: dbl(X) -> n__dbl(X)
r20: dbls(X) -> n__dbls(X)
r21: sel(X1,X2) -> n__sel(X1,X2)
r22: indx(X1,X2) -> n__indx(X1,X2)
r23: from(X) -> n__from(X)
r24: activate(n__s(X)) -> s(X)
r25: activate(n__dbl(X)) -> dbl(X)
r26: activate(n__dbls(X)) -> dbls(X)
r27: activate(n__sel(X1,X2)) -> sel(X1,X2)
r28: activate(n__indx(X1,X2)) -> indx(X1,X2)
r29: activate(n__from(X)) -> from(X)
r30: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        sel#_A(x1,x2) = max{x1 + 8, x2 + 8}
        s_A(x1) = max{2, x1}
        cons_A(x1,x2) = max{13, x1 - 6, x2}
        activate_A(x1) = x1
        dbl_A(x1) = x1 + 5
        |0|_A = 0
        n__s_A(x1) = max{2, x1}
        n__dbl_A(x1) = x1 + 5
        dbls_A(x1) = max{14, x1 + 12}
        nil_A = 15
        n__dbls_A(x1) = max{14, x1 + 12}
        sel_A(x1,x2) = max{x1 + 10, x2 + 17}
        indx_A(x1,x2) = max{x1 + 25, x2 + 18}
        n__sel_A(x1,x2) = max{x1 + 10, x2 + 17}
        n__indx_A(x1,x2) = max{x1 + 25, x2 + 18}
        from_A(x1) = max{14, x1 - 1}
        n__from_A(x1) = max{14, x1 - 1}
  
    precedence:
    
      from = n__from > sel# = indx = n__indx > dbl = |0| = n__dbl > s = cons = n__s = dbls = nil = n__dbls > activate = sel = n__sel
    
    partial status:
  
      pi(sel#) = [1]
      pi(s) = [1]
      pi(cons) = []
      pi(activate) = [1]
      pi(dbl) = [1]
      pi(|0|) = []
      pi(n__s) = [1]
      pi(n__dbl) = [1]
      pi(dbls) = [1]
      pi(nil) = []
      pi(n__dbls) = [1]
      pi(sel) = []
      pi(indx) = []
      pi(n__sel) = []
      pi(n__indx) = []
      pi(from) = []
      pi(n__from) = []

The next rules are strictly ordered:

  p1

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