MAYBE

Problem:
 plus(0(),x) -> x
 plus(s(x),y) -> s(plus(x,y))
 times(0(),y) -> 0()
 times(s(x),y) -> plus(y,times(x,y))
 p(s(x)) -> x
 p(0()) -> 0()
 minus(x,0()) -> x
 minus(0(),x) -> 0()
 minus(x,s(y)) -> p(minus(x,y))
 isZero(0()) -> true()
 isZero(s(x)) -> false()
 facIter(x,y) -> if(isZero(x),minus(x,s(0())),y,times(y,x))
 if(true(),x,y,z) -> y
 if(false(),x,y,z) -> facIter(x,z)
 factorial(x) -> facIter(x,s(0()))

Proof:
 DP Processor:
  DPs:
   plus#(s(x),y) -> plus#(x,y)
   times#(s(x),y) -> times#(x,y)
   times#(s(x),y) -> plus#(y,times(x,y))
   minus#(x,s(y)) -> minus#(x,y)
   minus#(x,s(y)) -> p#(minus(x,y))
   facIter#(x,y) -> times#(y,x)
   facIter#(x,y) -> minus#(x,s(0()))
   facIter#(x,y) -> isZero#(x)
   facIter#(x,y) -> if#(isZero(x),minus(x,s(0())),y,times(y,x))
   if#(false(),x,y,z) -> facIter#(x,z)
   factorial#(x) -> facIter#(x,s(0()))
  TRS:
   plus(0(),x) -> x
   plus(s(x),y) -> s(plus(x,y))
   times(0(),y) -> 0()
   times(s(x),y) -> plus(y,times(x,y))
   p(s(x)) -> x
   p(0()) -> 0()
   minus(x,0()) -> x
   minus(0(),x) -> 0()
   minus(x,s(y)) -> p(minus(x,y))
   isZero(0()) -> true()
   isZero(s(x)) -> false()
   facIter(x,y) -> if(isZero(x),minus(x,s(0())),y,times(y,x))
   if(true(),x,y,z) -> y
   if(false(),x,y,z) -> facIter(x,z)
   factorial(x) -> facIter(x,s(0()))
  Usable Rule Processor:
   DPs:
    plus#(s(x),y) -> plus#(x,y)
    times#(s(x),y) -> times#(x,y)
    times#(s(x),y) -> plus#(y,times(x,y))
    minus#(x,s(y)) -> minus#(x,y)
    minus#(x,s(y)) -> p#(minus(x,y))
    facIter#(x,y) -> times#(y,x)
    facIter#(x,y) -> minus#(x,s(0()))
    facIter#(x,y) -> isZero#(x)
    facIter#(x,y) -> if#(isZero(x),minus(x,s(0())),y,times(y,x))
    if#(false(),x,y,z) -> facIter#(x,z)
    factorial#(x) -> facIter#(x,s(0()))
   TRS:
    times(0(),y) -> 0()
    times(s(x),y) -> plus(y,times(x,y))
    plus(0(),x) -> x
    plus(s(x),y) -> s(plus(x,y))
    minus(x,0()) -> x
    minus(0(),x) -> 0()
    minus(x,s(y)) -> p(minus(x,y))
    p(s(x)) -> x
    p(0()) -> 0()
    isZero(0()) -> true()
    isZero(s(x)) -> false()
   Open