-9.4.1 - proof by induction over as

-

-Induction base:

- Suppose as = []. Then we have:

-

- map f (as ++ bs) // assumption as = []

- = map f ([] ++ bs) // definition of ++, rule 1

- = map f bs // definition of ++, rule 1

- = [] ++ (map f bs) // definition of map, rule 3

- = (map f []) ++ (map f bs) // assumption as = []

- = (map f as) ++ (map f bs).

-

-Induction step:

- Suppose map f (as ++ bs) = (map f as) ++ (map f bs) for certain as and any bs (induction hypothesis). Then we have:

-

- map f ([a:as] ++ bs) // definition of ++, rule 2

- = map f [a:as ++ bs] // definition of map, rule 4

- = [f a : map f (as ++ bs)] // induction hypothesis: assumption map f (as ++ bs) = (map f as) ++ (map f bs)

- = [f a : (map f as) ++ (map f bs)] // rewriting list

- = [f a : map f as] ++ (map f bs) // definition of map, rule 4

- = (map f [a:as]) ++ (map f bs).

-

-By the principle of induction we have now proven that map f (as ++ bs) = (map f as) ++ (map f bs) for any finite lists as, bs. \ No newline at end of file