/home/nowonder/forschung/aprove/TPDB05/TRS/D33/21.trs

The program

(VAR x y)
(RULES
p(s(x)) -> x
fact(0) -> s(0)
fact(s(x)) -> *(s(x),fact(p(s(x))))
*(0,y) -> 0
*(s(x),y) -> +(*(x,y),y)
+(x,0) -> x
+(x,s(y)) -> s(+(x,y))
)
(COMMENT Example 21 in \cite{D33})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend