Compress

Purpose of exercise

• Get started writing equation-based programs
• Practice specifying correctness properties
• Use DrACuLa DoubleCheck for predicate-based, random testing
• Certify correctness properties using ACL2

Activities

• Define the following function
• Package the function you define as a book.
• DoubleCheck the property stated below
• Use ACL2 to prove the property
• Package the theorem as a book.

Requirements

• (compress xs) is a list like xs, but with all adjacent occurrences of identical elements  compressed to one occurrence

Notes

• (member-equal x xs) is an intrinsic ACL2 function that will be useful in this problem