YES

Problem:
 minus_active(0(),y) -> 0()
 mark(0()) -> 0()
 minus_active(s(x),s(y)) -> minus_active(x,y)
 mark(s(x)) -> s(mark(x))
 ge_active(x,0()) -> true()
 mark(minus(x,y)) -> minus_active(x,y)
 ge_active(0(),s(y)) -> false()
 mark(ge(x,y)) -> ge_active(x,y)
 ge_active(s(x),s(y)) -> ge_active(x,y)
 mark(div(x,y)) -> div_active(mark(x),y)
 div_active(0(),s(y)) -> 0()
 mark(if(x,y,z)) -> if_active(mark(x),y,z)
 div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
 if_active(true(),x,y) -> mark(x)
 minus_active(x,y) -> minus(x,y)
 if_active(false(),x,y) -> mark(y)
 ge_active(x,y) -> ge(x,y)
 if_active(x,y,z) -> if(x,y,z)
 div_active(x,y) -> div(x,y)

Proof:
 DP Processor:
  DPs:
   minus_active#(s(x),s(y)) -> minus_active#(x,y)
   mark#(s(x)) -> mark#(x)
   mark#(minus(x,y)) -> minus_active#(x,y)
   mark#(ge(x,y)) -> ge_active#(x,y)
   ge_active#(s(x),s(y)) -> ge_active#(x,y)
   mark#(div(x,y)) -> mark#(x)
   mark#(div(x,y)) -> div_active#(mark(x),y)
   mark#(if(x,y,z)) -> mark#(x)
   mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
   div_active#(s(x),s(y)) -> ge_active#(x,y)
   div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
   if_active#(true(),x,y) -> mark#(x)
   if_active#(false(),x,y) -> mark#(y)
  TRS:
   minus_active(0(),y) -> 0()
   mark(0()) -> 0()
   minus_active(s(x),s(y)) -> minus_active(x,y)
   mark(s(x)) -> s(mark(x))
   ge_active(x,0()) -> true()
   mark(minus(x,y)) -> minus_active(x,y)
   ge_active(0(),s(y)) -> false()
   mark(ge(x,y)) -> ge_active(x,y)
   ge_active(s(x),s(y)) -> ge_active(x,y)
   mark(div(x,y)) -> div_active(mark(x),y)
   div_active(0(),s(y)) -> 0()
   mark(if(x,y,z)) -> if_active(mark(x),y,z)
   div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
   if_active(true(),x,y) -> mark(x)
   minus_active(x,y) -> minus(x,y)
   if_active(false(),x,y) -> mark(y)
   ge_active(x,y) -> ge(x,y)
   if_active(x,y,z) -> if(x,y,z)
   div_active(x,y) -> div(x,y)
  Matrix Interpretation Processor: dim=1
   
   usable rules:
    minus_active(0(),y) -> 0()
    mark(0()) -> 0()
    minus_active(s(x),s(y)) -> minus_active(x,y)
    mark(s(x)) -> s(mark(x))
    ge_active(x,0()) -> true()
    mark(minus(x,y)) -> minus_active(x,y)
    ge_active(0(),s(y)) -> false()
    mark(ge(x,y)) -> ge_active(x,y)
    ge_active(s(x),s(y)) -> ge_active(x,y)
    mark(div(x,y)) -> div_active(mark(x),y)
    div_active(0(),s(y)) -> 0()
    mark(if(x,y,z)) -> if_active(mark(x),y,z)
    div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
    if_active(true(),x,y) -> mark(x)
    minus_active(x,y) -> minus(x,y)
    if_active(false(),x,y) -> mark(y)
    ge_active(x,y) -> ge(x,y)
    if_active(x,y,z) -> if(x,y,z)
    div_active(x,y) -> div(x,y)
   interpretation:
    [if_active#](x0, x1, x2) = x0 + x1 + 2x2 + 1,
    
    [div_active#](x0, x1) = 2x0 + 1/2,
    
    [ge_active#](x0, x1) = 2x0,
    
    [mark#](x0) = x0 + 1/2,
    
    [minus_active#](x0, x1) = 1/2x0,
    
    [if_active](x0, x1, x2) = x0 + x1 + 5/2x2 + 3/2,
    
    [if](x0, x1, x2) = x0 + x1 + 5/2x2 + 3/2,
    
    [div_active](x0, x1) = 2x0 + 1/2,
    
    [div](x0, x1) = 2x0 + 1/2,
    
    [ge](x0, x1) = 2x0,
    
    [false] = 0,
    
    [minus](x0, x1) = 1/2x0,
    
    [true] = 0,
    
    [ge_active](x0, x1) = 2x0,
    
    [s](x0) = 2x0 + 2,
    
    [mark](x0) = x0,
    
    [minus_active](x0, x1) = 1/2x0,
    
    [0] = 0
   orientation:
    minus_active#(s(x),s(y)) = x + 1 >= 1/2x = minus_active#(x,y)
    
    mark#(s(x)) = 2x + 5/2 >= x + 1/2 = mark#(x)
    
    mark#(minus(x,y)) = 1/2x + 1/2 >= 1/2x = minus_active#(x,y)
    
    mark#(ge(x,y)) = 2x + 1/2 >= 2x = ge_active#(x,y)
    
    ge_active#(s(x),s(y)) = 4x + 4 >= 2x = ge_active#(x,y)
    
    mark#(div(x,y)) = 2x + 1 >= x + 1/2 = mark#(x)
    
    mark#(div(x,y)) = 2x + 1 >= 2x + 1/2 = div_active#(mark(x),y)
    
    mark#(if(x,y,z)) = x + y + 5/2z + 2 >= x + 1/2 = mark#(x)
    
    mark#(if(x,y,z)) = x + y + 5/2z + 2 >= x + y + 2z + 1 = if_active#(mark(x),y,z)
    
    div_active#(s(x),s(y)) = 4x + 9/2 >= 2x = ge_active#(x,y)
    
    div_active#(s(x),s(y)) = 4x + 9/2 >= 4x + 4 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
    
    if_active#(true(),x,y) = x + 2y + 1 >= x + 1/2 = mark#(x)
    
    if_active#(false(),x,y) = x + 2y + 1 >= y + 1/2 = mark#(y)
    
    minus_active(0(),y) = 0 >= 0 = 0()
    
    mark(0()) = 0 >= 0 = 0()
    
    minus_active(s(x),s(y)) = x + 1 >= 1/2x = minus_active(x,y)
    
    mark(s(x)) = 2x + 2 >= 2x + 2 = s(mark(x))
    
    ge_active(x,0()) = 2x >= 0 = true()
    
    mark(minus(x,y)) = 1/2x >= 1/2x = minus_active(x,y)
    
    ge_active(0(),s(y)) = 0 >= 0 = false()
    
    mark(ge(x,y)) = 2x >= 2x = ge_active(x,y)
    
    ge_active(s(x),s(y)) = 4x + 4 >= 2x = ge_active(x,y)
    
    mark(div(x,y)) = 2x + 1/2 >= 2x + 1/2 = div_active(mark(x),y)
    
    div_active(0(),s(y)) = 1/2 >= 0 = 0()
    
    mark(if(x,y,z)) = x + y + 5/2z + 3/2 >= x + y + 5/2z + 3/2 = if_active(mark(x),y,z)
    
    div_active(s(x),s(y)) = 4x + 9/2 >= 4x + 9/2 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
    
    if_active(true(),x,y) = x + 5/2y + 3/2 >= x = mark(x)
    
    minus_active(x,y) = 1/2x >= 1/2x = minus(x,y)
    
    if_active(false(),x,y) = x + 5/2y + 3/2 >= y = mark(y)
    
    ge_active(x,y) = 2x >= 2x = ge(x,y)
    
    if_active(x,y,z) = x + y + 5/2z + 3/2 >= x + y + 5/2z + 3/2 = if(x,y,z)
    
    div_active(x,y) = 2x + 1/2 >= 2x + 1/2 = div(x,y)
   problem:
    DPs:
     
    TRS:
     minus_active(0(),y) -> 0()
     mark(0()) -> 0()
     minus_active(s(x),s(y)) -> minus_active(x,y)
     mark(s(x)) -> s(mark(x))
     ge_active(x,0()) -> true()
     mark(minus(x,y)) -> minus_active(x,y)
     ge_active(0(),s(y)) -> false()
     mark(ge(x,y)) -> ge_active(x,y)
     ge_active(s(x),s(y)) -> ge_active(x,y)
     mark(div(x,y)) -> div_active(mark(x),y)
     div_active(0(),s(y)) -> 0()
     mark(if(x,y,z)) -> if_active(mark(x),y,z)
     div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
     if_active(true(),x,y) -> mark(x)
     minus_active(x,y) -> minus(x,y)
     if_active(false(),x,y) -> mark(y)
     ge_active(x,y) -> ge(x,y)
     if_active(x,y,z) -> if(x,y,z)
     div_active(x,y) -> div(x,y)
   Qed