YES

Problem:
 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)

Proof:
 DP Processor:
  DPs:
   a__minus#(s(X),s(Y)) -> a__minus#(X,Y)
   a__geq#(s(X),s(Y)) -> a__geq#(X,Y)
   a__div#(s(X),s(Y)) -> a__geq#(X,Y)
   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)) -> mark#(X1)
   mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
   mark#(if(X1,X2,X3)) -> mark#(X1)
   mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
   mark#(s(X)) -> mark#(X)
  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)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [mark#](x0) = 2x0 + 1/2,
    
    [a__if#](x0, x1, x2) = 2x0 + 2x1 + 2x2,
    
    [a__div#](x0, x1) = 7/2x0 + 1,
    
    [a__geq#](x0, x1) = x0 + 3,
    
    [a__minus#](x0, x1) = x0,
    
    [if](x0, x1, x2) = x0 + x1 + 2x2 + 2,
    
    [geq](x0, x1) = 1/2x0 + 3/2,
    
    [mark](x0) = x0,
    
    [a__if](x0, x1, x2) = x0 + x1 + 2x2 + 2,
    
    [div](x0, x1) = 3x0 + 1/2,
    
    [minus](x0, x1) = 1/2x0,
    
    [a__div](x0, x1) = 3x0 + 1/2,
    
    [false] = 1,
    
    [true] = 3/2,
    
    [a__geq](x0, x1) = 1/2x0 + 3/2,
    
    [s](x0) = 2x0 + 3,
    
    [a__minus](x0, x1) = 1/2x0,
    
    [0] = 0
   orientation:
    a__minus#(s(X),s(Y)) = 2X + 3 >= X = a__minus#(X,Y)
    
    a__geq#(s(X),s(Y)) = 2X + 6 >= X + 3 = a__geq#(X,Y)
    
    a__div#(s(X),s(Y)) = 7X + 23/2 >= X + 3 = a__geq#(X,Y)
    
    a__div#(s(X),s(Y)) = 7X + 23/2 >= 7X + 11 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    
    a__if#(true(),X,Y) = 2X + 2Y + 3 >= 2X + 1/2 = mark#(X)
    
    a__if#(false(),X,Y) = 2X + 2Y + 2 >= 2Y + 1/2 = mark#(Y)
    
    mark#(minus(X1,X2)) = X1 + 1/2 >= X1 = a__minus#(X1,X2)
    
    mark#(geq(X1,X2)) = X1 + 7/2 >= X1 + 3 = a__geq#(X1,X2)
    
    mark#(div(X1,X2)) = 6X1 + 3/2 >= 2X1 + 1/2 = mark#(X1)
    
    mark#(div(X1,X2)) = 6X1 + 3/2 >= 7/2X1 + 1 = a__div#(mark(X1),X2)
    
    mark#(if(X1,X2,X3)) = 2X1 + 2X2 + 4X3 + 9/2 >= 2X1 + 1/2 = mark#(X1)
    
    mark#(if(X1,X2,X3)) = 2X1 + 2X2 + 4X3 + 9/2 >= 2X1 + 2X2 + 2X3 = a__if#(mark(X1),X2,X3)
    
    mark#(s(X)) = 4X + 13/2 >= 2X + 1/2 = mark#(X)
    
    a__minus(0(),Y) = 0 >= 0 = 0()
    
    a__minus(s(X),s(Y)) = X + 3/2 >= 1/2X = a__minus(X,Y)
    
    a__geq(X,0()) = 1/2X + 3/2 >= 3/2 = true()
    
    a__geq(0(),s(Y)) = 3/2 >= 1 = false()
    
    a__geq(s(X),s(Y)) = X + 3 >= 1/2X + 3/2 = a__geq(X,Y)
    
    a__div(0(),s(Y)) = 1/2 >= 0 = 0()
    
    a__div(s(X),s(Y)) = 6X + 19/2 >= 7/2X + 15/2 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    
    a__if(true(),X,Y) = X + 2Y + 7/2 >= X = mark(X)
    
    a__if(false(),X,Y) = X + 2Y + 3 >= Y = mark(Y)
    
    mark(minus(X1,X2)) = 1/2X1 >= 1/2X1 = a__minus(X1,X2)
    
    mark(geq(X1,X2)) = 1/2X1 + 3/2 >= 1/2X1 + 3/2 = a__geq(X1,X2)
    
    mark(div(X1,X2)) = 3X1 + 1/2 >= 3X1 + 1/2 = a__div(mark(X1),X2)
    
    mark(if(X1,X2,X3)) = X1 + X2 + 2X3 + 2 >= X1 + X2 + 2X3 + 2 = a__if(mark(X1),X2,X3)
    
    mark(0()) = 0 >= 0 = 0()
    
    mark(s(X)) = 2X + 3 >= 2X + 3 = s(mark(X))
    
    mark(true()) = 3/2 >= 3/2 = true()
    
    mark(false()) = 1 >= 1 = false()
    
    a__minus(X1,X2) = 1/2X1 >= 1/2X1 = minus(X1,X2)
    
    a__geq(X1,X2) = 1/2X1 + 3/2 >= 1/2X1 + 3/2 = geq(X1,X2)
    
    a__div(X1,X2) = 3X1 + 1/2 >= 3X1 + 1/2 = div(X1,X2)
    
    a__if(X1,X2,X3) = X1 + X2 + 2X3 + 2 >= X1 + X2 + 2X3 + 2 = if(X1,X2,X3)
   problem:
    DPs:
     
    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)
   Qed