# Recursion and Induction, Nov. 1, 2011

### Today's Examples

A simple demo
A demo illustrating a bit of high-level strategy
Log of today's ACL2 session: `log.txt`

### Main points made today:

- Sometimes you can take a low-level
*tactical* approach,
focusing on the key checkpoints printed at the end of the proof --
either pre-induction, if you don't expect induction to be needed,
else post-induction.
- Sometimes, as in the rotate example, you need to think of some
high-level
*strategy*, as is typical in mathematical
proofs.
- Rewriting is a key proof technique in ACL2. We spent a little
time on it, including the notion of formulating rewrite rules that
can replace an expression by a "simpler" expression.

### Other important points discussed today