MAYBE

Problem:
 fac(0()) -> 1()
 fac(s(x)) -> *(s(x),fac(x))
 floop(0(),y) -> y
 floop(s(x),y) -> floop(x,*(s(x),y))
 *(x,0()) -> 0()
 *(x,s(y)) -> +(*(x,y),x)
 +(x,0()) -> x
 +(x,s(y)) -> s(+(x,y))
 1() -> s(0())
 fac(0()) -> s(0())

Proof:
 DP Processor:
  DPs:
   fac#(0()) -> 1#()
   fac#(s(x)) -> fac#(x)
   fac#(s(x)) -> *#(s(x),fac(x))
   floop#(s(x),y) -> *#(s(x),y)
   floop#(s(x),y) -> floop#(x,*(s(x),y))
   *#(x,s(y)) -> *#(x,y)
   *#(x,s(y)) -> +#(*(x,y),x)
   +#(x,s(y)) -> +#(x,y)
  TRS:
   fac(0()) -> 1()
   fac(s(x)) -> *(s(x),fac(x))
   floop(0(),y) -> y
   floop(s(x),y) -> floop(x,*(s(x),y))
   *(x,0()) -> 0()
   *(x,s(y)) -> +(*(x,y),x)
   +(x,0()) -> x
   +(x,s(y)) -> s(+(x,y))
   1() -> s(0())
   fac(0()) -> s(0())
  Open