Blocks

Purpose of exercise

Activities

Requirements

Properties

Notes

The following intrinsic ACL2 functions will be useful in this problem

You may find it helpful to define the following functions