YES

We show the termination of the TRS R:

  active(minus(|0|(),Y)) -> mark(|0|())
  active(minus(s(X),s(Y))) -> mark(minus(X,Y))
  active(geq(X,|0|())) -> mark(true())
  active(geq(|0|(),s(Y))) -> mark(false())
  active(geq(s(X),s(Y))) -> mark(geq(X,Y))
  active(div(|0|(),s(Y))) -> mark(|0|())
  active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
  active(if(true(),X,Y)) -> mark(X)
  active(if(false(),X,Y)) -> mark(Y)
  mark(minus(X1,X2)) -> active(minus(X1,X2))
  mark(|0|()) -> active(|0|())
  mark(s(X)) -> active(s(mark(X)))
  mark(geq(X1,X2)) -> active(geq(X1,X2))
  mark(true()) -> active(true())
  mark(false()) -> active(false())
  mark(div(X1,X2)) -> active(div(mark(X1),X2))
  mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
  minus(mark(X1),X2) -> minus(X1,X2)
  minus(X1,mark(X2)) -> minus(X1,X2)
  minus(active(X1),X2) -> minus(X1,X2)
  minus(X1,active(X2)) -> minus(X1,X2)
  s(mark(X)) -> s(X)
  s(active(X)) -> s(X)
  geq(mark(X1),X2) -> geq(X1,X2)
  geq(X1,mark(X2)) -> geq(X1,X2)
  geq(active(X1),X2) -> geq(X1,X2)
  geq(X1,active(X2)) -> geq(X1,X2)
  div(mark(X1),X2) -> div(X1,X2)
  div(X1,mark(X2)) -> div(X1,X2)
  div(active(X1),X2) -> div(X1,X2)
  div(X1,active(X2)) -> div(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)

-- SCC decomposition.

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

p1: active#(minus(|0|(),Y)) -> mark#(|0|())
p2: active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
p3: active#(minus(s(X),s(Y))) -> minus#(X,Y)
p4: active#(geq(X,|0|())) -> mark#(true())
p5: active#(geq(|0|(),s(Y))) -> mark#(false())
p6: active#(geq(s(X),s(Y))) -> mark#(geq(X,Y))
p7: active#(geq(s(X),s(Y))) -> geq#(X,Y)
p8: active#(div(|0|(),s(Y))) -> mark#(|0|())
p9: active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
p10: active#(div(s(X),s(Y))) -> if#(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|())
p11: active#(div(s(X),s(Y))) -> geq#(X,Y)
p12: active#(div(s(X),s(Y))) -> s#(div(minus(X,Y),s(Y)))
p13: active#(div(s(X),s(Y))) -> div#(minus(X,Y),s(Y))
p14: active#(div(s(X),s(Y))) -> minus#(X,Y)
p15: active#(if(true(),X,Y)) -> mark#(X)
p16: active#(if(false(),X,Y)) -> mark#(Y)
p17: mark#(minus(X1,X2)) -> active#(minus(X1,X2))
p18: mark#(|0|()) -> active#(|0|())
p19: mark#(s(X)) -> active#(s(mark(X)))
p20: mark#(s(X)) -> s#(mark(X))
p21: mark#(s(X)) -> mark#(X)
p22: mark#(geq(X1,X2)) -> active#(geq(X1,X2))
p23: mark#(true()) -> active#(true())
p24: mark#(false()) -> active#(false())
p25: mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
p26: mark#(div(X1,X2)) -> div#(mark(X1),X2)
p27: mark#(div(X1,X2)) -> mark#(X1)
p28: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p29: mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
p30: mark#(if(X1,X2,X3)) -> mark#(X1)
p31: minus#(mark(X1),X2) -> minus#(X1,X2)
p32: minus#(X1,mark(X2)) -> minus#(X1,X2)
p33: minus#(active(X1),X2) -> minus#(X1,X2)
p34: minus#(X1,active(X2)) -> minus#(X1,X2)
p35: s#(mark(X)) -> s#(X)
p36: s#(active(X)) -> s#(X)
p37: geq#(mark(X1),X2) -> geq#(X1,X2)
p38: geq#(X1,mark(X2)) -> geq#(X1,X2)
p39: geq#(active(X1),X2) -> geq#(X1,X2)
p40: geq#(X1,active(X2)) -> geq#(X1,X2)
p41: div#(mark(X1),X2) -> div#(X1,X2)
p42: div#(X1,mark(X2)) -> div#(X1,X2)
p43: div#(active(X1),X2) -> div#(X1,X2)
p44: div#(X1,active(X2)) -> div#(X1,X2)
p45: if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
p46: if#(X1,mark(X2),X3) -> if#(X1,X2,X3)
p47: if#(X1,X2,mark(X3)) -> if#(X1,X2,X3)
p48: if#(active(X1),X2,X3) -> if#(X1,X2,X3)
p49: if#(X1,active(X2),X3) -> if#(X1,X2,X3)
p50: if#(X1,X2,active(X3)) -> if#(X1,X2,X3)

and R consists of:

r1: active(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

The estimated dependency graph contains the following SCCs:

  {p2, p6, p9, p15, p16, p17, p19, p21, p22, p25, p27, p28, p30}
  {p31, p32, p33, p34}
  {p37, p38, p39, p40}
  {p45, p46, p47, p48, p49, p50}
  {p35, p36}
  {p41, p42, p43, p44}


-- Reduction pair.

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

p1: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p2: active#(if(false(),X,Y)) -> mark#(Y)
p3: mark#(if(X1,X2,X3)) -> mark#(X1)
p4: mark#(div(X1,X2)) -> mark#(X1)
p5: mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
p6: active#(if(true(),X,Y)) -> mark#(X)
p7: mark#(geq(X1,X2)) -> active#(geq(X1,X2))
p8: active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
p9: mark#(s(X)) -> mark#(X)
p10: mark#(s(X)) -> active#(s(mark(X)))
p11: active#(geq(s(X),s(Y))) -> mark#(geq(X,Y))
p12: mark#(minus(X1,X2)) -> active#(minus(X1,X2))
p13: active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))

and R consists of:

r1: active(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

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:
      mark#_A(x1) = ((1,0,0),(1,0,0),(0,0,0)) x1
      if_A(x1,x2,x3) = ((1,0,0),(0,0,0),(1,1,0)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + ((1,0,0),(1,1,0),(1,1,1)) x3 + (0,2,13)
      active#_A(x1) = ((1,0,0),(1,0,0),(0,0,0)) x1
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (0,17,16)
      false_A() = (0,5,1)
      div_A(x1,x2) = ((1,0,0),(0,0,0),(1,1,0)) x1 + ((1,0,0),(1,1,0),(1,1,1)) x2 + (1,13,1)
      true_A() = (0,1,1)
      geq_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((0,0,0),(1,0,0),(1,1,0)) x2 + (0,3,14)
      s_A(x1) = ((1,0,0),(1,0,0),(1,1,0)) x1 + (3,1,1)
      minus_A(x1,x2) = ((0,0,0),(1,0,0),(1,1,0)) x1 + ((0,0,0),(1,0,0),(1,1,0)) x2 + (0,3,1)
      |0|_A() = (0,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(0,1,1)) x1 + (0,16,1)

The next rules are strictly ordered:

  p4, p9, p11

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p2: active#(if(false(),X,Y)) -> mark#(Y)
p3: mark#(if(X1,X2,X3)) -> mark#(X1)
p4: mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
p5: active#(if(true(),X,Y)) -> mark#(X)
p6: mark#(geq(X1,X2)) -> active#(geq(X1,X2))
p7: active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
p8: mark#(s(X)) -> active#(s(mark(X)))
p9: mark#(minus(X1,X2)) -> active#(minus(X1,X2))
p10: active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))

and R consists of:

r1: active(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p2: active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
p3: mark#(minus(X1,X2)) -> active#(minus(X1,X2))
p4: active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
p5: mark#(s(X)) -> active#(s(mark(X)))
p6: active#(if(true(),X,Y)) -> mark#(X)
p7: mark#(geq(X1,X2)) -> active#(geq(X1,X2))
p8: active#(if(false(),X,Y)) -> mark#(Y)
p9: mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
p10: mark#(if(X1,X2,X3)) -> mark#(X1)

and R consists of:

r1: active(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

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:
      mark#_A(x1) = (0,0,2)
      if_A(x1,x2,x3) = (2,1,1)
      active#_A(x1) = ((0,0,0),(0,0,0),(1,0,0)) x1
      mark_A(x1) = (1,1,1)
      minus_A(x1,x2) = (2,1,1)
      s_A(x1) = (1,1,1)
      div_A(x1,x2) = (2,1,1)
      geq_A(x1,x2) = (1,1,1)
      |0|_A() = (1,1,1)
      true_A() = (1,1,1)
      false_A() = (1,1,1)
      active_A(x1) = (1,1,1)

The next rules are strictly ordered:

  p5, p7

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p2: active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
p3: mark#(minus(X1,X2)) -> active#(minus(X1,X2))
p4: active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
p5: active#(if(true(),X,Y)) -> mark#(X)
p6: active#(if(false(),X,Y)) -> mark#(Y)
p7: mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
p8: mark#(if(X1,X2,X3)) -> mark#(X1)

and R consists of:

r1: active(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

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: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p2: active#(if(false(),X,Y)) -> mark#(Y)
p3: mark#(if(X1,X2,X3)) -> mark#(X1)
p4: mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
p5: active#(if(true(),X,Y)) -> mark#(X)
p6: mark#(minus(X1,X2)) -> active#(minus(X1,X2))
p7: active#(div(s(X),s(Y))) -> mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
p8: active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))

and R consists of:

r1: active(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

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:
      mark#_A(x1) = ((0,0,0),(1,0,0),(0,1,0)) x1
      if_A(x1,x2,x3) = x1 + x2 + ((1,0,0),(1,1,0),(1,0,1)) x3 + (0,1,0)
      active#_A(x1) = ((0,0,0),(1,0,0),(0,1,0)) x1
      mark_A(x1) = x1 + (0,0,2)
      false_A() = (0,1,1)
      div_A(x1,x2) = ((1,0,0),(1,0,0),(0,1,0)) x1 + ((0,0,0),(1,0,0),(1,1,0)) x2 + (1,2,1)
      true_A() = (0,1,1)
      minus_A(x1,x2) = ((0,0,0),(0,0,0),(1,0,0)) x1 + ((0,0,0),(0,0,0),(1,0,0)) x2 + (0,1,3)
      s_A(x1) = ((1,0,0),(1,0,0),(1,0,0)) x1 + (2,1,1)
      geq_A(x1,x2) = ((0,0,0),(1,0,0),(0,0,0)) x1 + ((0,0,0),(1,0,0),(1,0,0)) x2 + (0,2,1)
      |0|_A() = (0,0,1)
      active_A(x1) = x1 + (0,0,1)

The next rules are strictly ordered:

  p2, p3, p5, p7

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p2: mark#(div(X1,X2)) -> active#(div(mark(X1),X2))
p3: mark#(minus(X1,X2)) -> active#(minus(X1,X2))
p4: active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))

and R consists of:

r1: active(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

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#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
p2: active#(minus(s(X),s(Y))) -> mark#(minus(X,Y))
p3: mark#(minus(X1,X2)) -> active#(minus(X1,X2))
p4: mark#(div(X1,X2)) -> active#(div(mark(X1),X2))

and R consists of:

r1: active(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

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:
      mark#_A(x1) = x1
      if_A(x1,x2,x3) = x2 + x3 + (0,2,3)
      active#_A(x1) = x1 + (0,2,2)
      mark_A(x1) = ((1,0,0),(1,1,0),(0,1,0)) x1 + (0,2,5)
      minus_A(x1,x2) = ((1,0,0),(1,1,0),(1,0,1)) x1 + ((0,0,0),(1,0,0),(1,0,0)) x2 + (0,23,2)
      s_A(x1) = ((1,0,0),(0,0,0),(0,1,0)) x1 + (8,7,9)
      div_A(x1,x2) = ((1,0,0),(0,0,0),(0,1,0)) x1 + ((0,0,0),(1,0,0),(1,0,0)) x2 + (0,3,0)
      active_A(x1) = ((1,0,0),(1,1,0),(0,0,1)) x1 + (0,1,1)
      |0|_A() = (0,1,4)
      geq_A(x1,x2) = x1 + x2 + (1,3,7)
      true_A() = (1,1,6)
      false_A() = (1,4,1)

The next rules are strictly ordered:

  p1, p2, p3, p4

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

and R consists of:

r1: active(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      minus#_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)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

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

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

and R consists of:

r1: active(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      geq#_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)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

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

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(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

The set of usable rules consists of

  (no rules)

Take the 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,0)) x3
      mark_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6

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

-- Reduction pair.

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

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

and R consists of:

r1: active(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

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),(1,1,0),(1,1,1)) x1
      mark_A(x1) = ((1,0,0),(0,1,0),(1,1,1)) x1 + (1,1,1)
      active_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

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

and R consists of:

r1: active(minus(|0|(),Y)) -> mark(|0|())
r2: active(minus(s(X),s(Y))) -> mark(minus(X,Y))
r3: active(geq(X,|0|())) -> mark(true())
r4: active(geq(|0|(),s(Y))) -> mark(false())
r5: active(geq(s(X),s(Y))) -> mark(geq(X,Y))
r6: active(div(|0|(),s(Y))) -> mark(|0|())
r7: active(div(s(X),s(Y))) -> mark(if(geq(X,Y),s(div(minus(X,Y),s(Y))),|0|()))
r8: active(if(true(),X,Y)) -> mark(X)
r9: active(if(false(),X,Y)) -> mark(Y)
r10: mark(minus(X1,X2)) -> active(minus(X1,X2))
r11: mark(|0|()) -> active(|0|())
r12: mark(s(X)) -> active(s(mark(X)))
r13: mark(geq(X1,X2)) -> active(geq(X1,X2))
r14: mark(true()) -> active(true())
r15: mark(false()) -> active(false())
r16: mark(div(X1,X2)) -> active(div(mark(X1),X2))
r17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
r18: minus(mark(X1),X2) -> minus(X1,X2)
r19: minus(X1,mark(X2)) -> minus(X1,X2)
r20: minus(active(X1),X2) -> minus(X1,X2)
r21: minus(X1,active(X2)) -> minus(X1,X2)
r22: s(mark(X)) -> s(X)
r23: s(active(X)) -> s(X)
r24: geq(mark(X1),X2) -> geq(X1,X2)
r25: geq(X1,mark(X2)) -> geq(X1,X2)
r26: geq(active(X1),X2) -> geq(X1,X2)
r27: geq(X1,active(X2)) -> geq(X1,X2)
r28: div(mark(X1),X2) -> div(X1,X2)
r29: div(X1,mark(X2)) -> div(X1,X2)
r30: div(active(X1),X2) -> div(X1,X2)
r31: div(X1,active(X2)) -> div(X1,X2)
r32: if(mark(X1),X2,X3) -> if(X1,X2,X3)
r33: if(X1,mark(X2),X3) -> if(X1,X2,X3)
r34: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
r35: if(active(X1),X2,X3) -> if(X1,X2,X3)
r36: if(X1,active(X2),X3) -> if(X1,X2,X3)
r37: if(X1,X2,active(X3)) -> if(X1,X2,X3)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      div#_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)
      active_A(x1) = ((1,0,0),(1,1,0),(1,1,1)) x1 + (1,1,1)

The next rules are strictly ordered:

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

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