YES

TRS:

  a__minus(0(),Y) -> 0()
  a__minus(s(X),s(Y)) -> a__minus(X,Y)
  a__geq(X,0()) -> true()
  a__geq(0(),s(Y)) -> false()
  a__geq(s(X),s(Y)) -> a__geq(X,Y)
  a__div(0(),s(Y)) -> 0()
  a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
  a__if(true(),X,Y) -> mark(X)
  a__if(false(),X,Y) -> mark(Y)
  mark(minus(X1,X2)) -> a__minus(X1,X2)
  mark(geq(X1,X2)) -> a__geq(X1,X2)
  mark(div(X1,X2)) -> a__div(mark(X1),X2)
  mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
  mark(0()) -> 0()
  mark(s(X)) -> s(mark(X))
  mark(true()) -> true()
  mark(false()) -> false()
  a__minus(X1,X2) -> minus(X1,X2)
  a__geq(X1,X2) -> geq(X1,X2)
  a__div(X1,X2) -> div(X1,X2)
  a__if(X1,X2,X3) -> if(X1,X2,X3)

max/plus interpretations on N:

  a__minus_A(x1,x2) = max{6, -22 + x1, -22}
  a__minus#_A(x1,x2) = max{0, -2 + x1, -4}
  0_A = 1
  0#_A = 89
  s_A(x1) = max{59, 3 + x1}
  s#_A(x1) = max{28, 29}
  a__geq_A(x1,x2) = max{13, -2, 6}
  a__geq#_A(x1,x2) = max{91, 29, 31}
  true_A = 7
  true#_A = 40
  false_A = 7
  false#_A = 30
  a__div_A(x1,x2) = max{41, 50 + x1, 63}
  a__div#_A(x1,x2) = max{90, 62 + x1, 59}
  a__if_A(x1,x2,x3) = max{64, 48 + x1, 35 + x2, 62 + x3}
  a__if#_A(x1,x2,x3) = max{93, 95, 35 + x2, 57 + x3}
  div_A(x1,x2) = max{42, 50 + x1, 26}
  div#_A(x1,x2) = max{90, 33, 90}
  minus_A(x1,x2) = max{1, -35 + x1, -22}
  minus#_A(x1,x2) = max{0, -5, -3}
  mark_A(x1) = max{6, 13 + x1}
  mark#_A(x1) = max{92, 34 + x1}
  geq_A(x1,x2) = max{0, -1, -2}
  geq#_A(x1,x2) = max{0, 0, 30}
  if_A(x1,x2,x3) = max{47, 48 + x1, 22 + x2, 62 + x3}
  if#_A(x1,x2,x3) = max{33, 94, 58, 94}

precedence:

  a__if > mark > a__minus = a__div = if > 0 = div = minus > s = true > a__geq > false = geq