/home/nowonder/forschung/aprove/TPDB05/TRS/AG01/#3.7.trs

The program

(from AG01 3.7)
(VAR x)
(RULES
half(0) -> 0
half(s(s(x))) -> s(half(x))
log(s(0)) -> 0
log(s(s(x))) -> s(log(s(half(x))))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend