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))
  TDG 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))
   graph:
    cond#(y,x,y) -> minus#(x,s(y)) ->
    minus#(x,y) -> cond#(min(x,y),x,y)
    cond#(y,x,y) -> minus#(x,s(y)) -> minus#(x,y) -> min#(x,y)
    min#(s(u),s(v)) -> min#(u,v) -> min#(s(u),s(v)) -> min#(u,v)
    minus#(x,y) -> cond#(min(x,y),x,y) -> cond#(y,x,y) -> minus#(x,s(y))
    minus#(x,y) -> min#(x,y) -> min#(s(u),s(v)) -> min#(u,v)
   SCC Processor:
    #sccs: 2
    #rules: 3
    #arcs: 5/16
    DPs:
     cond#(y,x,y) -> minus#(x,s(y))
     minus#(x,y) -> cond#(min(x,y),x,y)
    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))
    Open
    
    DPs:
     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))
    Open