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

-- SCC decomposition.

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

p1: active#(add(s(X),Y)) -> s#(add(X,Y))
p2: active#(add(s(X),Y)) -> add#(X,Y)
p3: active#(first(s(X),cons(Y,Z))) -> cons#(Y,first(X,Z))
p4: active#(first(s(X),cons(Y,Z))) -> first#(X,Z)
p5: active#(from(X)) -> cons#(X,from(s(X)))
p6: active#(from(X)) -> from#(s(X))
p7: active#(from(X)) -> s#(X)
p8: active#(and(X1,X2)) -> and#(active(X1),X2)
p9: active#(and(X1,X2)) -> active#(X1)
p10: active#(if(X1,X2,X3)) -> if#(active(X1),X2,X3)
p11: active#(if(X1,X2,X3)) -> active#(X1)
p12: active#(add(X1,X2)) -> add#(active(X1),X2)
p13: active#(add(X1,X2)) -> active#(X1)
p14: active#(first(X1,X2)) -> first#(active(X1),X2)
p15: active#(first(X1,X2)) -> active#(X1)
p16: active#(first(X1,X2)) -> first#(X1,active(X2))
p17: active#(first(X1,X2)) -> active#(X2)
p18: and#(mark(X1),X2) -> and#(X1,X2)
p19: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p20: add#(mark(X1),X2) -> add#(X1,X2)
p21: first#(mark(X1),X2) -> first#(X1,X2)
p22: first#(X1,mark(X2)) -> first#(X1,X2)
p23: proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
p24: proper#(and(X1,X2)) -> proper#(X1)
p25: proper#(and(X1,X2)) -> proper#(X2)
p26: proper#(if(X1,X2,X3)) -> if#(proper(X1),proper(X2),proper(X3))
p27: proper#(if(X1,X2,X3)) -> proper#(X1)
p28: proper#(if(X1,X2,X3)) -> proper#(X2)
p29: proper#(if(X1,X2,X3)) -> proper#(X3)
p30: proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
p31: proper#(add(X1,X2)) -> proper#(X1)
p32: proper#(add(X1,X2)) -> proper#(X2)
p33: proper#(s(X)) -> s#(proper(X))
p34: proper#(s(X)) -> proper#(X)
p35: proper#(first(X1,X2)) -> first#(proper(X1),proper(X2))
p36: proper#(first(X1,X2)) -> proper#(X1)
p37: proper#(first(X1,X2)) -> proper#(X2)
p38: proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
p39: proper#(cons(X1,X2)) -> proper#(X1)
p40: proper#(cons(X1,X2)) -> proper#(X2)
p41: proper#(from(X)) -> from#(proper(X))
p42: proper#(from(X)) -> proper#(X)
p43: and#(ok(X1),ok(X2)) -> and#(X1,X2)
p44: if#(ok(X1),ok(X2),ok(X3)) -> if#(X1,X2,X3)
p45: add#(ok(X1),ok(X2)) -> add#(X1,X2)
p46: s#(ok(X)) -> s#(X)
p47: first#(ok(X1),ok(X2)) -> first#(X1,X2)
p48: cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
p49: from#(ok(X)) -> from#(X)
p50: top#(mark(X)) -> top#(proper(X))
p51: top#(mark(X)) -> proper#(X)
p52: top#(ok(X)) -> top#(active(X))
p53: top#(ok(X)) -> active#(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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p50, p52}
  {p9, p11, p13, p15, p17}
  {p24, p25, p27, p28, p29, p31, p32, p34, p36, p37, p39, p40, p42}
  {p46}
  {p20, p45}
  {p48}
  {p21, p22, p47}
  {p49}
  {p18, p43}
  {p19, p44}


-- Reduction pair.

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

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

and R consists of:

r1: active(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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The set of usable rules consists of

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

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      top#_A(x1) = ((1,0,0),(1,1,0),(0,1,0)) x1
      ok_A(x1) = x1 + (0,4,2)
      active_A(x1) = ((1,0,0),(0,0,0),(1,1,0)) x1 + (0,4,0)
      mark_A(x1) = x1 + (9,1,26)
      proper_A(x1) = ((1,0,0),(1,0,0),(0,1,0)) x1
      and_A(x1,x2) = ((1,0,0),(0,1,0),(0,1,0)) x1 + x2 + (30,0,26)
      if_A(x1,x2,x3) = x1 + ((1,0,0),(0,0,0),(1,0,0)) x2 + ((1,0,0),(0,0,0),(1,0,0)) x3 + (22,0,1)
      add_A(x1,x2) = ((1,0,0),(0,0,0),(1,0,0)) x1 + x2 + (15,4,18)
      first_A(x1,x2) = x1 + x2 + (9,4,3)
      s_A(x1) = (6,5,3)
      cons_A(x1,x2) = ((0,0,0),(0,0,0),(1,0,0)) x2 + (6,5,1)
      from_A(x1) = ((1,0,0),(0,1,0),(1,0,0)) x1 + (27,0,3)
      true_A() = (5,3,1)
      false_A() = (5,0,1)
      |0|_A() = (6,0,1)
      nil_A() = (5,3,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: top#(ok(X)) -> top#(active(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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

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

and R consists of:

r1: active(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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r31, r32, r33, r34, r35, r36, r37

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      top#_A(x1) = ((0,0,0),(1,0,0),(0,0,0)) x1
      ok_A(x1) = ((1,0,0),(0,0,0),(1,1,0)) x1 + (5,1,9)
      active_A(x1) = x1 + (4,3,4)
      and_A(x1,x2) = ((0,0,0),(1,0,0),(0,0,0)) x1 + ((1,0,0),(0,0,0),(0,1,0)) x2 + (1,2,0)
      mark_A(x1) = ((0,0,0),(1,0,0),(1,1,0)) x1 + (0,0,1)
      if_A(x1,x2,x3) = ((0,0,0),(1,0,0),(0,0,0)) x1 + ((1,0,0),(1,1,0),(0,0,0)) x2 + (1,2,5)
      add_A(x1,x2) = ((0,0,0),(1,0,0),(0,0,0)) x1 + ((1,0,0),(1,1,0),(1,0,1)) x2 + (1,0,5)
      first_A(x1,x2) = ((1,0,0),(0,0,0),(0,1,0)) x1 + ((0,0,0),(0,0,0),(1,0,0)) x2 + (1,2,5)
      s_A(x1) = ((1,0,0),(1,1,0),(1,1,0)) x1 + (1,1,1)
      cons_A(x1,x2) = ((1,0,0),(0,1,0),(1,1,1)) x1 + x2 + (1,7,1)
      from_A(x1) = x1 + (2,1,4)
      true_A() = (1,1,1)
      false_A() = (1,3,1)
      |0|_A() = (1,1,0)
      nil_A() = (1,1,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: active#(first(X1,X2)) -> active#(X2)
p2: active#(first(X1,X2)) -> active#(X1)
p3: active#(add(X1,X2)) -> active#(X1)
p4: active#(if(X1,X2,X3)) -> active#(X1)
p5: active#(and(X1,X2)) -> active#(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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      active#_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1
      first_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(0,1,0),(1,1,1)) x2 + (1,1,1)
      add_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)
      if_A(x1,x2,x3) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + ((1,0,0),(1,1,0),(1,1,1)) x3 + (1,1,1)
      and_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5
  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

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

-- Reduction pair.

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

p1: proper#(from(X)) -> proper#(X)
p2: proper#(cons(X1,X2)) -> proper#(X2)
p3: proper#(cons(X1,X2)) -> proper#(X1)
p4: proper#(first(X1,X2)) -> proper#(X2)
p5: proper#(first(X1,X2)) -> proper#(X1)
p6: proper#(s(X)) -> proper#(X)
p7: proper#(add(X1,X2)) -> proper#(X2)
p8: proper#(add(X1,X2)) -> proper#(X1)
p9: proper#(if(X1,X2,X3)) -> proper#(X3)
p10: proper#(if(X1,X2,X3)) -> proper#(X2)
p11: proper#(if(X1,X2,X3)) -> proper#(X1)
p12: proper#(and(X1,X2)) -> proper#(X2)
p13: proper#(and(X1,X2)) -> proper#(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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      proper#_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1
      from_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      cons_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)
      first_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)
      s_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      add_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)
      if_A(x1,x2,x3) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + ((1,0,0),(1,1,0),(1,1,1)) x3 + (1,1,1)
      and_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13
  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

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

-- Reduction pair.

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

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

and R consists of:

r1: active(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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      s#_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1
      ok_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

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

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

-- Reduction pair.

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

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

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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      add#_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      ok_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

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

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#(ok(X1),ok(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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      cons#_A(x1,x2) = ((0,0,0),(0,0,0),(1,0,0)) x1
      ok_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1

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

-- Reduction pair.

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

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

and R consists of:

r1: active(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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      first#_A(x1,x2) = ((1,0,0),(1,1,0),(1,0,0)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      ok_A(x1) = ((1,0,0),(1,1,0),(1,1,0)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3

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#(ok(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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      from#_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1
      ok_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

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

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#(ok(X1),ok(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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      and#_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      ok_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

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

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#(ok(X1),ok(X2),ok(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: active(and(X1,X2)) -> and(active(X1),X2)
r11: active(if(X1,X2,X3)) -> if(active(X1),X2,X3)
r12: active(add(X1,X2)) -> add(active(X1),X2)
r13: active(first(X1,X2)) -> first(active(X1),X2)
r14: active(first(X1,X2)) -> first(X1,active(X2))
r15: and(mark(X1),X2) -> mark(and(X1,X2))
r16: if(mark(X1),X2,X3) -> mark(if(X1,X2,X3))
r17: add(mark(X1),X2) -> mark(add(X1,X2))
r18: first(mark(X1),X2) -> mark(first(X1,X2))
r19: first(X1,mark(X2)) -> mark(first(X1,X2))
r20: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
r21: proper(true()) -> ok(true())
r22: proper(false()) -> ok(false())
r23: proper(if(X1,X2,X3)) -> if(proper(X1),proper(X2),proper(X3))
r24: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
r25: proper(|0|()) -> ok(|0|())
r26: proper(s(X)) -> s(proper(X))
r27: proper(first(X1,X2)) -> first(proper(X1),proper(X2))
r28: proper(nil()) -> ok(nil())
r29: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
r30: proper(from(X)) -> from(proper(X))
r31: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
r32: if(ok(X1),ok(X2),ok(X3)) -> ok(if(X1,X2,X3))
r33: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
r34: s(ok(X)) -> ok(s(X))
r35: first(ok(X1),ok(X2)) -> ok(first(X1,X2))
r36: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
r37: from(ok(X)) -> ok(from(X))
r38: top(mark(X)) -> top(proper(X))
r39: top(ok(X)) -> top(active(X))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      if#_A(x1,x2,x3) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + ((1,0,0),(1,1,0),(1,1,1)) x3
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      ok_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

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

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