../../Task/Hailstone-sequence/ACL2