# sicp-ex-1.16

## Solution 1

``` (define (iter-fast-expt b n)
(define (iter N B A)
(cond ((= 0 N) A)
((even? N) (iter (/ N 2) (square B) A))
(else (iter (- N 1) B (* B A)))))
(iter n b 1))
```

Claim.

```(iter N B A) = B^N * A
```

This claim implies that iter-fast-expt is correct:

```(iter-fast-expt b n)
= (iter n b 1)
= b^n * 1 by claim
= b^n
```

Proof of claim.

Induction on N.

Case 1: N = 0.

```(iter N B A)
= (iter 0 B A)
= A
= B^0 * A
= B^N * A
```

Case 2: N > 0 and N is even.

```(iter N B A)
= (iter N/2 B^2 A)
= (B^2)^(N/2) * A by the inductive hypothesis
= B^N * A
```

Case 3: N > 0 and N is odd.

```(iter N B A)
= (iter N-1 B B*A)
= B^(N-1) * B*A by the inductive hypothesis
= B^N * A
```

QED.

## Solution 2

```
(define (fast-expt b n)
(define (cube x) (* x x x))
(define (fast-expt-iter b a counter)
(cond ((= counter 0) a)
((= counter 1) (* a b))
((even? counter) (fast-expt-iter
(square b)
(* (square b) a)
(- (/ counter 2) 1)))
(else (fast-expt-iter
(square b)
(* (cube b) a)
(- (/ (- counter 1) 2) 1)))))
(fast-expt-iter b 1 n))
```