YES
Input TRS:
    1: add(0(),x) -> x
    2: add(s(x),y) -> s(add(x,y))
    3: mult(0(),y) -> 0()
    4: mult(s(x),y) -> add(mult(x,y),y)
    5: lte(0(),y) -> true()
    6: lte(s(x),0()) -> false()
    7: lte(s(x),s(y)) -> lte(x,y)
    8: minus(0(),s(y)) -> 0()
    9: minus(x,0()) -> x
    10: minus(s(x),s(y)) -> minus(x,y)
    11: mod(0(),y) -> 0()
    12: mod(x,0()) -> x
    13: mod(x,s(y)) -> mod(minus(x,s(y)),s(y)) | lte(s(y),x) --> true()
    14: mod(x,s(y)) -> x | lte(s(y),x) --> false()
    15: div(0(),s(x)) -> 0()
    16: div(s(x),s(y)) -> 0() | lte(s(x),y) --> true()
    17: div(s(x),s(y)) -> s(q) | lte(s(x),y) --> false() | div(minus(x,y),s(y)) --> q
    18: power(x,0()) -> s(0())
    19: power(x,n) -> mult(mult(y,y),s(0())) | mod(n,s(s(0()))) --> 0() | power(x,div(n,s(s(0())))) --> y
    20: power(x,n) -> mult(mult(y,y),x) | mod(n,s(s(0()))) --> s(z) | power(x,div(n,s(s(0())))) --> y
Infeasibility test:
    mod(0(),s(s(0()))) --> s(x1)
    power(x2,div(0(),s(s(0())))) --> x4
Co-Order(NegReal,≥,Sum) ... succeeded.
   lte(x1,x2)	weight: 0
     s(x1)	weight: 0
 minus(x1,x2)	weight: x1
   mod(x1,x2)	weight: x1
 false()	weight: 0
   div(x1,x2)	weight: 0
  true()	weight: 0
  mult(x1,x2)	weight: 0
     0()	weight: (- (/ 1 2))
 power(x1,x2)	weight: 0
    #(x1,x2)	weight: x1
   add(x1,x2)	weight: 0