Exercises |
---|

Prove that `power2` is strict. While one can base the proof on the "obvious" fact that `power2 ` is , the latter is preferably proven using fixed point iteration. |

Remember that:

power2 0 = 1 power2 n = 2 * power2 (n-1)

First, we need to consider whether `⊥ - 1`

is `⊥`

or not. Using similar reasoning to the `⊥ + 1`

case, we can determine that `⊥ - 1`

is indeed `⊥`

. From there, we know that `power2 ⊥`

is `2 * power2 ⊥`

. Since this recurses indefinitely, it is equivalent to `⊥`

.