/home/nowonder/forschung/aprove/TPDB05/TRS/HM/t008.trs

The program

(VAR x)
(RULES
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
s(log(0)) -> s(0)
log(s(x)) -> s(log(half(s(x))))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend