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)
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [if_active#](x0, x1, x2) = x0 + x1 + 6x2 + 0,
      
      [div_active#](x0, x1) = x0 + 6x1 + 0,
      
      [mark#](x0) = x0,
      
      [if_active](x0, x1, x2) = x0 + x1 + 6x2 + 0,
      
      [if](x0, x1, x2) = x0 + x1 + 6x2 + 0,
      
      [div_active](x0, x1) = x0 + 6x1 + 0,
      
      [div](x0, x1) = x0 + 6x1 + 0,
      
      [ge](x0, x1) = x0 + x1 + 1,
      
      [false] = 0,
      
      [minus](x0, x1) = x0 + x1 + 0,
      
      [true] = 0,
      
      [ge_active](x0, x1) = x0 + x1 + 1,
      
      [s](x0) = x0 + 0,
      
      [mark](x0) = x0 + 0,
      
      [minus_active](x0, x1) = x0 + x1 + 0,
      
      [0] = 0
     orientation:
      if_active#(false(),x,y) = x + 6y + 0 >= y = mark#(y)
      
      mark#(s(x)) = x + 0 >= x = mark#(x)
      
      mark#(div(x,y)) = x + 6y + 0 >= x = mark#(x)
      
      mark#(div(x,y)) = x + 6y + 0 >= x + 6y + 0 = div_active#(mark(x),y)
      
      div_active#(s(x),s(y)) = x + 6y + 6 >= x + 6y + 6 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      
      if_active#(true(),x,y) = x + 6y + 0 >= x = mark#(x)
      
      mark#(if(x,y,z)) = x + y + 6z + 0 >= x = mark#(x)
      
      mark#(if(x,y,z)) = x + y + 6z + 0 >= x + y + 6z + 0 = if_active#(mark(x),y,z)
      
      minus_active(0(),y) = y + 0 >= 0 = 0()
      
      mark(0()) = 0 >= 0 = 0()
      
      minus_active(s(x),s(y)) = x + y + 0 >= x + y + 0 = minus_active(x,y)
      
      mark(s(x)) = x + 0 >= x + 0 = s(mark(x))
      
      ge_active(x,0()) = x + 1 >= 0 = true()
      
      mark(minus(x,y)) = x + y + 0 >= x + y + 0 = minus_active(x,y)
      
      ge_active(0(),s(y)) = y + 1 >= 0 = false()
      
      mark(ge(x,y)) = x + y + 1 >= x + y + 1 = ge_active(x,y)
      
      ge_active(s(x),s(y)) = x + y + 1 >= x + y + 1 = ge_active(x,y)
      
      mark(div(x,y)) = x + 6y + 0 >= x + 6y + 0 = div_active(mark(x),y)
      
      div_active(0(),s(y)) = 6y + 6 >= 0 = 0()
      
      mark(if(x,y,z)) = x + y + 6z + 0 >= x + y + 6z + 0 = if_active(mark(x),y,z)
      
      div_active(s(x),s(y)) = x + 6y + 6 >= x + 6y + 6 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      
      if_active(true(),x,y) = x + 6y + 0 >= x + 0 = mark(x)
      
      minus_active(x,y) = x + y + 0 >= x + y + 0 = minus(x,y)
      
      if_active(false(),x,y) = x + 6y + 0 >= y + 0 = mark(y)
      
      ge_active(x,y) = x + y + 1 >= x + y + 1 = ge(x,y)
      
      if_active(x,y,z) = x + y + 6z + 0 >= x + y + 6z + 0 = if(x,y,z)
      
      div_active(x,y) = x + 6y + 0 >= x + 6y + 0 = div(x,y)
     problem:
      DPs:
       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)
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [if_active#](x0, x1, x2) = x0 + x1 + 0,
       
       [div_active#](x0, x1) = x0 + 1x1 + 0,
       
       [mark#](x0) = x0 + 0,
       
       [if_active](x0, x1, x2) = x0 + x1 + x2 + 0,
       
       [if](x0, x1, x2) = x0 + x1 + x2 + 0,
       
       [div_active](x0, x1) = 1x0 + 1x1 + 1,
       
       [div](x0, x1) = 1x0 + 1x1 + 1,
       
       [ge](x0, x1) = x0 + 0,
       
       [false] = 0,
       
       [minus](x0, x1) = 0,
       
       [true] = 0,
       
       [ge_active](x0, x1) = x0 + 0,
       
       [s](x0) = x0 + 0,
       
       [mark](x0) = x0 + 0,
       
       [minus_active](x0, x1) = 0,
       
       [0] = 0
      orientation:
       mark#(s(x)) = x + 0 >= x + 0 = mark#(x)
       
       mark#(div(x,y)) = 1x + 1y + 1 >= x + 0 = mark#(x)
       
       mark#(div(x,y)) = 1x + 1y + 1 >= x + 1y + 0 = div_active#(mark(x),y)
       
       div_active#(s(x),s(y)) = x + 1y + 1 >= x + 1y + 1 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
       
       if_active#(true(),x,y) = x + 0 >= x + 0 = mark#(x)
       
       mark#(if(x,y,z)) = x + y + z + 0 >= x + 0 = mark#(x)
       
       mark#(if(x,y,z)) = x + y + z + 0 >= x + y + 0 = if_active#(mark(x),y,z)
       
       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)) = x + 0 >= x + 0 = s(mark(x))
       
       ge_active(x,0()) = x + 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)) = x + 0 >= x + 0 = ge_active(x,y)
       
       ge_active(s(x),s(y)) = x + 0 >= x + 0 = ge_active(x,y)
       
       mark(div(x,y)) = 1x + 1y + 1 >= 1x + 1y + 1 = div_active(mark(x),y)
       
       div_active(0(),s(y)) = 1y + 1 >= 0 = 0()
       
       mark(if(x,y,z)) = x + y + z + 0 >= x + y + z + 0 = if_active(mark(x),y,z)
       
       div_active(s(x),s(y)) = 1x + 1y + 1 >= x + 1y + 1 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
       
       if_active(true(),x,y) = x + y + 0 >= x + 0 = mark(x)
       
       minus_active(x,y) = 0 >= 0 = minus(x,y)
       
       if_active(false(),x,y) = x + y + 0 >= y + 0 = mark(y)
       
       ge_active(x,y) = x + 0 >= x + 0 = ge(x,y)
       
       if_active(x,y,z) = x + y + z + 0 >= x + y + z + 0 = if(x,y,z)
       
       div_active(x,y) = 1x + 1y + 1 >= 1x + 1y + 1 = div(x,y)
      problem:
       DPs:
        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())
        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)
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [if_active#](x0, x1, x2) = 2x0 + x1 + 6x2 + 0,
        
        [div_active#](x0, x1) = x0 + 6x1 + 0,
        
        [mark#](x0) = x0 + 0,
        
        [if_active](x0, x1, x2) = 2x0 + x1 + 6x2 + 2,
        
        [if](x0, x1, x2) = 2x0 + x1 + 6x2 + 2,
        
        [div_active](x0, x1) = x0 + 6x1 + 0,
        
        [div](x0, x1) = x0 + 6x1 + 0,
        
        [ge](x0, x1) = 2,
        
        [false] = 0,
        
        [minus](x0, x1) = x0 + x1,
        
        [true] = 0,
        
        [ge_active](x0, x1) = 2,
        
        [s](x0) = x0 + 0,
        
        [mark](x0) = x0 + 0,
        
        [minus_active](x0, x1) = x0 + x1,
        
        [0] = 0
       orientation:
        mark#(s(x)) = x + 0 >= x + 0 = mark#(x)
        
        mark#(div(x,y)) = x + 6y + 0 >= x + 6y + 0 = div_active#(mark(x),y)
        
        div_active#(s(x),s(y)) = x + 6y + 6 >= x + 6y + 6 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
        
        if_active#(true(),x,y) = x + 6y + 2 >= x + 0 = mark#(x)
        
        mark#(if(x,y,z)) = 2x + y + 6z + 2 >= x + 0 = mark#(x)
        
        mark#(if(x,y,z)) = 2x + y + 6z + 2 >= 2x + y + 6z + 2 = if_active#(mark(x),y,z)
        
        minus_active(0(),y) = y + 0 >= 0 = 0()
        
        mark(0()) = 0 >= 0 = 0()
        
        minus_active(s(x),s(y)) = x + y + 0 >= x + y = minus_active(x,y)
        
        mark(s(x)) = x + 0 >= x + 0 = s(mark(x))
        
        ge_active(x,0()) = 2 >= 0 = true()
        
        mark(minus(x,y)) = x + y + 0 >= x + y = minus_active(x,y)
        
        ge_active(0(),s(y)) = 2 >= 0 = false()
        
        mark(ge(x,y)) = 2 >= 2 = ge_active(x,y)
        
        ge_active(s(x),s(y)) = 2 >= 2 = ge_active(x,y)
        
        mark(div(x,y)) = x + 6y + 0 >= x + 6y + 0 = div_active(mark(x),y)
        
        div_active(0(),s(y)) = 6y + 6 >= 0 = 0()
        
        mark(if(x,y,z)) = 2x + y + 6z + 2 >= 2x + y + 6z + 2 = if_active(mark(x),y,z)
        
        div_active(s(x),s(y)) = x + 6y + 6 >= x + 6y + 6 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
        
        if_active(true(),x,y) = x + 6y + 2 >= x + 0 = mark(x)
        
        minus_active(x,y) = x + y >= x + y = minus(x,y)
        
        if_active(false(),x,y) = x + 6y + 2 >= y + 0 = mark(y)
        
        ge_active(x,y) = 2 >= 2 = ge(x,y)
        
        if_active(x,y,z) = 2x + y + 6z + 2 >= 2x + y + 6z + 2 = if(x,y,z)
        
        div_active(x,y) = x + 6y + 0 >= x + 6y + 0 = div(x,y)
       problem:
        DPs:
         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())
         if_active#(true(),x,y) -> 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)
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [if_active#](x0, x1, x2) = x1 + 5x2,
         
         [div_active#](x0, x1) = 4x1 + 0,
         
         [mark#](x0) = x0,
         
         [if_active](x0, x1, x2) = 1x0 + 1x1 + 6x2 + 0,
         
         [if](x0, x1, x2) = 1x0 + 1x1 + 6x2 + 0,
         
         [div_active](x0, x1) = x0 + 5x1 + 1,
         
         [div](x0, x1) = x0 + 4x1 + 0,
         
         [ge](x0, x1) = 2,
         
         [false] = 0,
         
         [minus](x0, x1) = 1x1 + 0,
         
         [true] = 0,
         
         [ge_active](x0, x1) = 3,
         
         [s](x0) = x0 + 1,
         
         [mark](x0) = 1x0 + 0,
         
         [minus_active](x0, x1) = 2x1 + 0,
         
         [0] = 0
        orientation:
         mark#(s(x)) = x + 1 >= x = mark#(x)
         
         mark#(div(x,y)) = x + 4y + 0 >= 4y + 0 = div_active#(mark(x),y)
         
         div_active#(s(x),s(y)) = 4y + 5 >= 4y + 5 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
         
         if_active#(true(),x,y) = x + 5y >= x = mark#(x)
         
         mark#(if(x,y,z)) = 1x + 1y + 6z + 0 >= y + 5z = if_active#(mark(x),y,z)
         
         minus_active(0(),y) = 2y + 0 >= 0 = 0()
         
         mark(0()) = 1 >= 0 = 0()
         
         minus_active(s(x),s(y)) = 2y + 3 >= 2y + 0 = minus_active(x,y)
         
         mark(s(x)) = 1x + 2 >= 1x + 1 = s(mark(x))
         
         ge_active(x,0()) = 3 >= 0 = true()
         
         mark(minus(x,y)) = 2y + 1 >= 2y + 0 = minus_active(x,y)
         
         ge_active(0(),s(y)) = 3 >= 0 = false()
         
         mark(ge(x,y)) = 3 >= 3 = ge_active(x,y)
         
         ge_active(s(x),s(y)) = 3 >= 3 = ge_active(x,y)
         
         mark(div(x,y)) = 1x + 5y + 1 >= 1x + 5y + 1 = div_active(mark(x),y)
         
         div_active(0(),s(y)) = 5y + 6 >= 0 = 0()
         
         mark(if(x,y,z)) = 2x + 2y + 7z + 1 >= 2x + 1y + 6z + 1 = if_active(mark(x),y,z)
         
         div_active(s(x),s(y)) = x + 5y + 6 >= 5y + 6 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
         
         if_active(true(),x,y) = 1x + 6y + 1 >= 1x + 0 = mark(x)
         
         minus_active(x,y) = 2y + 0 >= 1y + 0 = minus(x,y)
         
         if_active(false(),x,y) = 1x + 6y + 1 >= 1y + 0 = mark(y)
         
         ge_active(x,y) = 3 >= 2 = ge(x,y)
         
         if_active(x,y,z) = 1x + 1y + 6z + 0 >= 1x + 1y + 6z + 0 = if(x,y,z)
         
         div_active(x,y) = x + 5y + 1 >= x + 4y + 0 = div(x,y)
        problem:
         DPs:
          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())
          if_active#(true(),x,y) -> mark#(x)
         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)
        Arctic Interpretation Processor:
         dimension: 1
         interpretation:
          [if_active#](x0, x1, x2) = x0 + x1 + x2 + 0,
          
          [div_active#](x0, x1) = x0,
          
          [mark#](x0) = x0,
          
          [if_active](x0, x1, x2) = x0 + x1 + x2 + 0,
          
          [if](x0, x1, x2) = x0 + x1 + x2 + 0,
          
          [div_active](x0, x1) = x0,
          
          [div](x0, x1) = x0,
          
          [ge](x0, x1) = x0 + 0,
          
          [false] = 0,
          
          [minus](x0, x1) = x0,
          
          [true] = 0,
          
          [ge_active](x0, x1) = x0 + 0,
          
          [s](x0) = 1x0 + 0,
          
          [mark](x0) = x0,
          
          [minus_active](x0, x1) = x0,
          
          [0] = 0
         orientation:
          mark#(s(x)) = 1x + 0 >= x = mark#(x)
          
          mark#(div(x,y)) = x >= x = div_active#(mark(x),y)
          
          div_active#(s(x),s(y)) = 1x + 0 >= 1x + 0 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
          
          if_active#(true(),x,y) = x + y + 0 >= x = mark#(x)
          
          minus_active(0(),y) = 0 >= 0 = 0()
          
          mark(0()) = 0 >= 0 = 0()
          
          minus_active(s(x),s(y)) = 1x + 0 >= x = minus_active(x,y)
          
          mark(s(x)) = 1x + 0 >= 1x + 0 = s(mark(x))
          
          ge_active(x,0()) = x + 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)) = x + 0 >= x + 0 = ge_active(x,y)
          
          ge_active(s(x),s(y)) = 1x + 0 >= x + 0 = ge_active(x,y)
          
          mark(div(x,y)) = x >= x = div_active(mark(x),y)
          
          div_active(0(),s(y)) = 0 >= 0 = 0()
          
          mark(if(x,y,z)) = x + y + z + 0 >= x + y + z + 0 = if_active(mark(x),y,z)
          
          div_active(s(x),s(y)) = 1x + 0 >= 1x + 0 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
          
          if_active(true(),x,y) = x + y + 0 >= x = mark(x)
          
          minus_active(x,y) = x >= x = minus(x,y)
          
          if_active(false(),x,y) = x + y + 0 >= y = mark(y)
          
          ge_active(x,y) = x + 0 >= x + 0 = ge(x,y)
          
          if_active(x,y,z) = x + y + z + 0 >= x + y + z + 0 = if(x,y,z)
          
          div_active(x,y) = x >= x = div(x,y)
         problem:
          DPs:
           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)
          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)
         Arctic Interpretation Processor:
          dimension: 1
          interpretation:
           [if_active#](x0, x1, x2) = -5x0 + 1x1 + 5x2 + 0,
           
           [div_active#](x0, x1) = 1x0 + x1,
           
           [mark#](x0) = 1x0,
           
           [if_active](x0, x1, x2) = 1x0 + x1 + 7x2,
           
           [if](x0, x1, x2) = 1x0 + x1 + 7x2,
           
           [div_active](x0, x1) = 1x0 + x1 + -1,
           
           [div](x0, x1) = 1x0 + x1 + -1,
           
           [ge](x0, x1) = 5,
           
           [false] = 0,
           
           [minus](x0, x1) = 0,
           
           [true] = 5,
           
           [ge_active](x0, x1) = 5,
           
           [s](x0) = 6,
           
           [mark](x0) = x0,
           
           [minus_active](x0, x1) = 0,
           
           [0] = 0
          orientation:
           mark#(div(x,y)) = 2x + 1y + 0 >= 1x + y = div_active#(mark(x),y)
           
           div_active#(s(x),s(y)) = 7 >= 7 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
           
           if_active#(true(),x,y) = 1x + 5y + 0 >= 1x = mark#(x)
           
           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)) = 6 >= 6 = s(mark(x))
           
           ge_active(x,0()) = 5 >= 5 = true()
           
           mark(minus(x,y)) = 0 >= 0 = minus_active(x,y)
           
           ge_active(0(),s(y)) = 5 >= 0 = false()
           
           mark(ge(x,y)) = 5 >= 5 = ge_active(x,y)
           
           ge_active(s(x),s(y)) = 5 >= 5 = ge_active(x,y)
           
           mark(div(x,y)) = 1x + y + -1 >= 1x + y + -1 = div_active(mark(x),y)
           
           div_active(0(),s(y)) = 6 >= 0 = 0()
           
           mark(if(x,y,z)) = 1x + y + 7z >= 1x + y + 7z = if_active(mark(x),y,z)
           
           div_active(s(x),s(y)) = 7 >= 7 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
           
           if_active(true(),x,y) = x + 7y + 6 >= x = mark(x)
           
           minus_active(x,y) = 0 >= 0 = minus(x,y)
           
           if_active(false(),x,y) = x + 7y + 1 >= y = mark(y)
           
           ge_active(x,y) = 5 >= 5 = ge(x,y)
           
           if_active(x,y,z) = 1x + y + 7z >= 1x + y + 7z = if(x,y,z)
           
           div_active(x,y) = 1x + y + -1 >= 1x + y + -1 = div(x,y)
          problem:
           DPs:
            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)
           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)
          SCC Processor:
           #sccs: 0
           #rules: 0
           #arcs: 30/4
           
    
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(ge_active#) = 1
     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)
    Subterm Criterion Processor:
     simple projection:
      pi(minus_active#) = 1
     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