MAYBE

Problem:
 minus(x,y) -> cond(min(x,y),x,y)
 cond(y,x,y) -> s(minus(x,s(y)))
 min(0(),v) -> 0()
 min(u,0()) -> 0()
 min(s(u),s(v)) -> s(min(u,v))

Proof:
 DP Processor:
  DPs:
   minus#(x,y) -> min#(x,y)
   minus#(x,y) -> cond#(min(x,y),x,y)
   cond#(y,x,y) -> minus#(x,s(y))
   min#(s(u),s(v)) -> min#(u,v)
  TRS:
   minus(x,y) -> cond(min(x,y),x,y)
   cond(y,x,y) -> s(minus(x,s(y)))
   min(0(),v) -> 0()
   min(u,0()) -> 0()
   min(s(u),s(v)) -> s(min(u,v))
  Usable Rule Processor:
   DPs:
    minus#(x,y) -> min#(x,y)
    minus#(x,y) -> cond#(min(x,y),x,y)
    cond#(y,x,y) -> minus#(x,s(y))
    min#(s(u),s(v)) -> min#(u,v)
   TRS:
    min(0(),v) -> 0()
    min(u,0()) -> 0()
    min(s(u),s(v)) -> s(min(u,v))
   Open