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)
  EDG 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#(s(x)) -> mark#(x)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(minus(x,y)) -> minus_active#(x,y)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(ge(x,y)) -> ge_active#(x,y)
    if_active#(false(),x,y) -> mark#(y) ->
    mark#(div(x,y)) -> 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#(if(x,y,z)) -> mark#(x)
    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#(s(x)) -> mark#(x)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(minus(x,y)) -> minus_active#(x,y)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(ge(x,y)) -> ge_active#(x,y)
    if_active#(true(),x,y) -> mark#(x) ->
    mark#(div(x,y)) -> 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#(if(x,y,z)) -> mark#(x)
    if_active#(true(),x,y) -> mark#(x) ->
    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)
    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)) -> 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#(true(),x,y) -> mark#(x)
    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) -> mark#(s(x)) -> mark#(x)
    mark#(if(x,y,z)) -> mark#(x) ->
    mark#(minus(x,y)) -> minus_active#(x,y)
    mark#(if(x,y,z)) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y)
    mark#(if(x,y,z)) -> mark#(x) -> mark#(div(x,y)) -> 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#(if(x,y,z)) -> mark#(x)
    mark#(if(x,y,z)) -> mark#(x) ->
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    mark#(div(x,y)) -> div_active#(mark(x),y) ->
    div_active#(s(x),s(y)) -> ge_active#(x,y)
    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)) -> mark#(x) -> mark#(s(x)) -> mark#(x)
    mark#(div(x,y)) -> mark#(x) ->
    mark#(minus(x,y)) -> minus_active#(x,y)
    mark#(div(x,y)) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y)
    mark#(div(x,y)) -> mark#(x) -> mark#(div(x,y)) -> mark#(x)
    mark#(div(x,y)) -> mark#(x) ->
    mark#(div(x,y)) -> div_active#(mark(x),y)
    mark#(div(x,y)) -> mark#(x) -> mark#(if(x,y,z)) -> mark#(x)
    mark#(div(x,y)) -> mark#(x) ->
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    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#(s(x)) -> mark#(x)
    mark#(s(x)) -> mark#(x) -> mark#(minus(x,y)) -> minus_active#(x,y)
    mark#(s(x)) -> mark#(x) -> mark#(ge(x,y)) -> ge_active#(x,y)
    mark#(s(x)) -> mark#(x) -> mark#(div(x,y)) -> mark#(x)
    mark#(s(x)) -> mark#(x) -> mark#(div(x,y)) -> div_active#(mark(x),y)
    mark#(s(x)) -> mark#(x) -> mark#(if(x,y,z)) -> mark#(x)
    mark#(s(x)) -> mark#(x) ->
    mark#(if(x,y,z)) -> if_active#(mark(x),y,z)
    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#(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#(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)) -> mark#(x)
     mark#(s(x)) -> 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)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [if_active#](x0, x1, x2) = x1 + x2,
      
      [div_active#](x0, x1) = x0,
      
      [mark#](x0) = x0,
      
      [if_active](x0, x1, x2) = x0 + x1 + x2,
      
      [if](x0, x1, x2) = x0 + x1 + x2,
      
      [div_active](x0, x1) = x0,
      
      [div](x0, x1) = x0,
      
      [ge](x0, x1) = 0,
      
      [false] = 0,
      
      [minus](x0, x1) = 0,
      
      [true] = 0,
      
      [ge_active](x0, x1) = 0,
      
      [s](x0) = x0 + 1,
      
      [mark](x0) = x0,
      
      [minus_active](x0, x1) = 0,
      
      [0] = 0
     orientation:
      if_active#(false(),x,y) = x + y >= y = mark#(y)
      
      mark#(if(x,y,z)) = x + y + z >= y + z = if_active#(mark(x),y,z)
      
      if_active#(true(),x,y) = x + y >= x = mark#(x)
      
      mark#(if(x,y,z)) = x + y + z >= x = mark#(x)
      
      mark#(div(x,y)) = x >= x = div_active#(mark(x),y)
      
      div_active#(s(x),s(y)) = x + 1 >= 1 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      
      mark#(div(x,y)) = x >= x = mark#(x)
      
      mark#(s(x)) = x + 1 >= x = 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)) = x + 1 >= x + 1 = 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)) = x >= x = div_active(mark(x),y)
      
      div_active(0(),s(y)) = 0 >= 0 = 0()
      
      mark(if(x,y,z)) = x + y + z >= x + y + z = if_active(mark(x),y,z)
      
      div_active(s(x),s(y)) = x + 1 >= 1 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
      
      if_active(true(),x,y) = x + y >= x = mark(x)
      
      minus_active(x,y) = 0 >= 0 = minus(x,y)
      
      if_active(false(),x,y) = x + y >= y = mark(y)
      
      ge_active(x,y) = 0 >= 0 = ge(x,y)
      
      if_active(x,y,z) = x + y + z >= x + y + z = if(x,y,z)
      
      div_active(x,y) = x >= x = div(x,y)
     problem:
      DPs:
       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#(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)) -> 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)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [if_active#](x0, x1, x2) = x1 + x2,
       
       [div_active#](x0, x1) = 0,
       
       [mark#](x0) = x0,
       
       [if_active](x0, x1, x2) = x0 + x1 + x2,
       
       [if](x0, x1, x2) = x0 + x1 + x2,
       
       [div_active](x0, x1) = x0 + 1,
       
       [div](x0, x1) = x0 + 1,
       
       [ge](x0, x1) = 0,
       
       [false] = 0,
       
       [minus](x0, x1) = 0,
       
       [true] = 0,
       
       [ge_active](x0, x1) = 0,
       
       [s](x0) = 0,
       
       [mark](x0) = x0,
       
       [minus_active](x0, x1) = 0,
       
       [0] = 0
      orientation:
       if_active#(false(),x,y) = x + y >= y = mark#(y)
       
       mark#(if(x,y,z)) = x + y + z >= y + z = if_active#(mark(x),y,z)
       
       if_active#(true(),x,y) = x + y >= x = mark#(x)
       
       mark#(if(x,y,z)) = x + y + z >= x = mark#(x)
       
       mark#(div(x,y)) = x + 1 >= 0 = div_active#(mark(x),y)
       
       div_active#(s(x),s(y)) = 0 >= 0 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
       
       mark#(div(x,y)) = x + 1 >= x = 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)) = 0 >= 0 = 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)) = x + 1 >= x + 1 = div_active(mark(x),y)
       
       div_active(0(),s(y)) = 1 >= 0 = 0()
       
       mark(if(x,y,z)) = x + y + z >= x + y + z = if_active(mark(x),y,z)
       
       div_active(s(x),s(y)) = 1 >= 0 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
       
       if_active(true(),x,y) = x + y >= x = mark(x)
       
       minus_active(x,y) = 0 >= 0 = minus(x,y)
       
       if_active(false(),x,y) = x + y >= y = mark(y)
       
       ge_active(x,y) = 0 >= 0 = ge(x,y)
       
       if_active(x,y,z) = x + y + z >= x + y + z = if(x,y,z)
       
       div_active(x,y) = x + 1 >= x + 1 = div(x,y)
      problem:
       DPs:
        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)
        div_active#(s(x),s(y)) -> if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
       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:
       dimension: 1
       interpretation:
        [if_active#](x0, x1, x2) = 0,
        
        [div_active#](x0, x1) = 1,
        
        [mark#](x0) = 0,
        
        [if_active](x0, x1, x2) = x0,
        
        [if](x0, x1, x2) = x0,
        
        [div_active](x0, x1) = 1,
        
        [div](x0, x1) = 0,
        
        [ge](x0, x1) = 0,
        
        [false] = 1,
        
        [minus](x0, x1) = 0,
        
        [true] = 1,
        
        [ge_active](x0, x1) = 1,
        
        [s](x0) = 0,
        
        [mark](x0) = 1,
        
        [minus_active](x0, x1) = 0,
        
        [0] = 0
       orientation:
        if_active#(false(),x,y) = 0 >= 0 = mark#(y)
        
        mark#(if(x,y,z)) = 0 >= 0 = if_active#(mark(x),y,z)
        
        if_active#(true(),x,y) = 0 >= 0 = mark#(x)
        
        mark#(if(x,y,z)) = 0 >= 0 = mark#(x)
        
        div_active#(s(x),s(y)) = 1 >= 0 = if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0())
        
        minus_active(0(),y) = 0 >= 0 = 0()
        
        mark(0()) = 1 >= 0 = 0()
        
        minus_active(s(x),s(y)) = 0 >= 0 = minus_active(x,y)
        
        mark(s(x)) = 1 >= 0 = s(mark(x))
        
        ge_active(x,0()) = 1 >= 1 = true()
        
        mark(minus(x,y)) = 1 >= 0 = minus_active(x,y)
        
        ge_active(0(),s(y)) = 1 >= 1 = false()
        
        mark(ge(x,y)) = 1 >= 1 = ge_active(x,y)
        
        ge_active(s(x),s(y)) = 1 >= 1 = ge_active(x,y)
        
        mark(div(x,y)) = 1 >= 1 = div_active(mark(x),y)
        
        div_active(0(),s(y)) = 1 >= 0 = 0()
        
        mark(if(x,y,z)) = 1 >= 1 = if_active(mark(x),y,z)
        
        div_active(s(x),s(y)) = 1 >= 1 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
        
        if_active(true(),x,y) = 1 >= 1 = mark(x)
        
        minus_active(x,y) = 0 >= 0 = minus(x,y)
        
        if_active(false(),x,y) = 1 >= 1 = mark(y)
        
        ge_active(x,y) = 1 >= 0 = ge(x,y)
        
        if_active(x,y,z) = x >= x = if(x,y,z)
        
        div_active(x,y) = 1 >= 0 = div(x,y)
       problem:
        DPs:
         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)
        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:
        dimension: 1
        interpretation:
         [if_active#](x0, x1, x2) = x1 + x2,
         
         [mark#](x0) = x0,
         
         [if_active](x0, x1, x2) = x0 + x1 + x2 + 1,
         
         [if](x0, x1, x2) = x0 + x1 + x2 + 1,
         
         [div_active](x0, x1) = 1,
         
         [div](x0, x1) = 1,
         
         [ge](x0, x1) = 0,
         
         [false] = 0,
         
         [minus](x0, x1) = 0,
         
         [true] = 0,
         
         [ge_active](x0, x1) = 0,
         
         [s](x0) = 0,
         
         [mark](x0) = x0,
         
         [minus_active](x0, x1) = 0,
         
         [0] = 0
        orientation:
         if_active#(false(),x,y) = x + y >= y = mark#(y)
         
         mark#(if(x,y,z)) = x + y + z + 1 >= y + z = if_active#(mark(x),y,z)
         
         if_active#(true(),x,y) = x + y >= x = mark#(x)
         
         mark#(if(x,y,z)) = x + y + z + 1 >= x = 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)) = 0 >= 0 = 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)) = 1 >= 1 = div_active(mark(x),y)
         
         div_active(0(),s(y)) = 1 >= 0 = 0()
         
         mark(if(x,y,z)) = x + y + z + 1 >= x + y + z + 1 = if_active(mark(x),y,z)
         
         div_active(s(x),s(y)) = 1 >= 1 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
         
         if_active(true(),x,y) = x + y + 1 >= x = mark(x)
         
         minus_active(x,y) = 0 >= 0 = minus(x,y)
         
         if_active(false(),x,y) = x + y + 1 >= y = mark(y)
         
         ge_active(x,y) = 0 >= 0 = ge(x,y)
         
         if_active(x,y,z) = x + y + z + 1 >= x + y + z + 1 = if(x,y,z)
         
         div_active(x,y) = 1 >= 1 = div(x,y)
        problem:
         DPs:
          if_active#(false(),x,y) -> mark#(y)
          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)
        Matrix Interpretation Processor:
         dimension: 1
         interpretation:
          [if_active#](x0, x1, x2) = x0 + 1,
          
          [mark#](x0) = 0,
          
          [if_active](x0, x1, x2) = 1,
          
          [if](x0, x1, x2) = 1,
          
          [div_active](x0, x1) = 1,
          
          [div](x0, x1) = 1,
          
          [ge](x0, x1) = 1,
          
          [false] = 1,
          
          [minus](x0, x1) = 1,
          
          [true] = 1,
          
          [ge_active](x0, x1) = 1,
          
          [s](x0) = x0,
          
          [mark](x0) = 1,
          
          [minus_active](x0, x1) = 1,
          
          [0] = 1
         orientation:
          if_active#(false(),x,y) = 2 >= 0 = mark#(y)
          
          if_active#(true(),x,y) = 2 >= 0 = mark#(x)
          
          minus_active(0(),y) = 1 >= 1 = 0()
          
          mark(0()) = 1 >= 1 = 0()
          
          minus_active(s(x),s(y)) = 1 >= 1 = minus_active(x,y)
          
          mark(s(x)) = 1 >= 1 = s(mark(x))
          
          ge_active(x,0()) = 1 >= 1 = true()
          
          mark(minus(x,y)) = 1 >= 1 = minus_active(x,y)
          
          ge_active(0(),s(y)) = 1 >= 1 = false()
          
          mark(ge(x,y)) = 1 >= 1 = ge_active(x,y)
          
          ge_active(s(x),s(y)) = 1 >= 1 = ge_active(x,y)
          
          mark(div(x,y)) = 1 >= 1 = div_active(mark(x),y)
          
          div_active(0(),s(y)) = 1 >= 1 = 0()
          
          mark(if(x,y,z)) = 1 >= 1 = if_active(mark(x),y,z)
          
          div_active(s(x),s(y)) = 1 >= 1 = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0())
          
          if_active(true(),x,y) = 1 >= 1 = mark(x)
          
          minus_active(x,y) = 1 >= 1 = minus(x,y)
          
          if_active(false(),x,y) = 1 >= 1 = mark(y)
          
          ge_active(x,y) = 1 >= 1 = ge(x,y)
          
          if_active(x,y,z) = 1 >= 1 = if(x,y,z)
          
          div_active(x,y) = 1 >= 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:
     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
    
    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