MAYBE

Problem:
 f(x,y) -> cond(lt(x,y),x,y)
 cond(tt(),x,y) -> f(s(x),s(y))
 lt(0(),y) -> tt()
 lt(s(x),s(y)) -> lt(x,y)

Proof:
 DP Processor:
  DPs:
   f#(x,y) -> lt#(x,y)
   f#(x,y) -> cond#(lt(x,y),x,y)
   cond#(tt(),x,y) -> f#(s(x),s(y))
   lt#(s(x),s(y)) -> lt#(x,y)
  TRS:
   f(x,y) -> cond(lt(x,y),x,y)
   cond(tt(),x,y) -> f(s(x),s(y))
   lt(0(),y) -> tt()
   lt(s(x),s(y)) -> lt(x,y)
  Usable Rule Processor:
   DPs:
    f#(x,y) -> lt#(x,y)
    f#(x,y) -> cond#(lt(x,y),x,y)
    cond#(tt(),x,y) -> f#(s(x),s(y))
    lt#(s(x),s(y)) -> lt#(x,y)
   TRS:
    lt(0(),y) -> tt()
    lt(s(x),s(y)) -> lt(x,y)
   Open