(from AG01 4.28) (VAR x) (RULES half(0) -> 0 half(s(0)) -> 0 half(s(s(x))) -> s(half(x)) bits(0) -> 0 bits(s(x)) -> s(bits(half(s(x)))) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend