YES

TRS:

  minus(n__0(),Y) -> 0()
  minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
  geq(X,n__0()) -> true()
  geq(n__0(),n__s(Y)) -> false()
  geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
  div(0(),n__s(Y)) -> 0()
  div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0())
  if(true(),X,Y) -> activate(X)
  if(false(),X,Y) -> activate(Y)
  0() -> n__0()
  s(X) -> n__s(X)
  activate(n__0()) -> 0()
  activate(n__s(X)) -> s(X)
  activate(X) -> X

max/plus interpretations on N:

  minus_A(x1,x2) = max{0, -14, -13}
  minus#_A(x1,x2) = max{6, 2 + x1, 7}
  n__0_A = 0
  n__0#_A = 2
  0_A = 0
  0#_A = 3
  n__s_A(x1) = max{6, 12 + x1}
  n__s#_A(x1) = max{0, 7}
  activate_A(x1) = max{3, 1 + x1}
  activate#_A(x1) = max{2, 13}
  geq_A(x1,x2) = max{3, 1, 2}
  geq#_A(x1,x2) = max{11, 9 + x1, 13}
  true_A = 3
  true#_A = 0
  false_A = 3
  false#_A = 1
  div_A(x1,x2) = max{15, 15 + x1, 2}
  div#_A(x1,x2) = max{10, x1, 8}
  s_A(x1) = max{13, 13 + x1}
  s#_A(x1) = max{8, -1}
  if_A(x1,x2,x3) = max{28, 16, 1 + x2, 28 + x3}
  if#_A(x1,x2,x3) = max{13, 13, 13, 13}

precedence:

  div = s > minus = n__s = geq = if > activate > 0 > n__0 > true = false