YES

TRS:

  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)

max/plus interpretations on N:

  active_A(x1) = max{74, x1}
  active#_A(x1) = max{776, 634 + x1}
  minus_A(x1,x2) = max{36, -163, 36}
  minus#_A(x1,x2) = max{1150, 669 + x1, 1148}
  0_A = 36
  0#_A = 1356
  mark_A(x1) = max{56, 38 + x1}
  mark#_A(x1) = max{1149, 675 + x1}
  s_A(x1) = max{406, 43 + x1}
  s#_A(x1) = max{632, 633}
  geq_A(x1,x2) = max{519, 482 + x1, 665}
  geq#_A(x1,x2) = max{667, 775, 783}
  true_A = 626
  true#_A = 1300
  false_A = 623
  false#_A = 782
  div_A(x1,x2) = max{721, 500 + x1, 517}
  div#_A(x1,x2) = max{778, 741 + x1, 668}
  if_A(x1,x2,x3) = max{1, 19 + x1, 100 + x2, 61 + x3}
  if#_A(x1,x2,x3) = max{0, 2 + x1, 1, 735 + x3}

precedence:

  div > geq > true > active > 0 > false > minus = mark > s = if