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)
  TDG 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)
   graph:
    mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(div(X1,X2)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(geq(X1,X2)) -> a__geq#(X1,X2)
    mark#(if(X1,X2,X3)) -> mark#(X1) ->
    mark#(minus(X1,X2)) -> a__minus#(X1,X2)
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) ->
    a__if#(false(),X,Y) -> mark#(Y)
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) ->
    a__if#(true(),X,Y) -> mark#(X)
    mark#(geq(X1,X2)) -> a__geq#(X1,X2) ->
    a__geq#(s(X),s(Y)) -> a__geq#(X,Y)
    mark#(div(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
    mark#(div(X1,X2)) -> mark#(X1) -> mark#(div(X1,X2)) -> mark#(X1)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(geq(X1,X2)) -> a__geq#(X1,X2)
    mark#(div(X1,X2)) -> mark#(X1) ->
    mark#(minus(X1,X2)) -> a__minus#(X1,X2)
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2) ->
    a__div#(s(X),s(Y)) -> a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2) ->
    a__div#(s(X),s(Y)) -> a__geq#(X,Y)
    mark#(minus(X1,X2)) -> a__minus#(X1,X2) ->
    a__minus#(s(X),s(Y)) -> a__minus#(X,Y)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
    mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) -> mark#(div(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(geq(X1,X2)) -> a__geq#(X1,X2)
    mark#(s(X)) -> mark#(X) ->
    mark#(minus(X1,X2)) -> a__minus#(X1,X2)
    a__if#(false(),X,Y) -> mark#(Y) -> mark#(s(X)) -> mark#(X)
    a__if#(false(),X,Y) -> mark#(Y) ->
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
    a__if#(false(),X,Y) -> mark#(Y) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    a__if#(false(),X,Y) -> mark#(Y) ->
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
    a__if#(false(),X,Y) -> mark#(Y) ->
    mark#(div(X1,X2)) -> mark#(X1)
    a__if#(false(),X,Y) -> mark#(Y) ->
    mark#(geq(X1,X2)) -> a__geq#(X1,X2)
    a__if#(false(),X,Y) -> mark#(Y) ->
    mark#(minus(X1,X2)) -> a__minus#(X1,X2)
    a__if#(true(),X,Y) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__if#(true(),X,Y) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
    a__if#(true(),X,Y) -> mark#(X) ->
    mark#(if(X1,X2,X3)) -> mark#(X1)
    a__if#(true(),X,Y) -> mark#(X) ->
    mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
    a__if#(true(),X,Y) -> mark#(X) -> mark#(div(X1,X2)) -> mark#(X1)
    a__if#(true(),X,Y) -> mark#(X) ->
    mark#(geq(X1,X2)) -> a__geq#(X1,X2)
    a__if#(true(),X,Y) -> mark#(X) ->
    mark#(minus(X1,X2)) -> a__minus#(X1,X2)
    a__div#(s(X),s(Y)) -> a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) ->
    a__if#(false(),X,Y) -> mark#(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__div#(s(X),s(Y)) -> a__geq#(X,Y) ->
    a__geq#(s(X),s(Y)) -> a__geq#(X,Y)
    a__geq#(s(X),s(Y)) -> a__geq#(X,Y) ->
    a__geq#(s(X),s(Y)) -> a__geq#(X,Y)
    a__minus#(s(X),s(Y)) -> a__minus#(X,Y) -> a__minus#(s(X),s(Y)) -> a__minus#(X,Y)
   SCC Processor:
    #sccs: 3
    #rules: 10
    #arcs: 46/169
    DPs:
     mark#(if(X1,X2,X3)) -> mark#(X1)
     mark#(div(X1,X2)) -> mark#(X1)
     mark#(div(X1,X2)) -> a__div#(mark(X1),X2)
     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)
     mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3)
     a__if#(false(),X,Y) -> mark#(Y)
     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,
      
      [a__if#](x0, x1, x2) = 4x0 + 2x1 + 2x2 + 1,
      
      [a__div#](x0, x1) = 7x0 + 1,
      
      [if](x0, x1, x2) = 2x0 + 2x1 + x2 + 1,
      
      [geq](x0, x1) = 0,
      
      [mark](x0) = x0,
      
      [a__if](x0, x1, x2) = 2x0 + 2x1 + x2 + 1,
      
      [div](x0, x1) = 6x0 + 1,
      
      [minus](x0, x1) = 0,
      
      [a__div](x0, x1) = 6x0 + 1,
      
      [false] = 0,
      
      [true] = 0,
      
      [a__geq](x0, x1) = 0,
      
      [s](x0) = 2x0 + 1,
      
      [a__minus](x0, x1) = 0,
      
      [0] = 0
     orientation:
      mark#(if(X1,X2,X3)) = 4X1 + 4X2 + 2X3 + 2 >= 2X1 = mark#(X1)
      
      mark#(div(X1,X2)) = 12X1 + 2 >= 2X1 = mark#(X1)
      
      mark#(div(X1,X2)) = 12X1 + 2 >= 7X1 + 1 = a__div#(mark(X1),X2)
      
      a__div#(s(X),s(Y)) = 14X + 8 >= 7 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
      
      a__if#(true(),X,Y) = 2X + 2Y + 1 >= 2X = mark#(X)
      
      mark#(if(X1,X2,X3)) = 4X1 + 4X2 + 2X3 + 2 >= 4X1 + 2X2 + 2X3 + 1 = a__if#(mark(X1),X2,X3)
      
      a__if#(false(),X,Y) = 2X + 2Y + 1 >= 2Y = mark#(Y)
      
      mark#(s(X)) = 4X + 2 >= 2X = mark#(X)
      
      a__minus(0(),Y) = 0 >= 0 = 0()
      
      a__minus(s(X),s(Y)) = 0 >= 0 = a__minus(X,Y)
      
      a__geq(X,0()) = 0 >= 0 = true()
      
      a__geq(0(),s(Y)) = 0 >= 0 = false()
      
      a__geq(s(X),s(Y)) = 0 >= 0 = a__geq(X,Y)
      
      a__div(0(),s(Y)) = 1 >= 0 = 0()
      
      a__div(s(X),s(Y)) = 12X + 7 >= 7 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
      
      a__if(true(),X,Y) = 2X + Y + 1 >= X = mark(X)
      
      a__if(false(),X,Y) = 2X + Y + 1 >= Y = mark(Y)
      
      mark(minus(X1,X2)) = 0 >= 0 = a__minus(X1,X2)
      
      mark(geq(X1,X2)) = 0 >= 0 = a__geq(X1,X2)
      
      mark(div(X1,X2)) = 6X1 + 1 >= 6X1 + 1 = a__div(mark(X1),X2)
      
      mark(if(X1,X2,X3)) = 2X1 + 2X2 + X3 + 1 >= 2X1 + 2X2 + X3 + 1 = a__if(mark(X1),X2,X3)
      
      mark(0()) = 0 >= 0 = 0()
      
      mark(s(X)) = 2X + 1 >= 2X + 1 = s(mark(X))
      
      mark(true()) = 0 >= 0 = true()
      
      mark(false()) = 0 >= 0 = false()
      
      a__minus(X1,X2) = 0 >= 0 = minus(X1,X2)
      
      a__geq(X1,X2) = 0 >= 0 = geq(X1,X2)
      
      a__div(X1,X2) = 6X1 + 1 >= 6X1 + 1 = div(X1,X2)
      
      a__if(X1,X2,X3) = 2X1 + 2X2 + X3 + 1 >= 2X1 + 2X2 + X3 + 1 = 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
    
    DPs:
     a__geq#(s(X),s(Y)) -> a__geq#(X,Y)
    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:
      [a__geq#](x0, x1) = 2x1 + 1,
      
      [if](x0, x1, x2) = x0 + x1 + x2,
      
      [geq](x0, x1) = 4x0 + 2,
      
      [mark](x0) = x0,
      
      [a__if](x0, x1, x2) = x0 + x1 + x2,
      
      [div](x0, x1) = 7x0 + 4,
      
      [minus](x0, x1) = 0,
      
      [a__div](x0, x1) = 7x0 + 4,
      
      [false] = 2,
      
      [true] = 2,
      
      [a__geq](x0, x1) = 4x0 + 2,
      
      [s](x0) = 2x0 + 1,
      
      [a__minus](x0, x1) = 0,
      
      [0] = 0
     orientation:
      a__geq#(s(X),s(Y)) = 4Y + 3 >= 2Y + 1 = a__geq#(X,Y)
      
      a__minus(0(),Y) = 0 >= 0 = 0()
      
      a__minus(s(X),s(Y)) = 0 >= 0 = a__minus(X,Y)
      
      a__geq(X,0()) = 4X + 2 >= 2 = true()
      
      a__geq(0(),s(Y)) = 2 >= 2 = false()
      
      a__geq(s(X),s(Y)) = 8X + 6 >= 4X + 2 = a__geq(X,Y)
      
      a__div(0(),s(Y)) = 4 >= 0 = 0()
      
      a__div(s(X),s(Y)) = 14X + 11 >= 4X + 11 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
      
      a__if(true(),X,Y) = X + Y + 2 >= X = mark(X)
      
      a__if(false(),X,Y) = X + Y + 2 >= Y = mark(Y)
      
      mark(minus(X1,X2)) = 0 >= 0 = a__minus(X1,X2)
      
      mark(geq(X1,X2)) = 4X1 + 2 >= 4X1 + 2 = a__geq(X1,X2)
      
      mark(div(X1,X2)) = 7X1 + 4 >= 7X1 + 4 = a__div(mark(X1),X2)
      
      mark(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = a__if(mark(X1),X2,X3)
      
      mark(0()) = 0 >= 0 = 0()
      
      mark(s(X)) = 2X + 1 >= 2X + 1 = s(mark(X))
      
      mark(true()) = 2 >= 2 = true()
      
      mark(false()) = 2 >= 2 = false()
      
      a__minus(X1,X2) = 0 >= 0 = minus(X1,X2)
      
      a__geq(X1,X2) = 4X1 + 2 >= 4X1 + 2 = geq(X1,X2)
      
      a__div(X1,X2) = 7X1 + 4 >= 7X1 + 4 = div(X1,X2)
      
      a__if(X1,X2,X3) = X1 + X2 + X3 >= X1 + X2 + X3 = 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
    
    DPs:
     a__minus#(s(X),s(Y)) -> a__minus#(X,Y)
    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:
      [a__minus#](x0, x1) = 2x1 + 1,
      
      [if](x0, x1, x2) = x0 + x1 + x2,
      
      [geq](x0, x1) = 4x0 + 2,
      
      [mark](x0) = x0,
      
      [a__if](x0, x1, x2) = x0 + x1 + x2,
      
      [div](x0, x1) = 7x0 + 4,
      
      [minus](x0, x1) = 0,
      
      [a__div](x0, x1) = 7x0 + 4,
      
      [false] = 2,
      
      [true] = 2,
      
      [a__geq](x0, x1) = 4x0 + 2,
      
      [s](x0) = 2x0 + 1,
      
      [a__minus](x0, x1) = 0,
      
      [0] = 0
     orientation:
      a__minus#(s(X),s(Y)) = 4Y + 3 >= 2Y + 1 = a__minus#(X,Y)
      
      a__minus(0(),Y) = 0 >= 0 = 0()
      
      a__minus(s(X),s(Y)) = 0 >= 0 = a__minus(X,Y)
      
      a__geq(X,0()) = 4X + 2 >= 2 = true()
      
      a__geq(0(),s(Y)) = 2 >= 2 = false()
      
      a__geq(s(X),s(Y)) = 8X + 6 >= 4X + 2 = a__geq(X,Y)
      
      a__div(0(),s(Y)) = 4 >= 0 = 0()
      
      a__div(s(X),s(Y)) = 14X + 11 >= 4X + 11 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0())
      
      a__if(true(),X,Y) = X + Y + 2 >= X = mark(X)
      
      a__if(false(),X,Y) = X + Y + 2 >= Y = mark(Y)
      
      mark(minus(X1,X2)) = 0 >= 0 = a__minus(X1,X2)
      
      mark(geq(X1,X2)) = 4X1 + 2 >= 4X1 + 2 = a__geq(X1,X2)
      
      mark(div(X1,X2)) = 7X1 + 4 >= 7X1 + 4 = a__div(mark(X1),X2)
      
      mark(if(X1,X2,X3)) = X1 + X2 + X3 >= X1 + X2 + X3 = a__if(mark(X1),X2,X3)
      
      mark(0()) = 0 >= 0 = 0()
      
      mark(s(X)) = 2X + 1 >= 2X + 1 = s(mark(X))
      
      mark(true()) = 2 >= 2 = true()
      
      mark(false()) = 2 >= 2 = false()
      
      a__minus(X1,X2) = 0 >= 0 = minus(X1,X2)
      
      a__geq(X1,X2) = 4X1 + 2 >= 4X1 + 2 = geq(X1,X2)
      
      a__div(X1,X2) = 7X1 + 4 >= 7X1 + 4 = div(X1,X2)
      
      a__if(X1,X2,X3) = X1 + X2 + X3 >= X1 + X2 + X3 = 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