/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/4.17.trs

The program

(VAR x y z)
(RULES
fac(s(x)) -> *(fac(p(s(x))),s(x))
p(s(0)) -> 0
p(s(s(x))) -> s(p(s(x)))
)
(COMMENT Example 4.17 (Factorial Function) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend