YES

We show the termination of the TRS R:

  active(and(true(),X)) -> mark(X)
  active(and(false(),Y)) -> mark(false())
  active(if(true(),X,Y)) -> mark(X)
  active(if(false(),X,Y)) -> mark(Y)
  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(from(X)) -> mark(cons(X,from(s(X))))
  mark(and(X1,X2)) -> active(and(mark(X1),X2))
  mark(true()) -> active(true())
  mark(false()) -> active(false())
  mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
  mark(add(X1,X2)) -> active(add(mark(X1),X2))
  mark(|0|()) -> active(|0|())
  mark(s(X)) -> active(s(X))
  mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
  mark(nil()) -> active(nil())
  mark(cons(X1,X2)) -> active(cons(X1,X2))
  mark(from(X)) -> active(from(X))
  and(mark(X1),X2) -> and(X1,X2)
  and(X1,mark(X2)) -> and(X1,X2)
  and(active(X1),X2) -> and(X1,X2)
  and(X1,active(X2)) -> and(X1,X2)
  if(mark(X1),X2,X3) -> if(X1,X2,X3)
  if(X1,mark(X2),X3) -> if(X1,X2,X3)
  if(X1,X2,mark(X3)) -> if(X1,X2,X3)
  if(active(X1),X2,X3) -> if(X1,X2,X3)
  if(X1,active(X2),X3) -> if(X1,X2,X3)
  if(X1,X2,active(X3)) -> if(X1,X2,X3)
  add(mark(X1),X2) -> add(X1,X2)
  add(X1,mark(X2)) -> add(X1,X2)
  add(active(X1),X2) -> add(X1,X2)
  add(X1,active(X2)) -> add(X1,X2)
  s(mark(X)) -> s(X)
  s(active(X)) -> s(X)
  first(mark(X1),X2) -> first(X1,X2)
  first(X1,mark(X2)) -> first(X1,X2)
  first(active(X1),X2) -> first(X1,X2)
  first(X1,active(X2)) -> first(X1,X2)
  cons(mark(X1),X2) -> cons(X1,X2)
  cons(X1,mark(X2)) -> cons(X1,X2)
  cons(active(X1),X2) -> cons(X1,X2)
  cons(X1,active(X2)) -> cons(X1,X2)
  from(mark(X)) -> from(X)
  from(active(X)) -> from(X)

-- SCC decomposition.

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

p1: active#(and(true(),X)) -> mark#(X)
p2: active#(and(false(),Y)) -> mark#(false())
p3: active#(if(true(),X,Y)) -> mark#(X)
p4: active#(if(false(),X,Y)) -> mark#(Y)
p5: active#(add(|0|(),X)) -> mark#(X)
p6: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p7: active#(add(s(X),Y)) -> s#(add(X,Y))
p8: active#(add(s(X),Y)) -> add#(X,Y)
p9: active#(first(|0|(),X)) -> mark#(nil())
p10: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p11: active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
p12: active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
p13: active#(from(X)) -> mark#(cons(X,from(s(X))))
p14: active#(from(X)) -> cons#(X,from(s(X)))
p15: active#(from(X)) -> from#(s(X))
p16: active#(from(X)) -> s#(X)
p17: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p18: mark#(and(X1,X2)) -> and#(mark(X1),X2)
p19: mark#(and(X1,X2)) -> mark#(X1)
p20: mark#(true()) -> active#(true())
p21: mark#(false()) -> active#(false())
p22: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p23: mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
p24: mark#(if(X1,X2,X3)) -> mark#(X1)
p25: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
p26: mark#(add(X1,X2)) -> add#(mark(X1),X2)
p27: mark#(add(X1,X2)) -> mark#(X1)
p28: mark#(|0|()) -> active#(|0|())
p29: mark#(s(X)) -> active#(s(X))
p30: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p31: mark#(first(X1,X2)) -> first#(mark(X1),mark(X2))
p32: mark#(first(X1,X2)) -> mark#(X1)
p33: mark#(first(X1,X2)) -> mark#(X2)
p34: mark#(nil()) -> active#(nil())
p35: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p36: mark#(from(X)) -> active#(from(X))
p37: and#(mark(X1),X2) -> and#(X1,X2)
p38: and#(X1,mark(X2)) -> and#(X1,X2)
p39: and#(active(X1),X2) -> and#(X1,X2)
p40: and#(X1,active(X2)) -> and#(X1,X2)
p41: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p42: if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
p43: if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
p44: if#(active(X1),X2,X3) -> if#(X1,X2,X3)
p45: if#(X1,active(X2),X3) -> if#(X1,X2,X3)
p46: if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
p47: add#(mark(X1),X2) -> add#(X1,X2)
p48: add#(X1,mark(X2)) -> add#(X1,X2)
p49: add#(active(X1),X2) -> add#(X1,X2)
p50: add#(X1,active(X2)) -> add#(X1,X2)
p51: s#(mark(X)) -> s#(X)
p52: s#(active(X)) -> s#(X)
p53: first#(mark(X1),X2) -> first#(X1,X2)
p54: first#(X1,mark(X2)) -> first#(X1,X2)
p55: first#(active(X1),X2) -> first#(X1,X2)
p56: first#(X1,active(X2)) -> first#(X1,X2)
p57: cons#(mark(X1),X2) -> cons#(X1,X2)
p58: cons#(X1,mark(X2)) -> cons#(X1,X2)
p59: cons#(active(X1),X2) -> cons#(X1,X2)
p60: cons#(X1,active(X2)) -> cons#(X1,X2)
p61: from#(mark(X)) -> from#(X)
p62: from#(active(X)) -> from#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1, p3, p4, p5, p6, p10, p13, p17, p19, p22, p24, p25, p27, p29, p30, p32, p33, p35, p36}
  {p51, p52}
  {p47, p48, p49, p50}
  {p57, p58, p59, p60}
  {p53, p54, p55, p56}
  {p61, p62}
  {p37, p38, p39, p40}
  {p41, p42, p43, p44, p45, p46}


-- Reduction pair.

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

p1: active#(and(true(),X)) -> mark#(X)
p2: mark#(from(X)) -> active#(from(X))
p3: active#(from(X)) -> mark#(cons(X,from(s(X))))
p4: mark#(cons(X1,X2)) -> active#(cons(X1,X2))
p5: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p6: mark#(first(X1,X2)) -> mark#(X2)
p7: mark#(first(X1,X2)) -> mark#(X1)
p8: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p9: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p10: mark#(s(X)) -> active#(s(X))
p11: active#(add(|0|(),X)) -> mark#(X)
p12: mark#(add(X1,X2)) -> mark#(X1)
p13: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
p14: active#(if(false(),X,Y)) -> mark#(Y)
p15: mark#(if(X1,X2,X3)) -> mark#(X1)
p16: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p17: active#(if(true(),X,Y)) -> mark#(X)
p18: mark#(and(X1,X2)) -> mark#(X1)
p19: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    active#_A(x1) = max{0, x1 - 33}
    and_A(x1,x2) = 34
    true_A = 28
    mark#_A(x1) = 1
    from_A(x1) = 34
    cons_A(x1,x2) = 33
    s_A(x1) = 34
    first_A(x1,x2) = 34
    mark_A(x1) = 31
    add_A(x1,x2) = 34
    |0|_A = 33
    if_A(x1,x2,x3) = 34
    false_A = 33
    active_A(x1) = 31
    nil_A = 34

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: active#(and(true(),X)) -> mark#(X)
p2: mark#(from(X)) -> active#(from(X))
p3: active#(from(X)) -> mark#(cons(X,from(s(X))))
p4: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p5: mark#(first(X1,X2)) -> mark#(X2)
p6: mark#(first(X1,X2)) -> mark#(X1)
p7: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p8: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p9: mark#(s(X)) -> active#(s(X))
p10: active#(add(|0|(),X)) -> mark#(X)
p11: mark#(add(X1,X2)) -> mark#(X1)
p12: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
p13: active#(if(false(),X,Y)) -> mark#(Y)
p14: mark#(if(X1,X2,X3)) -> mark#(X1)
p15: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p16: active#(if(true(),X,Y)) -> mark#(X)
p17: mark#(and(X1,X2)) -> mark#(X1)
p18: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: active#(and(true(),X)) -> mark#(X)
p2: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p3: active#(if(true(),X,Y)) -> mark#(X)
p4: mark#(and(X1,X2)) -> mark#(X1)
p5: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p6: active#(if(false(),X,Y)) -> mark#(Y)
p7: mark#(if(X1,X2,X3)) -> mark#(X1)
p8: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
p9: active#(add(|0|(),X)) -> mark#(X)
p10: mark#(add(X1,X2)) -> mark#(X1)
p11: mark#(s(X)) -> active#(s(X))
p12: active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
p13: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p14: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p15: mark#(first(X1,X2)) -> mark#(X1)
p16: mark#(first(X1,X2)) -> mark#(X2)
p17: mark#(from(X)) -> active#(from(X))
p18: active#(from(X)) -> mark#(cons(X,from(s(X))))

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    active#_A(x1) = max{30, x1 - 4}
    and_A(x1,x2) = max{x1, x2 + 19}
    true_A = 6
    mark#_A(x1) = x1 + 12
    mark_A(x1) = x1 + 5
    if_A(x1,x2,x3) = max{22, x1, x2 + 16, x3 + 19}
    false_A = 6
    add_A(x1,x2) = max{x1 + 18, x2 + 17}
    |0|_A = 6
    s_A(x1) = 18
    first_A(x1,x2) = max{x1 + 18, x2 + 16}
    cons_A(x1,x2) = x1 + 22
    from_A(x1) = max{79, x1 + 38}
    active_A(x1) = max{2, x1}
    nil_A = 5

The next rules are strictly ordered:

  p1, p2, p5, p6, p9, p10, p12, p15, p16, p17

We remove them from the problem.

-- SCC decomposition.

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

p1: active#(if(true(),X,Y)) -> mark#(X)
p2: mark#(and(X1,X2)) -> mark#(X1)
p3: mark#(if(X1,X2,X3)) -> mark#(X1)
p4: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
p5: mark#(s(X)) -> active#(s(X))
p6: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p7: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p8: active#(from(X)) -> mark#(cons(X,from(s(X))))

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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#(if(true(),X,Y)) -> mark#(X)
p2: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p3: active#(from(X)) -> mark#(cons(X,from(s(X))))
p4: mark#(s(X)) -> active#(s(X))
p5: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p6: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
p7: mark#(if(X1,X2,X3)) -> mark#(X1)
p8: mark#(and(X1,X2)) -> mark#(X1)

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    active#_A(x1) = max{0, x1 - 7}
    if_A(x1,x2,x3) = max{x1 + 8, x2 + 10, x3 + 10}
    true_A = 3
    mark#_A(x1) = max{0, x1 - 7}
    first_A(x1,x2) = max{5, x2 + 2}
    mark_A(x1) = max{2, x1}
    from_A(x1) = x1 + 8
    cons_A(x1,x2) = max{x1 + 4, x2}
    s_A(x1) = max{0, x1 - 2}
    add_A(x1,x2) = max{x1 + 8, x2 + 10}
    and_A(x1,x2) = max{x1 + 1, x2 + 3}
    active_A(x1) = max{1, x1}
    false_A = 3
    |0|_A = 3
    nil_A = 0

The next rules are strictly ordered:

  p1, p7

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p2: active#(from(X)) -> mark#(cons(X,from(s(X))))
p3: mark#(s(X)) -> active#(s(X))
p4: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p5: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
p6: mark#(and(X1,X2)) -> mark#(X1)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p2: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p3: mark#(and(X1,X2)) -> mark#(X1)
p4: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
p5: active#(from(X)) -> mark#(cons(X,from(s(X))))
p6: mark#(s(X)) -> active#(s(X))

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = x1 + 2
    first_A(x1,x2) = max{x1 + 1, x2 + 1}
    active#_A(x1) = x1 + 2
    mark_A(x1) = x1
    s_A(x1) = x1
    cons_A(x1,x2) = max{x1 + 1, x2}
    and_A(x1,x2) = max{x1 + 1, x2 + 1}
    add_A(x1,x2) = max{x1 + 1, x2 + 2}
    from_A(x1) = x1 + 1
    active_A(x1) = x1
    true_A = 1
    false_A = 1
    if_A(x1,x2,x3) = max{x1 + 1, x2 + 1, x3 + 1}
    |0|_A = 1
    nil_A = 1

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p2: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p3: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
p4: active#(from(X)) -> mark#(cons(X,from(s(X))))
p5: mark#(s(X)) -> active#(s(X))

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p2: active#(from(X)) -> mark#(cons(X,from(s(X))))
p3: mark#(s(X)) -> active#(s(X))
p4: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p5: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = max{8, x1 + 4}
    first_A(x1,x2) = max{9, x2 + 5}
    active#_A(x1) = x1 + 4
    mark_A(x1) = max{4, x1}
    from_A(x1) = x1 + 6
    cons_A(x1,x2) = max{x1 + 5, x2}
    s_A(x1) = 0
    add_A(x1,x2) = max{x1 + 6, x2 + 10}
    active_A(x1) = max{1, x1}
    and_A(x1,x2) = max{x1 + 5, x2 + 9}
    true_A = 0
    false_A = 5
    if_A(x1,x2,x3) = max{x1 + 5, x2 + 9, x3 + 9}
    |0|_A = 0
    nil_A = 5

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p2: active#(from(X)) -> mark#(cons(X,from(s(X))))
p3: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p4: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p2: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p3: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))
p4: active#(from(X)) -> mark#(cons(X,from(s(X))))

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = max{0, x1 - 5}
    first_A(x1,x2) = max{22, x2 + 13}
    active#_A(x1) = max{7, x1 - 5}
    mark_A(x1) = max{8, x1}
    s_A(x1) = max{0, x1 - 6}
    cons_A(x1,x2) = max{x1 + 10, x2}
    add_A(x1,x2) = x2 + 12
    from_A(x1) = x1 + 11
    active_A(x1) = x1
    and_A(x1,x2) = max{9, x1 - 1, x2 + 7}
    true_A = 9
    false_A = 9
    if_A(x1,x2,x3) = max{x1 + 1, x2 + 9, x3 + 9}
    |0|_A = 9
    nil_A = 13

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: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p2: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p3: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p2: active#(first(s(X),cons(Y,Z))) -> mark#(cons(Y,first(X,Z)))
p3: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    mark#_A(x1) = max{1, x1 - 1}
    first_A(x1,x2) = max{x1 + 4, x2 + 8}
    active#_A(x1) = max{0, x1 - 1}
    mark_A(x1) = x1
    s_A(x1) = max{3, x1 - 1}
    cons_A(x1,x2) = x1 + 2
    add_A(x1,x2) = max{x1 + 3, x2 + 4}
    active_A(x1) = max{1, x1}
    and_A(x1,x2) = max{x1 + 3, x2 + 3}
    true_A = 1
    false_A = 2
    if_A(x1,x2,x3) = max{x1 + 1, x2 + 1, x3 + 1}
    |0|_A = 1
    nil_A = 6
    from_A(x1) = x1 + 3

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: mark#(first(X1,X2)) -> active#(first(mark(X1),mark(X2)))
p2: mark#(add(X1,X2)) -> active#(add(mark(X1),X2))

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: s#(mark(X)) -> s#(X)
p2: s#(active(X)) -> s#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    s#_A(x1) = max{0, x1 - 1}
    mark_A(x1) = x1 + 1
    active_A(x1) = x1 + 2

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: s#(mark(X)) -> s#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  max/plus interpretations on natural numbers:
  
    s#_A(x1) = x1
    mark_A(x1) = x1 + 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#(X1,active(X2)) -> add#(X1,X2)
p3: add#(active(X1),X2) -> add#(X1,X2)
p4: add#(X1,mark(X2)) -> add#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    add#_A(x1,x2) = x2
    mark_A(x1) = x1 + 1
    active_A(x1) = x1

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

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: add#(mark(X1),X2) -> add#(X1,X2)
p2: add#(active(X1),X2) -> add#(X1,X2)
p3: add#(X1,active(X2)) -> add#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    add#_A(x1,x2) = x2 + 1
    mark_A(x1) = max{0, x1 - 1}
    active_A(x1) = x1 + 1

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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#(active(X1),X2) -> add#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    add#_A(x1,x2) = x1
    mark_A(x1) = x1
    active_A(x1) = x1 + 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)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    add#_A(x1,x2) = x1
    mark_A(x1) = x1 + 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#(X1,active(X2)) -> cons#(X1,X2)
p3: cons#(active(X1),X2) -> cons#(X1,X2)
p4: cons#(X1,mark(X2)) -> cons#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    cons#_A(x1,x2) = x2
    mark_A(x1) = x1 + 1
    active_A(x1) = x1

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: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(X1,active(X2)) -> cons#(X1,X2)
p3: cons#(active(X1),X2) -> cons#(X1,X2)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(active(X1),X2) -> cons#(X1,X2)
p3: cons#(X1,active(X2)) -> cons#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    cons#_A(x1,x2) = x2 + 1
    mark_A(x1) = max{0, x1 - 1}
    active_A(x1) = x1 + 1

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: cons#(mark(X1),X2) -> cons#(X1,X2)
p2: cons#(active(X1),X2) -> cons#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    cons#_A(x1,x2) = x1
    mark_A(x1) = x1
    active_A(x1) = x1 + 1

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    cons#_A(x1,x2) = x1
    mark_A(x1) = x1 + 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#(X1,active(X2)) -> first#(X1,X2)
p3: first#(active(X1),X2) -> first#(X1,X2)
p4: first#(X1,mark(X2)) -> first#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    first#_A(x1,x2) = x2
    mark_A(x1) = x1 + 1
    active_A(x1) = x1

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: first#(mark(X1),X2) -> first#(X1,X2)
p2: first#(X1,active(X2)) -> first#(X1,X2)
p3: first#(active(X1),X2) -> first#(X1,X2)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: first#(mark(X1),X2) -> first#(X1,X2)
p2: first#(active(X1),X2) -> first#(X1,X2)
p3: first#(X1,active(X2)) -> first#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    first#_A(x1,x2) = x2 + 1
    mark_A(x1) = max{0, x1 - 1}
    active_A(x1) = x1 + 1

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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#(active(X1),X2) -> first#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    first#_A(x1,x2) = x1
    mark_A(x1) = x1
    active_A(x1) = x1 + 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)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    first#_A(x1,x2) = x1
    mark_A(x1) = x1 + 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: from#(mark(X)) -> from#(X)
p2: from#(active(X)) -> from#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    from#_A(x1) = max{0, x1 - 1}
    mark_A(x1) = x1 + 1
    active_A(x1) = x1 + 2

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: from#(mark(X)) -> from#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: from#(mark(X)) -> from#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  max/plus interpretations on natural numbers:
  
    from#_A(x1) = x1
    mark_A(x1) = x1 + 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: and#(mark(X1),X2) -> and#(X1,X2)
p2: and#(X1,active(X2)) -> and#(X1,X2)
p3: and#(active(X1),X2) -> and#(X1,X2)
p4: and#(X1,mark(X2)) -> and#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    and#_A(x1,x2) = x2
    mark_A(x1) = x1 + 1
    active_A(x1) = x1

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: and#(mark(X1),X2) -> and#(X1,X2)
p2: and#(X1,active(X2)) -> and#(X1,X2)
p3: and#(active(X1),X2) -> and#(X1,X2)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: and#(mark(X1),X2) -> and#(X1,X2)
p2: and#(active(X1),X2) -> and#(X1,X2)
p3: and#(X1,active(X2)) -> and#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    and#_A(x1,x2) = x2 + 1
    mark_A(x1) = max{0, x1 - 1}
    active_A(x1) = x1 + 1

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: and#(mark(X1),X2) -> and#(X1,X2)
p2: and#(active(X1),X2) -> and#(X1,X2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    and#_A(x1,x2) = x1
    mark_A(x1) = x1
    active_A(x1) = x1 + 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: and#(mark(X1),X2) -> and#(X1,X2)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    and#_A(x1,x2) = x1
    mark_A(x1) = x1 + 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: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p2: if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
p3: if#(X1,active(X2),X3) -> if#(X1,X2,X3)
p4: if#(active(X1),X2,X3) -> if#(X1,X2,X3)
p5: if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
p6: if#(X1,mark(X2),X3) -> if#(X1,X2,X3)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    if#_A(x1,x2,x3) = x3 + 1
    mark_A(x1) = x1 + 1
    active_A(x1) = x1

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- SCC decomposition.

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

p1: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p2: if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
p3: if#(X1,active(X2),X3) -> if#(X1,X2,X3)
p4: if#(active(X1),X2,X3) -> if#(X1,X2,X3)
p5: if#(X1,mark(X2),X3) -> if#(X1,X2,X3)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p2: if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
p3: if#(active(X1),X2,X3) -> if#(X1,X2,X3)
p4: if#(X1,active(X2),X3) -> if#(X1,X2,X3)
p5: if#(X1,X2,active(X3)) -> if#(X1,X2,X3)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    if#_A(x1,x2,x3) = x3
    mark_A(x1) = x1 + 2
    active_A(x1) = x1 + 1

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- SCC decomposition.

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

p1: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p2: if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
p3: if#(active(X1),X2,X3) -> if#(X1,X2,X3)
p4: if#(X1,active(X2),X3) -> if#(X1,X2,X3)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p2: if#(X1,active(X2),X3) -> if#(X1,X2,X3)
p3: if#(active(X1),X2,X3) -> if#(X1,X2,X3)
p4: if#(X1,mark(X2),X3) -> if#(X1,X2,X3)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    if#_A(x1,x2,x3) = max{2, x2 + 1}
    mark_A(x1) = x1 + 2
    active_A(x1) = x1 + 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: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p2: if#(X1,active(X2),X3) -> if#(X1,X2,X3)
p3: if#(active(X1),X2,X3) -> if#(X1,X2,X3)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p2: if#(active(X1),X2,X3) -> if#(X1,X2,X3)
p3: if#(X1,active(X2),X3) -> if#(X1,X2,X3)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    if#_A(x1,x2,x3) = x1 + 1
    mark_A(x1) = x1
    active_A(x1) = x1 + 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: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p2: if#(X1,active(X2),X3) -> if#(X1,X2,X3)

and R consists of:

r1: active(and(true(),X)) -> mark(X)
r2: active(and(false(),Y)) -> mark(false())
r3: active(if(true(),X,Y)) -> mark(X)
r4: active(if(false(),X,Y)) -> mark(Y)
r5: active(add(|0|(),X)) -> mark(X)
r6: active(add(s(X),Y)) -> mark(s(add(X,Y)))
r7: active(first(|0|(),X)) -> mark(nil())
r8: active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z)))
r9: active(from(X)) -> mark(cons(X,from(s(X))))
r10: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r11: mark(true()) -> active(true())
r12: mark(false()) -> active(false())
r13: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r14: mark(add(X1,X2)) -> active(add(mark(X1),X2))
r15: mark(|0|()) -> active(|0|())
r16: mark(s(X)) -> active(s(X))
r17: mark(first(X1,X2)) -> active(first(mark(X1),mark(X2)))
r18: mark(nil()) -> active(nil())
r19: mark(cons(X1,X2)) -> active(cons(X1,X2))
r20: mark(from(X)) -> active(from(X))
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r26: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r27: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r28: if(active(X1),X2,X3) -> if(X1,X2,X3)
r29: if(X1,active(X2),X3) -> if(X1,X2,X3)
r30: if(X1,X2,active(X3)) -> if(X1,X2,X3)
r31: add(mark(X1),X2) -> add(X1,X2)
r32: add(X1,mark(X2)) -> add(X1,X2)
r33: add(active(X1),X2) -> add(X1,X2)
r34: add(X1,active(X2)) -> add(X1,X2)
r35: s(mark(X)) -> s(X)
r36: s(active(X)) -> s(X)
r37: first(mark(X1),X2) -> first(X1,X2)
r38: first(X1,mark(X2)) -> first(X1,X2)
r39: first(active(X1),X2) -> first(X1,X2)
r40: first(X1,active(X2)) -> first(X1,X2)
r41: cons(mark(X1),X2) -> cons(X1,X2)
r42: cons(X1,mark(X2)) -> cons(X1,X2)
r43: cons(active(X1),X2) -> cons(X1,X2)
r44: cons(X1,active(X2)) -> cons(X1,X2)
r45: from(mark(X)) -> from(X)
r46: from(active(X)) -> from(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: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p2: if#(X1,active(X2),X3) -> if#(X1,X2,X3)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    if#_A(x1,x2,x3) = x1
    mark_A(x1) = x1 + 1
    active_A(x1) = max{0, x1 - 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: if#(X1,active(X2),X3) -> if#(X1,X2,X3)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: if#(X1,active(X2),X3) -> if#(X1,X2,X3)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  max/plus interpretations on natural numbers:
  
    if#_A(x1,x2,x3) = x2
    active_A(x1) = x1 + 1

The next rules are strictly ordered:

  p1

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