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)
  TDG 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)
   graph:
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(if(x,y,z)) -> mark#(x)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(div(x,y)) -> div_active#(mark(x),y)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(div(x,y)) -> mark#(x)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(ge(x,y)) -> ge_active#(x,y)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(minus(x,y)) -> minus_active#(x,y)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(s(x)) -> mark#(x)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(if(x,y,z)) -> mark#(x)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(div(x,y)) -> div_active#(mark(x),y)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(div(x,y)) -> mark#(x)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(ge(x,y)) -> ge_active#(x,y)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(minus(x,y)) -> minus_active#(x,y)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(s(x)) -> mark#(x)
    div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ->
    if_active#(false(),x,y) -> mark#(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)
    div_active#(s(x),s(y)) -> ge_active#(x,y) ->
    ge_active#(s(x),s(y)) -> ge_active#(x,y)
    ge_active#(s(x),s(y)) -> ge_active#(x,y) ->
    ge_active#(s(x),s(y)) -> ge_active#(x,y)
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z) ->
    if_active#(false(),x,y) -> mark#(y)
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z) ->
    if_active#(true(),x,y) -> mark#(x)
    mark#(if(x,y,z)) -> mark#(x) ->
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    mark#(if(x,y,z)) -> mark#(x) -> mark#(if(x,y,z)) -> mark#(x)
    mark#(if(x,y,z)) -> mark#(x) ->
    mark#(div(x,y)) -> div_active#(mark(x),y)
    mark#(if(x,y,z)) -> mark#(x) -> mark#(div(x,y)) -> mark#(x)
    mark#(if(x,y,z)) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y)
    mark#(if(x,y,z)) -> mark#(x) ->
    mark#(minus(x,y)) -> minus_active#(x,y)
    mark#(if(x,y,z)) -> mark#(x) ->
    mark#(s(x)) -> mark#(x)
    mark#(div(x,y)) -> div_active#(mark(x),y) ->
    div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
    mark#(div(x,y)) -> div_active#(mark(x),y) ->
    div_active#(s(x),s(y)) -> ge_active#(x,y)
    mark#(div(x,y)) -> mark#(x) ->
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    mark#(div(x,y)) -> mark#(x) -> mark#(if(x,y,z)) -> mark#(x)
    mark#(div(x,y)) -> mark#(x) ->
    mark#(div(x,y)) -> div_active#(mark(x),y)
    mark#(div(x,y)) -> mark#(x) -> mark#(div(x,y)) -> mark#(x)
    mark#(div(x,y)) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y)
    mark#(div(x,y)) -> mark#(x) ->
    mark#(minus(x,y)) -> minus_active#(x,y)
    mark#(div(x,y)) -> mark#(x) -> mark#(s(x)) -> mark#(x)
    mark#(ge(x,y)) -> ge_active#(x,y) ->
    ge_active#(s(x),s(y)) -> ge_active#(x,y)
    mark#(minus(x,y)) -> minus_active#(x,y) ->
    minus_active#(s(x),s(y)) -> minus_active#(x,y)
    mark#(s(x)) -> mark#(x) -> mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    mark#(s(x)) -> mark#(x) -> mark#(if(x,y,z)) -> mark#(x)
    mark#(s(x)) -> mark#(x) -> mark#(div(x,y)) -> div_active#(mark(x),y)
    mark#(s(x)) -> mark#(x) -> mark#(div(x,y)) -> mark#(x)
    mark#(s(x)) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y)
    mark#(s(x)) -> mark#(x) -> mark#(minus(x,y)) -> minus_active#(x,y)
    mark#(s(x)) -> mark#(x) ->
    mark#(s(x)) -> mark#(x)
    minus_active#(s(x),s(y)) -> minus_active#(x,y) ->
    minus_active#(s(x),s(y)) -> minus_active#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 10
    #arcs: 46/169
    DPs:
     if_active#(false(),x,y) -> mark#(y)
     mark#(s(x)) -> mark#(x)
     mark#(div(x,y)) -> mark#(x)
     mark#(div(x,y)) -> div_active#(mark(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)
     mark#(if(x,y,z)) -> mark#(x)
     mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    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
     
     interpretation:
      [if_active#](x0, x1, x2) = 2x1 + 4x2 + 2,
      
      [div_active#](x0, x1) = 4x0 + 2x1 + 1,
      
      [mark#](x0) = 2x0,
      
      [if_active](x0, x1, x2) = 4x0 + x1 + 3x2 + 2,
      
      [if](x0, x1, x2) = 4x0 + x1 + 3x2 + 2,
      
      [div_active](x0, x1) = 2x0 + x1 + 1,
      
      [div](x0, x1) = 2x0 + x1 + 1,
      
      [ge](x0, x1) = 0,
      
      [false] = 0,
      
      [minus](x0, x1) = x0,
      
      [true] = 0,
      
      [ge_active](x0, x1) = 0,
      
      [s](x0) = x0 + 2,
      
      [mark](x0) = x0,
      
      [minus_active](x0, x1) = x0,
      
      [0] = 0
     orientation:
      if_active#(false(),x,y) = 2x + 4y + 2 >= 2y = mark#(y)
      
      mark#(s(x)) = 2x + 4 >= 2x = mark#(x)
      
      mark#(div(x,y)) = 4x + 2y + 2 >= 2x = mark#(x)
      
      mark#(div(x,y)) = 4x + 2y + 2 >= 4x + 2y + 1 = div_active#(mark(x),y)
      
      div_active#(s(x),s(y)) = 4x + 2y + 13 >= 4x + 2y + 12 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      
      if_active#(true(),x,y) = 2x + 4y + 2 >= 2x = mark#(x)
      
      mark#(if(x,y,z)) = 8x + 2y + 6z + 4 >= 2x = mark#(x)
      
      mark#(if(x,y,z)) = 8x + 2y + 6z + 4 >= 2y + 4z + 2 = if_active#(mark(x),y,z)
      
      minus_active(0(),y) = 0 >= 0 = 0()
      
      mark(0()) = 0 >= 0 = 0()
      
      minus_active(s(x),s(y)) = x + 2 >= x = minus_active(x,y)
      
      mark(s(x)) = x + 2 >= x + 2 = s(mark(x))
      
      ge_active(x,0()) = 0 >= 0 = true()
      
      mark(minus(x,y)) = x >= x = minus_active(x,y)
      
      ge_active(0(),s(y)) = 0 >= 0 = false()
      
      mark(ge(x,y)) = 0 >= 0 = ge_active(x,y)
      
      ge_active(s(x),s(y)) = 0 >= 0 = ge_active(x,y)
      
      mark(div(x,y)) = 2x + y + 1 >= 2x + y + 1 = div_active(mark(x),y)
      
      div_active(0(),s(y)) = y + 3 >= 0 = 0()
      
      mark(if(x,y,z)) = 4x + y + 3z + 2 >= 4x + y + 3z + 2 = if_active(mark(x),y,z)
      
      div_active(s(x),s(y)) = 2x + y + 7 >= 2x + y + 7 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      
      if_active(true(),x,y) = x + 3y + 2 >= x = mark(x)
      
      minus_active(x,y) = x >= x = minus(x,y)
      
      if_active(false(),x,y) = x + 3y + 2 >= y = mark(y)
      
      ge_active(x,y) = 0 >= 0 = ge(x,y)
      
      if_active(x,y,z) = 4x + y + 3z + 2 >= 4x + y + 3z + 2 = if(x,y,z)
      
      div_active(x,y) = 2x + y + 1 >= 2x + y + 1 = 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
    
    DPs:
     ge_active#(s(x),s(y)) -> ge_active#(x,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
     
     interpretation:
      [ge_active#](x0, x1) = 5x0 + 6,
      
      [if_active](x0, x1, x2) = 6x1 + 4x2,
      
      [if](x0, x1, x2) = 6x1 + 4x2,
      
      [div_active](x0, x1) = 6x0,
      
      [div](x0, x1) = 6x0,
      
      [ge](x0, x1) = 0,
      
      [false] = 0,
      
      [minus](x0, x1) = 0,
      
      [true] = 0,
      
      [ge_active](x0, x1) = 0,
      
      [s](x0) = 4x0 + 5,
      
      [mark](x0) = x0,
      
      [minus_active](x0, x1) = 0,
      
      [0] = 0
     orientation:
      ge_active#(s(x),s(y)) = 20x + 31 >= 5x + 6 = ge_active#(x,y)
      
      minus_active(0(),y) = 0 >= 0 = 0()
      
      mark(0()) = 0 >= 0 = 0()
      
      minus_active(s(x),s(y)) = 0 >= 0 = minus_active(x,y)
      
      mark(s(x)) = 4x + 5 >= 4x + 5 = s(mark(x))
      
      ge_active(x,0()) = 0 >= 0 = true()
      
      mark(minus(x,y)) = 0 >= 0 = minus_active(x,y)
      
      ge_active(0(),s(y)) = 0 >= 0 = false()
      
      mark(ge(x,y)) = 0 >= 0 = ge_active(x,y)
      
      ge_active(s(x),s(y)) = 0 >= 0 = ge_active(x,y)
      
      mark(div(x,y)) = 6x >= 6x = div_active(mark(x),y)
      
      div_active(0(),s(y)) = 0 >= 0 = 0()
      
      mark(if(x,y,z)) = 6y + 4z >= 6y + 4z = if_active(mark(x),y,z)
      
      div_active(s(x),s(y)) = 24x + 30 >= 30 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      
      if_active(true(),x,y) = 6x + 4y >= x = mark(x)
      
      minus_active(x,y) = 0 >= 0 = minus(x,y)
      
      if_active(false(),x,y) = 6x + 4y >= y = mark(y)
      
      ge_active(x,y) = 0 >= 0 = ge(x,y)
      
      if_active(x,y,z) = 6y + 4z >= 6y + 4z = if(x,y,z)
      
      div_active(x,y) = 6x >= 6x = 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
    
    DPs:
     minus_active#(s(x),s(y)) -> minus_active#(x,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
     
     interpretation:
      [minus_active#](x0, x1) = 5x0 + 6,
      
      [if_active](x0, x1, x2) = 6x1 + 4x2,
      
      [if](x0, x1, x2) = 6x1 + 4x2,
      
      [div_active](x0, x1) = 6x0,
      
      [div](x0, x1) = 6x0,
      
      [ge](x0, x1) = 0,
      
      [false] = 0,
      
      [minus](x0, x1) = 0,
      
      [true] = 0,
      
      [ge_active](x0, x1) = 0,
      
      [s](x0) = 4x0 + 5,
      
      [mark](x0) = x0,
      
      [minus_active](x0, x1) = 0,
      
      [0] = 0
     orientation:
      minus_active#(s(x),s(y)) = 20x + 31 >= 5x + 6 = minus_active#(x,y)
      
      minus_active(0(),y) = 0 >= 0 = 0()
      
      mark(0()) = 0 >= 0 = 0()
      
      minus_active(s(x),s(y)) = 0 >= 0 = minus_active(x,y)
      
      mark(s(x)) = 4x + 5 >= 4x + 5 = s(mark(x))
      
      ge_active(x,0()) = 0 >= 0 = true()
      
      mark(minus(x,y)) = 0 >= 0 = minus_active(x,y)
      
      ge_active(0(),s(y)) = 0 >= 0 = false()
      
      mark(ge(x,y)) = 0 >= 0 = ge_active(x,y)
      
      ge_active(s(x),s(y)) = 0 >= 0 = ge_active(x,y)
      
      mark(div(x,y)) = 6x >= 6x = div_active(mark(x),y)
      
      div_active(0(),s(y)) = 0 >= 0 = 0()
      
      mark(if(x,y,z)) = 6y + 4z >= 6y + 4z = if_active(mark(x),y,z)
      
      div_active(s(x),s(y)) = 24x + 30 >= 30 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      
      if_active(true(),x,y) = 6x + 4y >= x = mark(x)
      
      minus_active(x,y) = 0 >= 0 = minus(x,y)
      
      if_active(false(),x,y) = 6x + 4y >= y = mark(y)
      
      ge_active(x,y) = 0 >= 0 = ge(x,y)
      
      if_active(x,y,z) = 6y + 4z >= 6y + 4z = if(x,y,z)
      
      div_active(x,y) = 6x >= 6x = 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